Project 311 (3rd year)
Software Security Verification and Analysis
| The aim of the software security part (311) of iCAST is to develop fundamental and practical solutions to the assurance of software security. Within the wide spectrum of techniques that would constitute such solutions, we have focused on two particular topics: (1) Memory Safety Analysis of Programs with Pointers and (2) 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 automation of the compositional approach to alleviating the state-explosion problem for large systems. Though the techniques we are developing for solving 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. In addition, the separation logic that we apply in the first topic is inherently compositional, a central concept in the second topic. |
| (1) | Memory Safety Analysis: Memory errors in programs, 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 tool we call THOR (Tool for Heap-Oriented Reasoning) for memory safety analysis of C programs (see our CAV 2008 paper). Because of our innovative method for combining shape and arithmetic reasoning, the THOR tool is able to leverage the best numerical tools available. It also features an interactive and graphical display of analysis data that makes it easier for the user to understand these data. Currently, THOR supports analysis of doubly-linked lists. We are developing techniques for more data structures and also extending the tool to support more C features and stronger invariants. |
| (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 a contextual assumption about its environment, and then discharge the assumption on the collection of the rest of the components. In the current paradigm of automated compositional verification via learning, system behaviors and their requirements are typically formalized as (classic) regular languages. Contextual assumptions in the premises of a compositional proof rule are therefore also regular languages and their corresponding finite-state automata can 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-based paradigm to the full class of omega-regular languages (see our TACAS 2008 paper). More recently, for the classic case, we have also made some progress in improving the efficiency. We have developed an algorithm for learning a minimal separating DFA of two disjoint regular languages that requires only a polynomial number of queries and is far more efficient than existing algorithms. The algorithm can be easily adapted to serve as a learning algorithm for automated compositional verification, guaranteeing generation of minimal contextual assumptions. |
Achievements and Contributions
Member List
| Country | Organization | Full Name | Title | |
|---|---|---|---|---|
Taiwan |
TWISC |
Tsay, Yih-Kuen |
PI |
|
Taiwan |
TWISC |
Wang, Bow-Yaw |
Co-PI |
|
Taiwan |
TWISC |
Chuang, Tyng-Ruey |
Co-PI |
|
Taiwan |
TWISC |
Chen, Yu-Fang |
Student |
|
Taiwan |
TWISC |
Tsai, Ming-Hsien |
Student |
|
Taiwan |
TWISC |
Chang, Jinn-Shu |
Student |
|
Taiwan |
TWISC |
Chang, Yi-Wen |
Student |
|
US |
CMU |
Peter Lee |
CPI |
|
US |
CMU |
Ed Clarke |
CPI |
|
US |
CMU |
Stephen Magill |
Student |
|
US |
CMU |
Will Klieber |
Student |
Project 300 Orgnization Chart (in Hanzi)
Required Documents (3rd year)
Self-Assessment Presentation File (Internal Review Meeting)
Midterm Report (External Review Meeting)
Final Report (External Review Meeting)