Practical advances in the formal verification of security and safety critical software

据估计，有缺陷的软件每年给世界经济造成1600亿美元的损失。因此，能够帮助提高软件可靠性的努力，即使是以很小的方式，也是值得的。Tony Hoare爵士和其他著名的研究人员最近决定，现在是时候恢复Robert Floyd 1967年的验证编译器（VC）项目了。他们以计算机科学和软件工程的大挑战6 （GC6）的形式重新定义了这个项目，即可靠的系统进化。总而言之，GC6是一项时间尺度为15-20年的国际努力，其主要成果包括：(1)统一的软件分析和构建理论；（ii）验证编译器（VC），一种能够在程序运行之前根据其规格确定其正确性的工具；（iii）工业级应用程序的验证软件储存库（VSR）及其规格。本提案背后的总体研究目标是促进理论、语言、工具和方法的发展，这些可以帮助软件行业更有效地开发高质量的软件。为了实现这一目标，将通过对GC6的贡献来实现，重点是Java建模语言（JML）， Java的行为接口规范语言（BISL），因为Java用于安全性和安全性关键领域，如基于web的企业应用程序（WEAs）和嵌入式设备和控制器（如智能卡）。本提案范围内的具体项目包括：(1)综合运行时断言检查、扩展静态检查、全静态程序验证和模型检查的好处；(2) JML公理化的统一，多证明者支持，并行验证；(3)增强了JML的语言设计和语义基础；(4)行业案例研究。提案中提出的综合进展是新颖的。它们将有助于提高可以使用JML工具进行正式验证的应用程序的规模。

It is estimated that faulty software costs the world economy 160 billion dollars yearly. Hence, efforts that can be made to help improve software reliability, even in a small way, will be worthwhile. Sir Tony Hoare and other eminent researchers recently determined that the "time was right" to revive Robert Floyd's 1967 Verifying Compiler (VC) project. They did so by recasting the project in the form of a Grand Challenge for Computer Science and Software Engineering known as Grand Challenge 6 (GC6), Dependable Systems Evolution. In summary, the GC6 is an international effort with a time scale of 15-20 years whose main deliverables consist of: (i) Unified theory of software analysis and construction; (ii) Verifying Compiler (VC), a tool that can establish the correctness of a program, relative to its specification, before it is run; (iii) Verified Software Repository (VSR) of industrial grade applications and their specifications. The overall research goal behind this proposal is to contribute to the development of theories, languages, tools and methodologies which can help the software industry be more effective at developing quality software. Work towards this goal will be through contributions to the GC6 with a focus on the Java Modeling Language (JML), a Behavioral Interface Specification Language (BISL) for Java because of Java's use in security and safety critical areas such as Web-based Enterprise Applications (WEAs) and embedded devices and controllers (such as smart cards). Specific projects within the scope of this proposal include: (1) compounding the benefits of Runtime Assertion Checking, Extended Static Checking, Full Static Program Verification and Model Checking; (2) unification of JML axiomatizations, mutliprover support, parallel verification; (3) enhancements to the language design and semantic foundation of JML; (4) industrial case studies. The combined advances set forth in the proposal are novel. They will help raise the bar on the size of applications that can be subject to formal verification using JML tools.