Latest news

Stance Press Release

 

07/09/2016: Please click here to read the press release!

Read More

Frama-C Day 2016

 

In a society driven by information technologies and communication, the safety and security of software have become crucial challenges. Frama-C is a software analysis platform that enables the design, implementation, and dissemination of formal verification solutions.

Speakers at the Frama-C Day will demonstrate and discuss innovative approaches to software analysis, from both academic and industrial points of views.

In addition to invited presentations, this will be a space for community discussions, updates on new developments, and upcoming projects.

Click here for more details

Read More

Publications

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.