This project intends to increase the level of confidence in software systems deployed in mission-critical environments by providing a comprehensive platform for analyzing various aspects of software correctness. More precisely, it focuses on developing a deductive program transformation framework for automatically generating specialized analyzers for C programs in an aspect-oriented way. In contrast with code analyzers that take arbitrary programs as input, this research will show how to synthesize a code analyzer that is specialized to the program under analysis and the correctness aspect under consideration. Such specialization will open up new vistas for making code analyzers more efficient than is currently possible, as well as providing a platform for experimenting with different program analysis algorithms. The project will lead to the development of a deductive framework for a new class of modal logics. In addition, it will lead to a study of the application of partial evaluation and program transformation techniques for generating efficient program analyzers suited to particular analysis problems. The results of this project will be used to aid open source developers in analyzing their software projects, and to introduce students to mathematically rigorous techniques for reasoning about the correctness of software.
We have been able to accomplish the following tasks in this project 1. Development of a deductive abstraction framework that provides safe approximations of program semantics 2. Implementation of a program transformation framework for weaving in analysis aspects written in FCTL 3. Development of the syntax and semantics of a modal logic VCL (Verification of C Logic) for specifying properties of C programs 4. Implementation of a resolution procedure with constraints 5. Extension and implementation of the program transformation framework for dealing with pointers and arrays and incorporating VCL formulas as analysis aspects 6. An abstraction framework for deriving an abstract resolution procedure and predicting its accuracy and termination 7. Introduction of a logic with a sound and complete proof system for reasoning about C and Java programs with library function calls (model-based static analysis) 8. Preliminary definition of a soft analysis approach for generating unit tests from results of static analysis 9. Development of a language-based abstraction framework 10. Integration of deductive verification in higher order logic with static analysis and a case study of verifying an open source Netgear router using deductive static analysis Our project introduces a new paradigm in analysis of software: on-demand intelligent program analysis. It draws ideas from hitherto unexplored areas of constructive logic and type theory to develop techniques for automatically synthesizing "static program monitors" on-demand from specifications of analysis aspects. These "monitors" accept the "collecting semantics" of the source code as input and decide whether it conforms to the given analysis aspect. In addition, our project helps shift the focus of program analysis from "hunting for shallow application-independent errors" to deeper application-dependent errors". The major discoveries can be summarized in the following bullets 1. Development of a language-based abstraction framework 2. A case study of verifying an open source Netgear router using deductive static analysis. Christopher Steinmuller, an undergraduate student, together with graduate student Zheng Lu, formally verified the conformance of the firmware of Netgear's WNR 3500 L wireless router with RFC 2131 based on which it is designed. This resulted in the world's first router with formally verified router. Formally verified OCAML code for the router firmware was generated automatically. Based on this work, Christopher Steinmuller won an honorable mention in CRA Undergraduate Research award competition, 2011. 3. Analysis of termination and other liveness properties of an imperative program can be reduced to termination proof synthesis for simple loops, i.e., loops with only variable updates in the loop body. Among simple loops, the subset of Linear Simple Loops (LSLs) is particular interesting because it is common in practice and expressive in theory. Existing techniques can successfully synthesize a linear ranking function for an LSL if there exists one. However, when a terminating LSL does not have a linear ranking function, these techniques fail. We describe an automatic method that generates proofs of universal termination for LSLs based on the synthesis of disjunctive ranking relations. The method repeatedly finds linear ranking functions on parts of the state space and checks whether the transitive closure of the transition relation is included in the union of the ranking relations. Our method extends the work of Podelski and Rybalchenko. We have implemented a prototype of the method and have shown experimental evidence of the effectiveness of our method. 4. We combined static analysis techniques with model-based deductive verification using SMT solvers to provide a framework that, given an analysis aspect of the source code, automatically generates an analyzer capable of inferring information about that aspect. The analyzer is generated by translating the collecting semantics of a program to a "marked" formula in first order logic over multiple underlying theories. These assertions constitute the models used by the analyzer. Logical specification of the desired program behavior (rather its negation) is incorporated as a first order logic formula. An SMT-LIB formula solver treats the combined formula as a "constraint" and "solves" it. The solution can be used to identify logical (security) errors in programs. Security properties are represented as constraints and the analysis aims to show that these constraints are respected 5. Three PhD students (including a minority student) supported by the project graduated
