ADM-201 dump PMP dumps pdf SSCP exam materials CBAP exam sample questions

有什么软件是黑客黑不了的吗? – 译学馆
未登陆,请登陆后再发表信息
最新评论 (0)
播放视频

有什么软件是黑客黑不了的吗?

How coders are creating software that's impossible to hack | Kathleen Fisher

有什么是黑客黑不了的吗?
“HACMS”是美国国防部高级研究计划局的一个历时4.5年的项目
HACMS is a program at DARPA that ran for four-and-a-half years
该项目聚焦于科技的运用
that was focused on using techniques
研究人员被称为“形式验证团队”
from what is called the ‘formal methods community’,
大家都知道技术或多或少都以数学为基础
so techniques based on math more or less,
这样才能确保做出来的软件系统
to produce software for vehicles that came with proofs
有令人满意的性能
that the software had certain desirable properties;
HACMS的功能相当卓越
that parts of it were functionally correct,
没有漏洞 也不会出故障
that there were no bugs and certain kinds of bugs in the software.
由此导致的结果就是
And the consequence of those proofs is
系统更难被侵入了
that the system is much harder to hack into.
而该团队一直以来的理念就是
So the formal methods community has been promising for, like,
哪怕用上50年来生产一种软件
50 years that they could produce
也必定要确保该软件没有任何特定的缺陷
software that provably didn’t have certain kind of vulnerabilities.
先不说该软件系统的研发期有没有50年
And for more or less 50 years they
反正该团队在软件效果上并没有食言
have failed to deliver on that promise.
是的 他们正努力打造可靠性极高的源代码
Yes, they could produce proofs of correctness
而原先那些10行 100行的编码
for code but for ten lines of code or 100
根本不足以
lines of code—not enough code to make a difference
产生实际性的影响
for any kind of practical purpose.
近来在不同的研究领域
But recently there have been advances
编码问题一直有所突破
in a bunch of different research areas that have
代码形式也有了改观
changed that equation,
所以形式验证团队的研究员们为了确保该系统的性能
and so now formal methods researchers can prove important properties
构建了1万行到10万行不等的代码库
about code bases that are 10,000 or 100,000 lines of code.
而微软系统以及Linux系统的代码长度
And that’s still small potatoes compared to the size
长达上百万 上亿万行
of Microsoft Windows or the size
和它们比起来 HACMS系统的代码就不值得一提了
of Linux which are millions, hundreds of millions of lines of code.
但是当你写了1万行或者10万行代码
But when you start to get to 10,000 or 100,000 lines
就会很享受这个过程
of code there are really interesting
因为编出的软件绝对对得起你的辛苦
software artifacts that fit in that size.
就拿编译器和微内核来说
Things like compilers and microkernels,
你可以利用这两个不错的工具
and you can leverage those kinds of exquisite
写出更加复杂的软件系统
artifacts to build much more complex software systems
虽然HACMS系统
where only a small part of the system
仅有一部分内容被证实在功能上是正确的
has to be verified to be functionally correct,
但你可以在其之上运行很多软件 这是没问题的
and then you can have lots of software running on top of it, that isn’t software correct,
虽然不能保证所有软件有同样的安全性
that doesn’t have that same level of assurance associated with it
但是可以确定:这一点无关紧要
but that you can prove: it doesn’t matter what it does,
因为并不会影响到
it’s not going to affect the operation
整个系统的运行
of the overall system.
比如说
So, for example,
HACMS研究员使用了高可信度的代码
HACMS researchers used the high-assurance code and put it on a Boeing
并将之运用于波音无人机上
Unmanned Little Bird which is a
这时候直升飞机完全可以自主飞行
helicopter that can fly completely autonomously or it
或许还可以捎上两个飞行员
can fly with two pilots.
直升机上有两台电脑
And this helicopter has two computers on it:
一台是任务控制电脑
one is the mission control computer that controls
它负责飞机飞往这里然后拍照
things like ‘fly over there and take a picture’ or ‘fly
飞往那里然后拍照
over there and take a picture’, and
并负责与地面站点进行沟通
communicate to the ground station or the operator
然后给直升机下达指令
who’s telling the helicopter what to do.
另一台是飞行控制电脑
It also has a flight control computer that controls things
它负责维持直升机的高度和稳定性
like altitude hold and stability,
并掌握直升机的即刻飞行状况
sort of the mechanics of flying the helicopter at any given time period.
所以研究员使用了seL4微内核
So the researchers put seL4 microkernel,
它是一种已被证实的微内核 能够保证软件运行正常
which is a verified microkernel guaranteed to be functionally correct,
而在任务控制型电脑上
on the mission control computer,
研究员会用微内核来创建不同的软件分区
and they used it to create different software partitions.
而这些分区中的其中一个是负责和地面站点沟通的
So one of those partitions was responsible for communicating with the ground station.
这些分区中还有一个部分是用来
Another one of those partitions was responsible
操控直升机上的相机的
for operating the camera that the helicopter had.
经研究员们核实
The researchers verified that the code
该系统和地面站点进行沟通是完全没问题的
in the ‘communicate with the ground station’ was functionally correct and
和相机控制部分是独立存在的
isolated from the software in the ‘control the camera’ part.
不过用于控制相机的软件并不是新研发的
So the camera part was all the legacy
它早就安在直升飞机上
software that had previously been on the helicopter
用来控制相机操作
to control camera operation.
此外HACMS研究人员在研究中让红队进入该系统
They allowed the red team to additionally put—the
红队的意思就是黑客团队
red team is a group of people who
他们试图黑进并接管直升飞机
are charged with trying to take over control
与合法操作者作对
of the helicopter against the wishes of the legitimate operator—
也就是说黑客们试图
so they’re trying to
侵入并接管直升飞机
hack in, take over control, disrupt the
并扰乱直升飞机的操作
operation of the helicopter.
所以在这个设置中
So in this setting,
红队拥有进入权限
the red team was allowed to have root access, so unfettered access
他们可以无拘无束地出入相机分区
within the camera partition,
而红队的目的就是:冲破一切束缚
and was charged with: break out of this, take over control
接管整架直升飞机
of the rest of the helicopter,
想方设法破坏直升飞机的操作系统
disrupt the operation of the helicopter in any way, corrupt
他们甚至会篡改直升飞机发给地表站点的信息
the messages to the ground station—basically interfere
反正无论如何都要
in any way you can with the legitimate
干扰直升机的运行
operation of this helicopter.
而在源代码方面 红队也有足够的权限
The red team had full access to the source code.
他们理解所有代码的含义
They understood all the design documents.
聪明如你 想必也知道了红队对该系统了如指掌
They knew as much about the system as you could reasonably expect to know.
但是六周后他们仍然束手无策
And after six weeks they were not able to break out.
他们根本没法去扰乱直升飞机的运行
They were not able to disrupt the operation of the copter at all.
他们能做的就是对自己使用叉路炸弹
All they could do was they could fork-bomb themselves.
红队基本上可以攻击自己的进程
They could basically crash their own
但对于直升飞机来说
process but the rest of the helicopter would then
它能清醒地意识到该进程崩溃了 并能重启
notice that that process was crashed and restart it again,
还能继续组织相机操作
restoring the operation of the camera.
这个例子说明了
So that’s an example
你可以使用形式验证技术
of where you could use the formal methods-based techniques to
来创建这种深层次的防卫体系
create this kind of thin level at the bottom,
这就是seL4微内核的用途所在
which was the seL4 microkernel, and then leverage
它可以让直升机正常发挥自己的功能
that to produce the full functionality ofthe helicopter.
黑客会时不时头脑发热地发动攻击
The camera functionality might come and go as hackers break
所以相机的功能可能会出现断断续续的现象
in or don’t break in but you’re guaranteed
但直升机仍然能和地面站点保持交流
that the helicopter will be still able to communicate to the ground
并且平稳地翱翔于蓝天
station and fly appropriately.

发表评论

译制信息
视频概述

美国国防部高级研究计划局开启了一个新项目HACMS(高可信军事网络系统),旨在全方位保护无人机和军事网络系统,使其不受黑客攻击。

听录译者

收集自网络

翻译译者

ABC

审核员

审核员 AF

视频来源

https://www.youtube.com/watch?v=9_dxtq7JtgA

相关推荐