Kickoff @ CMU (2008.08.20)
Project 311 (2nd year)
Software Security Verification and Analysis
| The goal of this project is to develop methods and tools, based on sound mathematical foundations, for the verification and analysis of software security properties. We have selected two topics as our current focuses: Memory Safety of Programs and Automated Compositional Verification. The first topic concerns the problem of locating memory errors that are often a cause of security vulnerabilities, while the second investigates a compositional approach to alleviating the state-explosion problem for large systems. Though the solutions we seek to the two problems are quite different, they share one common principle, namely the combination of algorithmic and deductive techniques, which has been an important trend in the general area of formal verification. |
| (1) | Memory Safety of Programs: Memory errors such as dereferencing of dangling pointers and buffer overflows are a common cause of security vulnerabilities. Techniques exist to locate such vulnerabilities and, in the case where these vulnerabilities are not present, to prove their absence. However, these techniques generally have trouble scaling to real-world software. Two common problems include the exponential nature of the program state space and a lack of support for the full range of data structures and operations used in real-world programs. We have addressed the first issue by developing shape analysis techniques based on separation logic, which has better scalability properties than more classical program logics. We have made progress on the second issue by developing a method for combining shape analysis and arithmetic reasoning, which permits the analysis of programs that perform both data structure and arithmetic operations. Support for such operations is important in order to provide hard guarantees about the safety and security of software systems. We have implemented these techniques in a program analysis tool we call THOR (Tool for Heap-Oriented Reasoning). |
| (2) | Automated Compositional Verification: Compositional verification is an effective technique for addressing the state-explosion problem in Model Checking. Most compositional techniques advocate proving properties of a system by checking properties of its components in an assume-guarantee style. The essential idea is to model check each component independently by making an assumption about its environment, and then discharge the assumption on the collection of the rest of the components. In the paradigm of automated compositional reasoning via learning, system behaviors and their requirements are formalized as regular languages. Assumptions in the premises of a compositional proof rule are often regular languages and their corresponding finite-state automata can therefore be generated by learning techniques for regular languages. All existing algorithms fall short when it comes to learning assumptions which involve liveness properties. We have discovered an algorithm that fills this gap and extends the learning paradigm to the full class of omega-regular languages. |
Member List
| Country | Organization | Full Name | Title | |
|---|---|---|---|---|
Taiwan |
TWISC |
Tsay, Yih-Kuen |
PI |
|
Taiwan |
TWISC |
Chuang, Tyng-Ruey |
Co-PI |
|
Taiwan |
TWISC |
Wang, Bow-Yaw |
Co-PI |
|
Taiwan |
TWISC |
Max Schaefer |
Assistant |
|
Taiwan |
TWISC |
Chen, Yu-Fang |
Assistant |
|
Taiwan |
TWISC |
Tsai, Ming-Hsien |
Student |
|
US |
CMU |
Peter Lee |
CPI |
|
US |
CMU |
Ed Clarke |
CPI |
|
US |
CMU |
Frank Pfenning |
Professor |
|
US |
CMU |
Robert Harper |
Professor |
Project 300 Orgnization Chart (in Hanzi)
Required Documents (2nd year)
Self-Assessment Presentation File (Internal Review Meeting)
Midterm Report (External Review Meeting)
Final Report (External Review Meeting)