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

点击翻译按钮获取中文摘要

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.