Information is an important strategic and operational corporate asset, and, therefore, there is a need to have adequate security measures which can safeguard sensitive information. This project targets the development of techniques that are exhaustive and formally guarantee the correctness of security properties of the actual implementation given in a language such as ANSI-C. Model Checking, a perfect candidate to fulfill the task, exhaustively explores the entire state-space for violations of a property of interest.
However, Model Checking suffers from the state-space explosion problem, i.e., the size of the state-space often exceeds the capacity of the Model Checking tool. The main research challenge when applying Model Checking to large-scale software therefore is to address the scalability problem. In this project we tailor state-space reduction algorithms to the code security domain, and thus, develop specialized model checking algorithms for detecting security vulnerabilities.
During the first half of the project we were able to show that focusing on low-level security properties results in a considerable performance gain in static analysis algorithms. This project extends this work to model checking algorithms and subsequent refinement of abstract models. Among the methods we investigate are:
a) performance and precision improvements in alias analysis,
b) abstract counterexample analysis and, based on that, guiding heuristics for model checking algorithms,
c) novel counterexample guided abstraction refinement (CEGAR) algorithms based on new abstract transformers, and
d) extensions to modeling formalisms by introduction of quantified verification conditions and improvements in algorithms for quantified bit-vector arithmetic.