Algebraic Program-Analysis Techniques for Invariant Synthesis
Abstract
The goal of the proposed project is to create tools and techniques for enhancing the reliability of software systems. The aim of the research is to develop improved static-analysis techniques for (i) verifying properties of a program~s behavior, and (ii) finding potential bugs and security vulnerabilities in programs.Static analysis concerns techniques for obtaining information about the run-time behavior of a program without actually running the program on specific inputs. Instead, static-analysis techniques explore a program~s behavior for all possible inputs and all possible states that the program can reach. The trick to make this feasible is to explore the program symbolically and conservatively~ i.e., we analyze the program by manipulating abstract descriptors that represent sets ofbehaviors with the goal of computing an abstract descriptor that includes all possible behaviors of the program (even if it additionally contains impossible ones). The information obtained in this way can be used in verification tools to establish that a program does not exhibit erroneous behavior.The project will further develop the recent unification of work by Zachary Kincaid (Princeton) on compositional recurrence analysis (CRA) with work by Thomas Reps (Wisconsin) on Newtonian program analysis via tensor product (NPA-TP). CRA is essentially a method for analyzing single-procedure programs, but by combining it with NPA-TP, they were able to create an analyzer for multi-procedure programs, called interprocedural CRA (ICRA). The key distinguishing features of ICRA are that (1) is generates invariants in a rich assertional language, allowing ICRA to achieve a low false positive rate, and (2) it is compositional in the sense that it analyzes a program by breaking it into parts, analyzing each part independently, and combining the results, allowing ICRA toscale. The proposed project aims to make fundamental advances in program verification and bug detection by (i) enhancing ICRA so that it can analyze additional kinds of programs, and (ii) applying ICRA to challenging problems, such as side-channel discovery and analysis. The outcomes of the project will be software tools for performing static analysis, which will be made availablefor other researchers to download over the web and use in their own analysis and verification work.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- May 23, 2019
- Source ID
- N000141912318
Entities
People
- Zachary Kincaid
Organizations
- Office of Naval Research
- Trustees of Princeton University
- United States Navy