防黑客编程*

阅读量:432
赵永望,冯新宇
PDF在线浏览 下载本文    软件验证规约

软件验证有助于发现漏洞、防止黑客攻击。

在华盛顿大学的医学中心内,放射治疗系统将高能辐射光束射入到病人头中,以治疗患者舌头和食道内的肿瘤。系统中的任何软件都不允许出现错误,任何错误都将是致命的,因此,医学中心的工程师和科学家们进行合作,以确保系统不会失效。一旦规定的配置超出允许范围,高能辐射光束将被立即关闭。

这是通过一种被称为软件验证(software verification)方法实现的。验证关键系统,例如放射治疗装置,正是扎卡里·塔特洛克(Zachary Tatlock)衷的事情。三年前,塔特洛克作为一名博士生在华盛顿大学对他毕业论文课题中关于程序验证的研究作了报告。医学中心放射治疗团队的首席工程师在听众席中询问,如何将验证方法应用到他们的系统中。塔特洛克回想这件事时说到:“这可能帮助我找到了一份工作。”如今,他已成为华盛顿大学计算机科学领域的一名助理教授。他一直与华盛顿大学的其他同事及学生一起,与医学中心的团队开展合作。

软件验证在上述放射治疗系统上应用的挑战在于,该系统由多种语言开发,因此须采用不同的技术来完整地验证软件。整个系统由十多个组件构成,每个组件又有不同的关键等级。

塔特洛克解释说,事件日志软件的关键等级要比辐射功率控制软件的低得多。他认为,“我们希望确保所有模块的可靠性,并确保不存在影响关键部件的软件缺陷。其中有两三个组件是系统的核心,保证它们的正确性显得尤为重要”。

放射治疗系统团队使用了多种验证方法,包括从自动定理证明工具到手工编写,再到经证明辅助工具检查的手工证明等各种有力的验证方法。其中,证明辅助工具是一种检查证明正确性的程序,证明来自某种表达力丰富的逻辑。

防止软件攻击

通常计算机代码的开发不经过任何形式化过程,并且测试代码的主要指标是简单地运行程序,看其是否工作。这种测试,既不能保证覆盖到运行时发生的所有情况,也不能够防止恶意攻击者通过研读程序,设计巧妙的方法对软件进行破坏。形式化软件验证(formal software verification)依赖数学定理和推理,并且使用演绎方法检查系统最关键的部分。支持者相信使用这种技术,可以开发出防止黑客攻击的软件。

“攻击者控制机器和互联网上程序的很多方法是利用安全漏洞,而安全语言对于其中很多类型的漏洞是免疫的,如缓冲区溢出漏洞。”普林斯顿大学计算机科学教授、程序验证领域的专家安德鲁·阿佩尔(Andrew Appel)解释道。

形式化软件验证采用的方法不依赖于程序的运行。它通过分析程序文本来证明在任何可能的输入的情况下程序行为的性质。阿佩尔说,“即使使用所谓的‘安全’语言(如Java编写程序也不一定保证它们就是正确的。它们仍然可能有漏洞并且出错,只是没有什么灾难性的后果。”他强调,安全始终是重要的,但对于系统的关键基础组件,正确性变得至关重要。

此前,安全性已被证明是关键系统的重要问题,并已在多个案例中危及患者的生命。1982年,加拿大原子能有限公司(AECL)生产了Therac-25型放射治疗机。1985~1987年间发生的至少6起事故都与该系统有关。在这些事故中,患者遭受了过量的辐射——有时候比正常值高出数百倍,从而导致患者死亡或者遭受严重伤害。

Therac-25事故的调查结果显示,AECL公司既没有独立审查软件代码,也没有在医院组装系统之前测试系统的软硬件。

“如果要确保程序的正确性,而不仅仅是安全,就需要证明程序是根据某种规约执行的。”阿佩尔说,“必须根据程序输入/输出的相关性,使用形式化方法定义程序的正确性,即规约,然后必须找到一种方法来保证对于任何可能的输入,程序的输出都满足该规约。”

阿佩尔是DeepSpec1研究项目的成员。他在该项目中的职责是检查软件应用程序和硬件的完全功能正确性(full functional correctness),使程序按照预定的方式运行。为了达到该目的,DeepSpec项目正在构建一系列工具,用于验证程序是否符合深度规约(基于形式逻辑和数学给出的细粒度、精确的软件行为的描述),同时验证软件组件(例如操作系统内核)是否符合其深度规约。

会员登录后可下载全文

中国计算机学会(CCF)拥有《中国计算机学会通讯》(CCCF)所刊登内容的所有版权,未经CCF允许,不得转载本刊文字及照片,否则被视为侵权。对于侵权行为,CCF将追究其法律责任。
<<< 上一篇   无
<<< 下一篇 无
读完这篇文章后,您心情如何?

作者介绍

赵永望

  • CCF高级会员
  • 北京航空航天大学副教授
  • 研究方向:形式化方法、操作系统内核等
  • zhaoyw@buaa.edu.cn

冯新宇

  • CCF专业会员
  • 中国科学技术大学教授
  • 研究方向:程序验证、可信操作系统等
  • xyfeng@ustc.edu.cn