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 objectives

The main technical objectives of the STANCE project are consequently the following:

  1. To classify common security vulnerabilities and characterize how susceptible they are to source code analysis techniques. The formal classification will group vulnerabilities that have common underlying formal models and separate the others. It will highlight potential relationships between safety and security vulnerabilities. The classification will be compared with existing vulnerability classifications such as (MITRE, 2011) or (Microsoft, 2011), and proposed for integration with them.

  2. To specify algorithms for the sound detection of well-defined classes of security threats in source code. This will be achieved by using, extending, and innovating on known techniques for safety-oriented source code analysis, including abstract interpretation, deductive verification, and model-checking. These analyses will be extended with diagnostic capabilities based on model-based diagnosis and counterexamples, and dynamic analysis using fault injection and automatic test case generation. The completion of this objective will provide a theoretical foundation to formally guarantee the absence of security flaws on a given piece of software.

  3. To implement and test these algorithms. Development will produce (a) efficient source code analysis front-ends for the C++ and Java languages; (b) security source code analysis tools. These developments will be validated against a predefined, industrially representative set of small and medium scale test cases. Performance, soundness, and precision will be precisely evaluated, as well as compatibility and integration with pre-existing implementations in safety-oriented partner tools.

  4. To process and check large scale use cases from STANCE’s industrial partners. The source code analysis tools will attempt to detect multiple classes of security defects or guarantee their absence. This will help evaluate the completion of the previous objectives, and serve as a first assessment of the applicability of the STANCE source code analysis tools. Of particular interest will be the adaptation of the tools to the full complexity of industrial software systems. Within STANCE, the evaluation will be instantiated: on e-maintenance software upload protocol, on a Single Sign On (SSO) system application, and on an embedded security library. The results of this objective are intended to serve both as a large-scale benchmark and as a technology transfer vector to the industrial partners. The use cases will also serve as a public showcase for the project.

  5. To foster support for automated software verification, and strengthen the socio-economic repercussions of the produced technological advances. The project will anticipate and influence the evolution of normative security frameworks to include these guarantees as parts of the certification process. From an economic standpoint the developments in STANCE will provide a strategic market differentiator to the companies using these methods, and have a long-term beneficial impact on development and maintenance costs. More generally, STANCE will contribute to the installation of the trust necessary to both the sociological and economical bloom of cyber-technologies in our societies. Part of the STANCE project will contribute to assess this impact.