CEA is a French government-funded technological research organisation whose activities range from low-carbon energies to defense and security, from information technologies to health technologies.

Within CEA the LSL laboratory leverages formal methods to ensure fundamental properties of software artifacts. Of particular interest are those pertaining to safety or security.

We share the conviction that innovative, mathematically rigorous analyses are cost-effective means to verify and validate an increasing part of the growing diversity of software-intensive systems.

Our contribution to this evolving state-of-practice takes the form of industrial-strength tools: GATeL, Frama-C and Unisim bring advanced V&V techniques to various classes of digital artifacts.

Offprints
  • Conference paper
  • Pascal Cuoq, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski.
  • Frama-C - A Software Analysis Perspective.
  • SEFM 2012: 233-247.
  • Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software.
  • Journal article
  • Thomas P. Jensen and David Pichardie.
  • Secure the Clones.
  • Logical Methods in Computer Science 8(2) (2012).
  • Exchanging mutable data objects with untrusted code is a delicate matter because of the risk of creating a data space that is accessible by an attacker.
All publications »
The STANCE project

The objective of this FP7 STREP is to drive scientific and technological breakthroughs in the domain of software security. Over three years, STANCE will define, implement and validate a set of program analysis tools capable of verifying the security of complex software systems written in C, C++ and Java.

STANCE proposes to build on existing assets: formal methods, state-of-the-art static and dynamic program analysis tools, security evaluation expertise, and industry-specific knowledge will be used and significantly extended. The resulting program analysis toolbox and supporting methods will increase the trustworthiness and the cost-effectiveness of existing security-oriented processes. These innovations will durably alter the domain of software security assurance, with broad consequences on its legal, societal, and economic aspects.

Project partners yield from France, Germany, Austria, Hungary, and Belgium.