Latest news

No news at this moment


Press Release

Commissariat à l’Energie Atomique, France

An Introduction to VeriFast for Java

Jochen Burghardt, Hans Werner Pohl

A Trusted Virtual Security Module

Ronald Toegl, Florian Reimair, Martin Pirker

Work Structure

The work is organised in seven work packages

STANCE - Work Packages


WP1 Security properties and requirements.

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.

WP3 Implementation of C++ and Java analysis tools based on Frama-C and VeriFast.

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 Development of dedicated security analysis plug-ins.

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.

WP5 Development of security applications and verification of use cases

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 Security evaluation and certification

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 Project management, distribution and dissemination.

WP7 addresses the way the resulting platform will be distributed. WP7 also performs management and dissemination activities.