The work is organised in seven work packages
WP1 investigates what are the security properties of the applications and formalizes them to allow their verification. The Frama-C and VeriFast specifications languages, and their extensions built within the project, will be used.
•Research on the security and verification of C++ and Java source code.
WP2 develops a method to parse and represent the C++ and Java source code by means of some intermediate representation language, and to verify the security properties of C, C++ and Java source code. This will lay the theoretical foundations for the security analysis of industrial programs written in C, C++ and Java.
In WP3, new analysers based on the existing Frama-C and VeriFast tools are implemented. Mutualised Java and C++ front-ends will be built. These front-ends will use a common intermediate representation language. The existing back-end analysers (value analysis and weakest-precondition calculus for Frama-C, and the VeriFast separation logic engine) will be extended.
WP4 is the core of the project, namely where specific plug-ins are developed to analyse the security properties gathered in WP1. The resulting source code analysis tools shall be properly integrated in order to work efficiently and seamlessly.
In WP5, security-critical applications are used as use cases for the security analyses, in order to prove their practicability and measure the benefits (in terms of efforts) obtained. Some security use cases, such as the TSS for eTPM, will be developed during the project, and others will be ready made.
WP6 serves different purposes: 1) the security evaluation and assessment of the use-cases w.r.t. their security properties, and 2) the CC certification preparation of the use-cases
WP7 addresses the way the resulting platform will be distributed. WP7 also performs management and dissemination activities.