One of the objectives of the SecureChange project is the development of verification techniques for evolving systems, with a strong focus on the development time and run time phases of the software lifecycle. This includes the development of programming models that can ensure the absence of classes of vulnerabilities. A programming model consists of a set of programming guidelines designed to avoid a specific class of vulnerabilities. Source code annotations make the programming model explicit, and can support formal verification of compliance with the programming model.
Read on in the D6.1 Programming model and annotations report.