欢迎来到 黑吧安全网 聚焦网络安全前沿资讯,精华内容,交流技术心得!

耶鲁大学邵中:操作系统发展拐点已到,我们需要的是“反黑客入侵”的CertiKOS

来源:本站整理 作者:佚名 时间:2017-07-13 TAG: 我要投稿

2017年7月9日,中国计算机学会(CCF)主办、雷锋网与香港中文大学(深圳)承办的第二届全球人工智能与机器人峰会(CCF-GAIR 2017)进入到最后一天的议程。自动驾驶作为人工智能大潮中一个最重要的分支,在这天得到广泛而深入的探讨。

事实上,自动驾驶的各个环节,都不得不面对网络安全问题。来自耶鲁大学的邵中教授,作为计算机程序语言设计的权威专家受邀进行了大会主题演讲,为我们阐述了其正在研发的“反黑客攻击”操作系统CertiKOS背后的理念。
1.
大家都知道,无论是区块链、机器人还是自动驾驶,其核心软件都有一个操作系统操作系统一旦被黑客攻击,上层安全便得不到保证。所以自动驾驶汽车的信息安全问题是一个特别大的挑战。

最近几年,业内发生了很多黑客攻击汽车的案例,他们根本不需要靠近车辆,便可轻松获取十英里外车辆的控制权。这些攻击还不能很快修复,且每年都有发生。此外,勒索病毒、物联网病毒等,一直困扰着那些联网的设备,哪怕只是其中某一部件被攻击,后果也不堪设想。

近来,纽约时报的一篇文章中提到,自动驾驶系统比你见到的手机、电脑的系统更加复杂,其上的联网接口数不胜数,一旦被攻击,不是修复(reboot)一下就了事的,这辆车很可能变成黑客的武器,危及公众安全。
2.
为了从底层来解决这些问题,邵中带领耶鲁大学的团队开启了研发项目,重新设计操作系统——黑客无法进行攻击。
目前,一般的软件出了错,都是用Test的方式来找到Bug的位置,了解其在特定的执行状态和攻击下会有什么状况。如果要解决Bug就不能用Test,唯一能做的就是形式化验证。那么,如何能够用Formal Methods(形式化方法)来验证新的不带Bug的操作系统

所谓Formal Methods,就跟中学里的数学证明一样,一个简单的数学定理要花一页纸,要验证它有什么样的可能性,会不会成功。但是不管它能不能做到,形式化验证要证明这个程序满足它的规范,而且是在任何执行条件下,面对某一类攻击时都不会有错,这是形式化验证要达到的效果。
形式化验证为什么到现在还没有成功应用到商业的各个部门呢?原因主要有这么几类。
第一,写证明要有形式化支持,比如下图是在2009年操作系统大会上,第一个被验证的操作系统内核。有7500行代码,但是光7500行的C语言代码就花了11个人年为其工作,其中还有500行的汇编代码1000多行的C语言代码没有被验证,可以看出工作量非常大。

另外一个问题是,用户平时写C语言代码的时候,究竟对它有多清晰的概念?C语言也不是特别好的语言,一旦要用它来写操作系统最底端的东西,可能就会出现C语言代码、汇编代码以及C语言代码和汇编代码杂交体并存的情况,依赖性很强,一旦这些代码连在一起组成一个复杂的系统,要保证其不出错简直是不可能完成的任务。

除了这个问题以外,所有的操作系统,尤其是现在新的多核的CPU平台上,还有用Concurrency(并发)的,往往有好几个版本,要验证它也非常难。

所以,现在的系统能做到的程度与理想状态还有一个很大的Gap,像IoT、自动驾驶平台这类系统会变得越来越复杂,所以Gap会越拉越大。

[1] [2] [3] [4]  下一页

【声明】:黑吧安全网(http://www.myhack58.com)登载此文出于传递更多信息之目的,并不代表本站赞同其观点和对其真实性负责,仅适于网络安全技术爱好者学习研究使用,学习中请遵循国家相关法律法规。如有问题请联系我们,联系邮箱admin@myhack58.com,我们会在最短的时间内进行处理。
  • 最新更新
    • 相关阅读
      • 本类热门
        • 最近下载