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

Project Outputs and Outcomes

The main expected and measurable results are the following:

1)   A series of enhancements and breakthroughs for the theoretical security analysis techniques used in the field of software security. At the academic level this will be measured as a series of publications in the fields of Static Analysis, Software Engineering and Debugging, Software Security, and Formal Methods.

2)   The production of the software analysis STANCE toolbox for C99 ISO C, C++03 ISO C++ and Java SE 7 code, of industrial quality. The toolbox will include the Frama-C, VeriFast, and Flinder tools, enhanced with:

  • C++ and Java front ends extending both the Frama-C and VeriFast tools.
  • Extensions dedicated to security analysis using abstract interpretation, and Hoare or separation logics.
  • A dynamic analyser using injection-based white box security testing.

The source code analysis tools will be accompanied by manuals and methodological guidelines tailored for security engineers and software developers. A majority of the software developments will be made available under permissive licenses, compatible with existing tools, and extensible to further evolutions. The STANCE toolbox will demonstrate competitive performance on a priori defined test cases and be quality controlled during its development to achieve a high quality product ready for industrial use.

3)   Three industrial use cases used to refine the platform requirements and validate the STANCE source code analysis tools. Results will be measured against the cost and effectiveness of manual code review on similar code bases. A comparison with industrial in-house ad-hoc techniques will also be performed if possible.

  • In the aeronautic domain one of the very first industrial-size security-critical use case will be verified through a combination of static and dynamic analysis techniques. This use case – an e-maintenance software up-load protocol – will encompass ground-based COTS C++ or Java source code and custom airborne embedded C code.
  • In the network systems domain the second industrial use case is a SSO system that allows a user to access all authorized resources (machines, systems, networks) by authenticating once on the network. The objective of such an SSO application is to propagate the authentication information to various services inside or outside of the network, thus saving the user from providing multiple passwords. Securing this process is consequently critical, to prevent access to unauthorized resources.
  • In the embedded security domain a software stack managing dedicated hardware components will be the third use case. This stack and the underlying hardware (the Trusted Platform Module or TPM) are used to realize trusted computing on a variety of platforms. The STANCE toolbox will be applied to the security verification of selected libraries in the stack, to enable their use in security-critical systems.

4)   An evaluation of the relevance of the STANCE toolbox for preparing and helping  the security certification of an application or software system. This assessment will include a proposal for integration within existing and future normative standards.

5)   An assessment of the project’s social, legal, and economic impact. It will be evaluated by the size of the audience in the project’s dissemination events (attendance to real events and internet traffic to web dissemination tools); we will also monitor the impact of the project’s results in specialized and mainstream media.