Specification and automatic verification of security guidelines for program certification

Software engineering processes have grown exponentially in past years in terms of code bases complexity and development team size working on the same project.  As a consequence, building secure software becomes a more and more challenging task, as it requires establishing the mechanisms to protect the software and avoid flaws that can be the source of serious vulnerabilities.
Running tests would not be sufficient to detect errors before the software release, and is rather costly if it requires the end of the development process to be carried out.
Adopting static code analysis and deploying it on the programmers' side would be a wise decision for different reasons. First, running static code analysis on pieces of software does not require the end of the development process, and can be run on a non necessarily complete product. Another advantage of applying static code analysis is that it does not require to run or compile the code, and can be run by the developer when development activities are ongoing. Moreover, locating the source of the detected security flaw can be much faster and more precise.
Using existing static code analysis tools requires a very large expertise by developers to interpret and fix the detected security issues. However, developers should not be security experts, and what is really needed is to provide guidance and help to them when using static code analysis tools. In addition, static code analysis tools are more focused on vulnerability detection, and do not focus on security guidelines verification, as the latter are presented in informal way. This makes their interpretation and implementation difficult for developers.
The goal of this thesis is a framework to help bridging the gap between the informal presentation of security guidelines, and their automatic verification at code level from the programmer point-of-view. The security guidelines that we consider relate to good and bad programming practices, instead of the traditional CIA (Confidentiality, Integrity and Availability) properties.
Integrating the formal specification and automatic verification of security guidelines in the early stages of the development lifecycle is another key objective of this work.
We describe how security guidelines might be captured by security experts and verified formally by developers. Our technique relies on abstracting actions in a program based on modularity, and on combining model checking together with control and information flow analysis. Our goal is to formalize the existing body of knowledge in security best practices using formulas in the Model Checking Language and to conduct formal verification of the conformance of programs with such security guidelines through model checking, and provide precise feedback to the developer.
This PhD work resulted in the design of a tool-chain and its almost complete implementation covering the end-to-end verification of compliance to security guidelines at code level.