中科大-耶鲁高可信软件联合研究中心的研究引起瞩目

发布时间:2011-06-07浏览次数:71

 

  美国《技术评论》(Technology Review)杂志最近评选出2011年度十大新兴技术,“不会崩溃的代码”(Crash-Proof Code)名列其中(见http://www.technologyreview.com/tr10/)。这项技术是指用逻辑推理的方法来进行程序验证,以构造高可信的安全攸关软件。

 

  《技术评论》主要介绍了澳大利亚国家信息与通信技术研究中心(NICTA)2009年完成的对可以实际应用的操作系统内核seL4的验证。它证明了seL4能可靠地运行,绝不会崩溃,并且其运行始终满足对它的安全性质要求,只要该证明的各项前提(又称为信任基,即trusted computing base)得到满足。

 

  系统软件作为直接控制计算硬件系统的基础软件,它本身的缺陷更容易导致整个计算系统的失控。2010年被用来攻击伊朗的大量工业设施,甚至包括伊朗布什尔核电厂的令人闻之色变的“超级蠕虫病毒”Stuxnet就是通过操作系统漏洞开展攻击。该病毒利用Windows操作系统的4个“zero-day attack”,获取系统控制权,然后攻击运行于系统之上的西门子WinCC/PCS 7 SCADA控制软件。攻击成功后,离心机运转速度失控,直至瘫痪。为最大限度达到破坏效果,病毒还同时向监控设备发送伪造的“正常数据”,令监控人员无法及时察觉。构造crash-proof的系统内核则有望从根本上杜绝这一类攻击。

 

  《技术评论》在有关这项技术的报导中提到,从事这方面研究的还有我校冯新宇教授、微软Redmond研究院Chris Hawblitzel研究员和耶鲁大学邵中教授(我校大师讲席教授)。

 

  邵中教授、冯新宇教授和中科大-耶鲁高可信软件联合研究中心的其他研究人员等在2008年也验证了一个小的操作系统内核。虽然该内核仅仅是一个非常小的实验性系统,功能比seL4要少得多,但该验证工作所依赖的信任基比seL4的验证也要小得多,因为它基于一种非常基础的元逻辑并且所有的代码都经过验证,而seL4的底层部分C代码和600行汇编代码并没有验证,属于所依赖的信任基部分(信任基越小,验证工作的可靠性就越高)。

 

  《技术评论》是美国专业的科技商业杂志,创刊于1899年,由麻省理工学院主办,以推介、评析科技创新为宗旨,展示最新科技成果及其商业潜能,内容涉及互联网、通讯、计算机技术、能源、新材料、生物医学和商务科技等领域。

 

  《技术评论》主编Jason Pontin去年6月在广州演讲时说:“几乎每年我们都会选出十大新兴技术。我们认为这些技术能够改变世界,这些技术能够商业化,能够投入到当今市场中,促进市场的发展。… 例如,几年前我们评选出手机,认为它是相当先进的技术,今天大家已看到确有很多人在使用手机。2005年我们选择了合成生物,合成生物今天也在快速发展。”

 

 

 

(中科大-耶鲁高可信软件联合研究中心供稿)