美国《技术评论》（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年我们选择了合成生物，合成生物今天也在快速发展。”
（中科大－耶鲁高可信软件联合研究中心供稿）
