Detection of Security Flaws and Vulnerabilities by Guided Model Checking

Modern information-driven society has  an obvious need for security measures that can safeguard the storage and transfer of sensitive information. Software is responsible for almost 100% of the data manipulation in the world and, thus, should be placed under particularly strict security control. Unfortunately, writing a program devoid of bugs is still one of the greatest challenges for developers. As a result, low level implementation mistakes lead not only to software malfunction, but also to security breaches.

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. It aims to tailor state-space reduction algorithms to the code security domain in order to develop specialized verification algorithms for detecting security vulnerabilities. In particular this research work resulted in:

  1. An algorithm for loop summarization using abstract transformers [1]that allows for the construction and analysis of loop-free program abstractions with a required level of precision.
  2. Loopfrog: — a static analyzer for ANSI-C programs [2] that applies loop summarization to tackle buffer-overflow vulnerabilities. In a recent version,  Loopfrog is also able to analyze loop termination.
  3. Compositional termination analysis [3]: — a technique to analyze program termination with the help of compositional relations.
  4. New techniques to compute ranking functions for termination analysis, including methods that require solving quantified boolean formulae.

This is a joint project between USI and ETH Zurich, funded by SNSF.

References

  1. Loop Summarization using Abstract Transformers, Kroening, D.; Sharygina, N.; Tonetta, S.; Tsitovich, A.; Wintersteiger, C.M. , 6th International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 5311, Seoul, South Korea, p.111-125, Springer (2008)
  2. Loopfrog: A Static Analyzer for ANSI-C Programs, Kroening, D.; Sharygina, N.; Tonetta, S.; Tsitovich, A.; Wintersteiger, C.M. , The 24th IEEE/ACM International Conference on Automated Software Engineering, Auckland, New Zealand, p.668-670, IEEE Computer Society (2009)
  3. Termination Analysis with Compositional Transition Invariants, Kroening, D.; Sharygina, N.; Tsitovich, A.; Wintersteiger, C.M. , International Conference on Computer-Aided Verification (CAV), Edinburgh, UK, p.89-103, Springer (2010)