Collaborative Research: Advanced Static-Analysis Techniques for Ensuring Reliable Software

University Of Massachusetts Amherst, Amherst MA

Investigators

Abstract

This research aims to create techniques for enhancing the reliability of software systems -- a problem that is hugely valuable in today's computerized society. The goal is to develop improved techniques for (i) verifying properties of a program's behavior, and (ii) finding potential bugs and security vulnerabilities. The project will develop static-analysis techniques, which obtain information about the possible states that a program passes through during execution (but without running the program on specific inputs). Instead, all possible inputs are considered, and all possible reachable states are explored. The trick to making this feasible is to run the program on descriptors that represent multiple states. The project will extend the Three-Valued Logic Analyzer (TVLA), a tool for analyzing programs that allocate and deallocate memory and destructively update pointers. These actions are essential in most modern programming languages, but are extremely difficult to analyze. TVLA uses finite three-valued logical structures to model the possibly infinite set of states that such programs can reach. The goals of this research are (i) to develop methods for allowing TVLA to combine analyses of sub-programs, which would allow the creation of reusable summaries of library functions; (ii) to develop symbolic methods, such as decision procedures for logic fragments, that interpret three-valued models as precisely as possible; and (iii) to apply these techniques to analyze low-level assembly code.