Automated Invariant Discovery for Efficient Security Checks
Responsabile del progetto all'USI: Natasha Sharygina
Data di inizio: 1 Ottobre 2009
Durata: 36 mesi
- Facoltà di scienze informatiche
- Hasler Foundation
If someone is looking to perform a program verification task today, the most probable candidate will be model checking, the technique allows exhaustive exploration of the entire state-space for violations of a property of interest. However, it suffers from the state-space explosion problem, i.e., the size of the state-space often exceeds the capacity of the tool. Therefore, the main research challenge when applying model checking to large-scale software is to address the scalability problem. A possible answer is program abstraction an approach to construction of program models that preserve important properties of the original program. A number of abstraction methods are already known, however none by itself is sufficiently good for a sound and efficient analysis of large-scale software.
The main difficulty is evident: modern programs are large and operate huge sets of data; that all should be accurately (i.e. precisely and scalably) handled by the abstraction technique.
In our earlier work we build program abstractions, which are driven by the property domains.
In particular, by doing loop summarization we tackle the key problem: infinite program fragments such as loops or recursive functions should be represented by a finite summary. It is crucial to have such summaries both small and precise in representing the semantics of the original program fragment. Construction of abstract domains manually is an art. This project targets this problem and focuses on the automated invariant generation for abstract summaries. In particular, we investigate the following methods:
- Invariant generation using automatic assertions and congruence equations for the loops;
- Iterative strengthening of loop invariants.
Alongside, we study the effective representation of the loop invariants in terms of fast-decidable theories including quantified ones. That enables more compact summaries and faster assertion checks of the summarized program.