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

据估计，有缺陷的软件每年给世界经济造成1600亿美元的损失。因此，努力帮助提高软件可靠性，即使是很小的方式，也是值得的。托尼·霍尔爵士和其他杰出的研究人员最近确定，恢复罗伯特·弗洛伊德1967年的风险投资（VC）项目的“时机已经成熟”。他们以计算机科学和软件工程的大挑战的形式重新设计了这个项目，称为Grand Challenge 6（GC 6），Dependency Systems Evolution。总而言之，GC 6是一项国际努力，时间跨度为15-20年，其主要成果包括：（i）软件分析和构建的统一理论;（ii）验证编译器（VC），一种可以在程序运行之前相对于其规范确定程序正确性的工具;（iii）工业级应用程序及其规范的验证软件存储库（VSR）。该提案背后的总体研究目标是促进理论，语言，工具和方法的发展，以帮助软件行业更有效地开发优质软件。实现这一目标的工作将通过对GC 6的贡献，重点是Java建模语言（JML），这是一种Java行为接口规范语言（BISL），因为Java用于安全和安全关键领域，如基于Web的企业应用程序（WEA）和嵌入式设备和控制器（如智能卡）。本提案范围内的具体项目包括：（1）综合JML断言检查、扩展静态检查、完全静态程序验证和模型检查的优点;（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.