Publications

Frama-C Framework

Manuals

Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze, Virgile Prevosto, Armand Puccetti, Julien Signoles, Boris Yakobowski
Frama-C User Manual [link] [BibTeX]
@manual{frama_c_user_manual,
title = "Frama-C User Manual",
author = "Correnson, Loïc and Cuoq, Pascal and Kirchner, Florent and Maroneze, André and Prevosto, Virgile and Puccetti, Armand and Signoles, Julien and Yakobowski, Boris",
url = "http://frama-c.com/download/frama-c-user-manual.pdf",
}
The manual introducing common features to all analyzers.
Julien Signoles, Thibaud Antignac, Loïc Correnson, Matthieu Lemerre, Virgile Prevosto
Frama-C Plug-in Development Guide [link] [BibTeX]
@manual{developer_manual,
title = "Frama-C Plug-in Development Guide",
author = "Signoles, Julien and Antignac, Thibaud and Correnson, Loïc and Lemerre, Matthieu and Prevosto, Virgile",
url = "http://frama-c.com/download/frama-c-plugin-development-guide.pdf",
}
The manual for developing a Frama-C plug-in.
Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, Virgile Prevosto
ACSL: ANSI/ISO C Specification Language [link] [BibTeX]
@manual{acsl_reference,
title = "ACSL: ANSI/ISO C Specification Language",
author = "Baudin, Patrick and Filliâtre, Jean-Christophe and Marché, Claude and Monate, Benjamin and Moy, Yannick and Prevosto, Virgile",
url = "http://frama-c.com/download/acsl.pdf",
}
The reference manual of ACSL, the specification language used by Frama-C.

Foundational

Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles, Nicky Williams
The Dogged Pursuit of Bug-Free C Programs: The Frama-C Software Analysis Platform [link]
In Communications of the ACM, Vol. 64, No. 8, 2021

The C programming language is a cornerstone of computer science. Designed by Dennis Ritchie and Ken Thompson at Bell Labs as a key element of Unix engineering, it was rapidly adopted by system-level programmers for its portability, efficiency, and relative ease of use compared to assembly languages. Nearly 50 years after its creation, it is still widely used in software engineering.

Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski
Frama-C, A Software Analysis Perspective [link]
In Formal Aspects of Computing, vol. 27 issue 3, 2015

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. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.

Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, Boris Yakobowski
Frama-C, A Software Analysis Perspective
In Proceedings of International Conference on Software Engineering and Formal Methods 2012 (SEFM), 2012
This paper presents a synthetic view of Frama-C, its main and composite analyses, and some of its industrial achievements.

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. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.

About the Frama-C Kernel

Julien Signoles
Software Architecture of Code Analysis Frameworks Matters: The Frama-C Example [link]
In Formal Integrated Development Environment (F-IDE), 2015
This papers presents the Frama-C architecture and discusses its design choices.

Implementing large software, as software analyzers which aim to be used in industrial settings, requires a well-engineered software architecture in order to ease its daily development and its maintenance process during its lifecycle. If the analyzer is not only a single tool, but an open extensible collaborative framework in which external developers may develop plug-ins collaborating with each other, such a well designed architecture even becomes more important.

In this experience report, we explain difficulties of developing and maintaining open extensible collaborative analysis frameworks, through the example of Frama-C, a platform dedicated to the analysis of code written in C. We also present the new upcoming software architecture of Frama-C and how it aims to solve some of these issues.

Loïc Correnson, Julien Signoles
Combining Analyses for C Program Verification [link]
In Proceedings of International Workshop on Formal Methods for Industrial Critical Systems (FMICS), 2012
This paper explains how Frama-C combines several partial results coming from its plug-ins into a fully consolidated validity status for each program property.

Static analyzers usually return partial results. They can assert that some properties are valid during all possible executions of a program, but gener-ally leave some other properties to be verified by other means. In practice, it is common to combine results from several methods manually to achieve the full verification of a program. In this context, Frama-C is a platform for analyzing C source programs with multiple analyzers. Hence, one analyzer might conclude about properties assumed by another one, in the same environment. We present here the semantical foundations of validity of program properties in such a con-text. We propose a correct and complete algorithm for combining several partial results into a fully consolidated validity status for each program property. We illustrate how such a framework provides meaningful feedback on partial results.

Pascal Cuoq, Damien Doligez, Julien Signoles
Lightweight Typed Customizable Unmarshaling [link]
In Workshop on ML, 2011
This short paper presents how Frama-C unmarshal its data.

The contribution of this work is threefold. First, we offer an OCaml unmarshaling algorithm that uses a lightweight type-directed description of the expected structure of data to make consistency checks. The second contribution is the opportunity to specify functions to be systematically applied on values as they are being unmarshaled. Our third contribution is a type-safe layer for these functions and for the unmarshaling algorithm itself.

Pascal Cuoq, Julien Signoles, Patrick Baudin, Richard Bonichon, Géraud Canet, Loïc Correnson, Benjamin Monate, Virgile Prevosto, Armand Puccetti
Experience Report: OCaml for an Industrial-Strength Static Analysis Framework [link]
In International Conference of Functional Programming (ICFP), 2009
This experience report describes the choice of OCaml as the implementation language for Frama-C.

This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources…) but could have prevented the use of OCaml for this project if they had been missing.

Julien Signoles
Comment un chameau peut-il écrire un journal ?
In Journées Francophones des Langages Applicatifs (JFLA), 2014
In French. Presentation of the journalization mechanism of Frama-C.

Dans Frama-C, plate-forme d’analyse de code C développée en OCaml, un journal est un script OCaml généré automatiquement et permettant de reproduire les actions utilisateurs, notamment effectuées via l’interface utilisateur. Outre la reproductibilité des résultats qui est nécessaire dans un contexte industriel soumis à des exigences de certication fortes comme la norme avionique DO-178C, un journal permet d’automatiser le pilotage de l’outil dans un contexte d’utilisation particulier. Cet article présente comment le mécanisme de génération du journal de Frama-C, appelé journalisation et requérant intrinsèquement de l’introspection, a été développé en OCaml, en combinant typage statique et dynamique.

Julien Signoles
Une bibliothèque de typage dynamique en OCaml
In Journées Francophones des Langages Applicatifs (JFLA), 2011
In French. Presentation of the Frama-C library for dynamic typing and its usage.

Cet article présente une bibliothèque OCaml fournissant une représentation dynamique des types monomorphes, y compris pour les instances des types polymorphes et les types de données abstraits. Elle permet ainsi de voir les types OCaml comme des citoyens de première classe. Elle comble aussi le fossé séparant OCaml des langages dynamiques en mêlant vérifications statiques et dynamiques des types. Nous nous concentrons ici sur le coeur de son implantation, ses propriétés théoriques et l’usage qui en est fait dans Frama-C, plateforme logicielle libre d’analyse statique de programmes C au sein de laquelle cette bibliothèque est distribuée.

Julien Signoles
Foncteurs impératifs et composés: la notion de projets dans Frama-C
In Journées Francophones des Langages Applicatifs (JFLA), 2009
In French. Presentation of the Frama-C library providing its notion of projects.

This article describes the library of projects embedded in Frama-C, which is an extensible platform dedicated to development of source-code analysis of C software. Through this presentation, we detail an original aspect of ML functors which uses their imperative and compositional parts. That is the only well-typed way to implement the required functionality. Furthermore we show a singular example of a hugely-applied functor. This article also introduces the Frama-C platform through one of its main features, the notion of project.

About the Frama-C Graphical User Interface

Loïc Correnson
Ivette: A Modern GUI for Frama-C [link]
In Formal Integrated Development Environment (F-IDE), 2022
This papers presents the Frama-C Ivette GUI and discusses its design choices.

Using a static analyzer such as Frama-C is known to be difficult, even for experienced users. Building a comfortable user interface to alleviate those difficulties is however a complex task that requires many technical issues to be handled that are outside the scope of static analyzers techniques. In this paper, we present the design directions that we have chosen for completely refactoring the old Graphical User Interface of Frama-C within the ReactJS framework. In particular, we discuss middleware and language issues, multithreaded client vs batch analyzer design, synchronization issues, multiple protocol support, plug-in integration, graphical and user-interaction techniques and how various programming language traits scale (or not) for such a development project.

Tutorials

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
A Lesson on Verification of IoT Software with Frama-C [link]
In International Conference on High Performance Computing & Simulation (HPCS), 2019

This paper is a tutorial introduction to Frama-C, a framework for the analysis and verification of sequential C programs, and in particular its EVA, WP, and E-ACSL plugins. The examples are drawn from Contiki, a lightweight operating system for the Internet of Things.

Nikolai Kosmatov, Julien Signoles
Frama-C, a Collaborative Framework for C Code Verification. Tutorial Synopsis [link]
In International Conference on Runtime Verification (RV), 2016

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 and dynamic analysis for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel, and their compliance to a common specification language, ACSL.

This paper presents a three-hour tutorial on Frama-C in which we provide a comprehensive overview of its most important plug-ins: the abstract-interpretation based plug-in Value, the deductive verification tool WP, the runtime verification tool E-ACSL and the test generation tool PathCrawler. We also emphasize different possible collaborations between these plug-ins and a few others. The presentation is illustrated on concrete examples of C programs

Virgile Prevosto
Frama-C tutorial
In STANCE Project, 2013
David Mentré
Practical introduction to Frama-C [link]
In Mitsubishi Electric R&D Centre Europe, 2013

Examples

Plug-ins distributed with Frama-C

Eva, an Evolved Value Analysis

Manuals

David Bühler, Pascal Cuoq, Boris Yakobowski
Eva - The Evolved Value Analysis plug-in [link] [BibTeX]
@manual{eva_user_manual,
title = "Eva - The Evolved Value Analysis plug-in",
author = "Bühler, David and Cuoq, Pascal and Yakobowski, Boris",
url = "http://frama-c.com/download/frama-c-eva-manual.pdf",
}

Theses

David Bühler
EVA, an Evolved Value Analysis for Frama-C: structuring an abstract interpreter through value and state abstractions [link] [BibTeX]
@phdthesis{2017_thesis_buhler,
title = "EVA, an Evolved Value Analysis for Frama-C: structuring an abstract interpreter through value and state abstractions",
author = "Bühler, David",
year = "2017",
url = "http://www.theses.fr/2017REN1S016",
school = "University of Rennes 1",
}
University of Rennes 1, PhD Thesis, 2017

Foundational

Sandrine Blazy, David Bühler, Boris Yakobowski
Structuring Abstract Interpreters Through State and Value Abstractions [link]
In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2017
Formalization of the communication mechanism between abstractions in EVA.

We present a new modular way to structure abstract interpreters. Modular means that new analysis domains may be plugged-in. These abstract domains can communicate through different means to achieve maximal precision. First, all abstractions work cooperatively to emit alarms that exclude the undesirable behaviors of the program. Second, the state abstract domains may exchange information through abstractions of the possible value for expressions. Those value abstractions are themselves extensible, should two domains require a novel form of cooperation. We used this approach to design EVA, an abstract interpreter for C implemented within the Frama-C framework. We present the domains that are available so far within EVA, and show that this communication mechanism is able to handle them seamlessly.

Richard Bonichon, Pascal Cuoq
A Mergeable Interval Map [link]
In Journées Francophones des Langages Applicatifs (JFLA), 2011

This article describes an efficient persistent mergeable data structure for mapping intervals to values. We call this data structure rangemap. We provide an example of application where the need for such a data structure arises (abstract interpretation of programs with pointer casts). We detail different solutions we have considered and dismissed before reaching the solution of rangemaps. We show how they solve the initial problem and eventually describe their implementation.

Others

Géraud Canet, Pascal Cuoq, Benjamin Monate
A Value Analysis for C Programs
In Proceedings of the Ninth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM), 2009
Presentation of a former version of Eva.

We demonstrate the value analysis of Frama-C. Frama-C is an Open Source static analysis framework for the C language. In Frama-C, each static analysis technique, approach or idea can be implemented as a new plug-in, with the opportunity to obtain information from other plug-ins, and to leave the verification of difficult properties to yet other plug-ins. The new analysis may in turn provide access to the data it has computed. The value analysis of Frama-C is a plug-in based on abstract interpretation. It computes and stores supersets of possible values for all the variables at each statement of the analyzed program. It handles pointers, arrays, structs, and heterogeneous pointer casts. Besides producing supersets of possible values for the variables at each point of the execution, the value analysis produces run-time-error alarms. An alarm is emitted for each operation in the analyzed program where the value analysis cannot guarantee that there will not be a run-time error.

Pascal Cuoq, Damien Doligez
Hashconsing in an incrementally garbage-collected system: a story of weak pointers and hashconsing in OCaml 3.10.2
In Workshop on ML, 2008
This article describes weak pointers, weak hashtables and hashconsing as implemented in OCaml and used in a former version of Eva.

This article describes the implementations of weak pointers, weak hashtables and hashconsing in version 3.10.2 of the Objective Caml system, with focus on several performance pitfalls and their solutions.

WP

Manuals

Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye, Allan Blanchard
WP Plug-in Manual [link] [BibTeX]
@manual{wp_user_manual,
title = "WP Plug-in Manual",
author = "Baudin, Patrick and Bobot, François and Correnson, Loïc and Dargaye, Zaynah and Blanchard, Allan",
url = "http://frama-c.com/download/frama-c-wp-manual.pdf",
}
The official manual for the WP plug-in.

Foundational

Loïc Correnson
Qed. Computing What Remains to Be Proved. [link]
In NASA Formal Methods (NFM), 2012
Presentation of Qed, a core library of WP that simplifies proof obligations before sending them to provers.

We propose a framework for manipulating in a efficient way terms and formulæ in classical logic modulo theories. Qed was initially designed for the generation of proof obligations of a weakest-precondition engine for C programs inside the Frama-C framework, but it has been implemented as an independent library. Key features of Qed include on-the-fly strong normalization with various theories and maximal sharing of terms in memory. Qed is also equipped with an extensible simplification engine. We illustrate the power of our framework by the implementation of non-trivial simplifications inside the Wp plug-in of Frama-C. These optimizations have been used to prove industrial, critical embedded softwares.

Tutorials

Allan Blanchard
Introduction to C Program Proof with Frama-C and its WP plug-in [link]
A comprehensive tutorial on how to prove C programs with Frama-C and WP.
Jens Gerlach, Denis Efremov, Tim Sikatzki
ACSL by Example [link]
A fairly complete tour of ACSL and WP features through various functions inspired from C++ STL.

GitHub repository

Virgile Prevosto
Frama-C WP tutorial [link]
In Laboratoire d'Informatique Fondamentale d'Orléans, 2014
A tutorial about the Frama-C plug-in WP.

LIFO’s website

Annotated files

Virgile Prevosto, Nikolay Kosmatov, Julien Signoles
Specification and Proof of Programs with Frama-C [link]
In Integrated Formal Methods (iFM), 2013
A tutorial about the Frama-C plug-in WP.

Despite the spectacular progress made by the developers of formal verification tools, their usage remains basically reserved for the most critical software. More and more engineers and researchers today are interested in such tools in order to integrate them into their everyday work. This half-day tutorial proposes a practical introduction during which the participants will write C program specifications, observe the proof results, analyze proof failures and fix them. Participants will be taught how to write a specification for a C program, in the form of function contracts, and easily prove it with an automatic tool in Frama-C, a freely available software verification toolset. Those who will have Frama-C installed (e.g. from ready-to-install packages frama-c, why, alt-ergo under Linux) will also run automatic proof of programs on their computer. Program specifications will be written in the specification language ACSL similar to other specification languages like JML that some participants may know. ACSL-syntax is intentionally close to C and can be easily learned on-the-fly.

Annotated files

Others

Pascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto
Functional Dependencies of C Functions via Weakest Pre-Conditions [link]
In International Journal on Software Tools for Technology Transfer (STTT), 2011

We present functional dependencies, a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool.

E-ACSL

Manuals

Julien Signoles, Basile Desloges, Kostyantyn Vorobyov
E-ACSL User Manual [link] [BibTeX]
@manual{e_acsl_user_manual,
title = "E-ACSL User Manual",
author = "Signoles, Julien and Desloges, Basile and Vorobyov, Kostyantyn",
url = "http://frama-c.com/download/e-acsl/e-acsl-manual.pdf",
}
The official manual of the Frama-C plug-in E-ACSL.
Julien Signoles
E-ACSL: Executable ANSI/ISO C Specification Language [link] [BibTeX]
@manual{e_acsl_reference,
title = "E-ACSL: Executable ANSI/ISO C Specification Language",
author = "Signoles, Julien",
url = "http://frama-c.com/download/e-acsl/e-acsl.pdf",
}
The reference manual of the E-ACSL specification language.

Theses

Dara Ly
Formalisation d'un vérificateur dynamique de propriétés mémoire pour programmes C [link] [BibTeX]
@phdthesis{2022_ly_phd,
title = "Formalisation d'un vérificateur dynamique de propriétés mémoire pour programmes C",
author = "Ly, Dara",
year = "2022",
url = "https://www.theses.fr/s265339",
school = "University of Orléans",
}
University of Orléans, PhD Thesis, 2022

Runtime Assertion Checking is a program verification technique allowing to monitor programs during their execution, in order to check their validity with respect to some specification expressed as assertions, that is, formal annotations inserted in the source code. Assertions are translated into executable code through a process called instrumentation, thus implementing an inline monitor for the program. During execution, the monitor checks whether the program complies with its assertions, and aborts the execution in case of violation of an assertion. If no such violation occurs, the program’s functional behavior is unchanged. Instrumenting a program is a process whose implementation complexity is strongly related to the expressiveness of the annotation language. For C programs, the E-ACSL plugin of Frama-C, an open-source analysis platform for C programs, can express properties related to the memory state of the program, at the cost of a complex instrumentation. In this thesis, we present a formalization of the instrumentation process, that is, a description accurate enough to enable formal reasoning about the semantic properties of the instrumentation. The problem is modeled as a translation, from a source language with logical assertions, to a target language. The latter has no logical assertions, instead featuring a data-structure we call observation memory, which is designed to keep track of memory properties. We present an axiomatic characterization of observation memory, and use it to define the translation’s target language semantics. The translation is then proved correct with regards to the respective semantics of source and target languages. In addition, we study an optimization of the instrumentation through data-flow analysis. This optimization is implemented in E-ACSL in order to mitigate the performance costs of the instrumentation. The analysis aims at identifying a minimal subset of memory locations, whose instrumentation suffices for the monitor to evaluate the program’s assertions soundly. We define such an analysis and prove its soundness, meaning that restricting the instrumentation to memory locations computed by the analysis does not threaten the validity of the monitor’s verdicts.

Julien Signoles
From Static Analysis to Runtime Verification with Frama-C and E-ACSL [link] [BibTeX]
@phdthesis{2018_thesis_signoles,
title = "From Static Analysis to Runtime Verification with Frama-C and E-ACSL",
author = "Signoles, Julien",
year = "2018",
url = "https://julien-signoles.fr/publis/hdr.pdf",
school = "University of Paris Sud",
}
University of Paris Sud, Habilitation Thesis, 2018

Foundational

Nikolai Kosmatov, Fonenantsoa Maurica, Julien Signoles
Efficient Runtime Assertion Checking for Properties over Mathematical Numbers [link]
In International Conference on Runtime Verification (RV), 2020

Runtime assertion checking is the discipline of detecting at runtime violations of program properties written as formal code annotations. These properties often include numerical properties, which may rely on either (bounded) machine representations or (unbounded) mathematical numbers. The verification of the former is easier to implement and more efficient at runtime, while the latter are more expressive and often more adequate for writing specifications. This short paper explains how the runtime assertion checker E-ACSL reconciles both approaches by presenting a type system that allows the tool to generate efficient machine-number based code when it is safe to do so, while generating arbitrary-precision code when it is necessary. This type system and the code generator not only handle integers but also rational arithmetics. As far as we know, it is the first runtime verification tool that supports the verification of properties over rational numbers.

Julien Signoles, Nikolai Kosmatov, Kostyantyn Vorobyov
E-ACSL, a Runtime Verification Tool for Safety and Security of C Programs. Tool Paper. [link]
In International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools (RV-CuBES), 2017
An overview of the E-ACSL plug-in.

This tool paper presents E-ACSL, a runtime verification tool for C programs capable of checking a broad range of safety and security properties expressed using a formal specification language. E-ACSL consumes a C program annotated with formal specifications and generates a new C program that behaves similarly to the original if the formal properties are satisfied, or aborts its execution whenever a property does not hold. This paper presents an overview of E-ACSL and its specification language.

Kostyantyn Vorobyov, Julien Signoles, Nikolai Kosmatov
Shadow state encoding for efficient monitoring of block-level properties [link]
In International Symposium on Memory Management (ISMM), 2017
Presentation of the shadow memory technique used by E-ACSL to monitor memory properties.

Memory shadowing associates addresses from an application’s memory to values stored in a disjoint memory space called shadow memory. At runtime shadow values store metadata about application memory locations they are mapped to. Shadow state encodings – the structure of shadow values and their interpretation – vary across different tools. Encodings used by the state-of-the-art monitoring tools have been proven useful for tracking memory at a byte-level, but cannot address properties related to memory block boundaries. Tracking block boundaries is however crucial for spatial memory safety analysis, where a spatial violation such as out-of-bounds access, may dereference an allocated location belonging to an adjacent block or a different struct member.

This paper describes two novel shadow state encodings which capture block-boundary-related properties. These encodings have been implemented in E-ACSL - a runtime verification tool for C programs. Initial experiments involving checking validity of pointer and array accesses in computationally intensive runs of programs selected from SPEC CPU benchmarks demonstrate runtime and memory overheads comparable to state-of-the-art memory debuggers.

Michaël Delahaye, Nikolai Kosmatov, Julien Signoles
Common Specification Language for Static and Dynamic Analysis of C Programs [link]
In Proceedings of Symposium on Applied Computing (SAC), 2013
An overview of the specification language.

Various combinations of static and dynamic analysis techniques were recently shown to be beneficial for software verification. A frequent obstacle to combining different tools in a completely automatic way is the lack of a common specification language. Our work proposes to translate a Pre-Post based specification into executable C code. This paper presents e-acsl, subset of the acsl specification language for C programs, and its automatic translator into C implemented as a Frama-C plug-in. The resulting C code is executable and can be used by a dynamic analysis tool. We illustrate how the PathCrawler test generation tool automatically treats such pre- and postconditions specified as C functions.

Tutorials

Nikolai Kosmatov, Julien Signoles
A Lesson on Runtime Assertion Checking with Frama-C [link]
In International Conference on Runtime Verification (RV), 2013
A tutorial about the Frama-C plug-in E-ACSL.

Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. This paper provides a lesson on runtime assertion checking with Frama-C, a publicly available toolset for analysis of C programs. We illustrate how a C program can be specified in executable specification language E-ACSL and how this specification can be automatically translated into instrumented C code suitable for monitoring and runtime verification of specified properties. We show how various errors can be automatically detected on the instrumented code, including C runtime errors, failures in postconditions, assertions, preconditions of called functions, and memory leaks. Benefits of combining runtime assertion checking with other Frama-C analyzers are illustrated as well.

Others

Thibaut Benjamin, Felix Ridoux, Julien Signoles
Formalisation d'un vérificateur efficace d'assertions arithmétiques à l'exécution [link]
In Journées Francophones des Langages Applicatifs (JFLA), 2022
In French

La vérification d’assertions à l’exécution est une technique consistant à vérifier la validité d’annotations formelles pendant l’exécution d’un programme. Bien qu’ancienne, cette technique reste encore peu étudiée d’un point de vue théorique. Cet article contribue à pallier ce manque en formalisant un vérificateur d’assertions à l’exécution pour des propriétés arithmétiques entières. La principale difficulté réside dans la modélisation d’un générateur de code pour les propriétés visées qui génère du code à la fois correct et efficace. Ainsi, le code généré repose sur des entiers machines lorsque le générateur peut prouver qu’il est correct de le faire et sur une bibliothèque spécialisée dans l’arithmétique exacte, correcte mais moins efficace, dans les autres cas. Il utilise pour cela un système de types dédié. En outre, la logique considérée pour les propriétés inclue des constructions d’ordre supérieur. L’article présente également une implémentation de ce générateur de code au sein d’E-ACSL, le greffon de Frama-C dédié à la vérification d’assertions à l’exécution, ainsi qu’une première évaluation expérimentale démontrant empiriquement l’efficacité du code généré.

Julien Signoles
The E-ACSL Perspective on Runtime Assertion Checking [link]
In International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX), 2021

Runtime Assertion Checking (RAC) is the discipline of verifying program assertions at runtime, i.e. when executing the code. Nowadays, RAC usually relies on Behavioral Interface Specification Languages (BISL) à la Eiffel for writing powerful code specifications. Since now more than 20 years, several works have studied RAC. Most of them have focused on BISL. Some others have also considered combinations of RAC with others techniques, e.g. deductive verification (DV). Very few tackle RAC as a verification technique that soundly generates efficient code from formal annotations. Here, we revisit these three RAC’s research areas by emphasizing the works done in E-ACSL, which is both a BISL and a RAC tool for C code. We also compare it to others languages and tools.

Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, Julien Signoles
Runtime abstract interpretation for numerical accuracy and robustness. [link]
In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2021

Verification of numerical accuracy properties in modern software remains an important and challenging task. One of its difficulties is related to unstable tests, where the execution can take different branches for real and floating-point numbers. This paper presents a new verification technique for numerical properties, named Runtime Abstract Interpretation (RAI), that, given an annotated source code, embeds into it an abstract analyzer in order to analyze the program behavior at runtime. RAI is a hybrid technique combining abstract interpretation and runtime verification that aims at being sound as the former while taking benefit from the concrete run to gain greater precision from the latter when necessary. It solves the problem of unstable tests by surrounding an un- stable test by two carefully defined program points, forming a so-called split-merge section, for which it separately analyzes different executions and merges the computed domains at the end of the section. The imple- mentation of this technique relies on two basic tools, FLDCompiler, that performs a source-to-source transformation of the given program and defines the split-merge sections, and an instrumentation library FLDLib that provides necessary primitives to explore relevant (partial) executions of each section and propagate accuracy properties. Initial experiments show that the proposed technique can efficiently and soundly analyze numerical accuracy for industrial programs on thin numerical scenarios.

Dara Ly, Nikolai Kosmatov, Frédéric Loulergue, Julien Signoles
Verified Runtime Assertion Checking for Memory Properties [link]
In International Conference on Tests and Proofs (TAP), 2020

Runtime Assertion Checking (RAC) for expressive specification languages is a non-trivial verification task, that becomes even more complex for memory-related properties of imperative languages with dynamic memory allocation. It is important to ensure the soundness of RAC verdicts, in particular when RAC reports the absence of failures for execution traces. This paper presents a formalization of a program transformation technique for RAC of memory properties for a representative language with memory operations. It includes an observation memory model that is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.

Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles
Detection of Security Vulnerabilities in C Code using Runtime Verification [link]
In International Conference on Tests and Proofs (TAP), 2018
Explore how some runtime verification tools (including E-ACSL) may detect security vulnerabilities.

Despite significant progress made by runtime verification tools in recent years, memory errors remain one of the primary threats to software security. The present work is aimed at providing an objective up-to-date experience study on the capacity of modern online runtime verification tools to automatically detect security flaws in C programs. The reported experiments are performed using three advanced runtime verification tools (E-ACSL, Google Sanitizer and RV-Match) over 700 test cases belonging to SARD-100 test suite of the SAMATE project and Toyota ITC Benchmark, a publicly available benchmarking suite developed at the Toyota InfoTechnology Center. SARD-100 specifically targets security flaws identified by the Common Weakness Enumeration (CWE) taxonomy, while Toyota ITC Benchmark addresses more general memory defects, as well as numerical and concurrency issues. We compare tools based on different approaches – a formal semantic based tool, a formal specification verifier and a memory debugger – and evaluate their cumulative detection capacity.

Dara Ly, Nikolai Kosmatov, Julien Signoles, Frédéric Loulergue
Soundness of a Dataflow Analysis for Memory Monitoring [link]
In Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems (HILT), 2018

An important concern addressed by runtime verification tools for C code is related to detecting memory errors. It requires to monitor some properties of memory locations (e.g., their validity and initialization) along the whole program execution. Static analysis based optimizations have been shown to significantly improve the performances of such tools by reducing the monitoring of irrelevant locations. However, soundness of the verdict of the whole tool strongly depends on the soundness of the underlying static analysis technique. This paper tackles this issue for the dataflow analysis used to optimize the E-ACSL runtime assertion checking tool. We formally define the core dataflow analysis used by E-ACSL and prove its soundness.

Kostyantyn Vorobyov, Nikolai Kosmatov, Julien Signoles, Arvid Jakobsson
Runtime detection of temporal memory errors. [link]
In International Conference on Runtime Verification (RV), 2017

State-of-the-art memory debuggers have become efficient in detecting spatial memory errors – dereference of pointers to unallocated memory. These tools, however, cannot always detect errors arising from the use of stale pointers to valid memory (temporal memory errors). This paper presents an approach to reliable detection of temporal memory errors during a run of a program. This technique tracks allocated memory tagging allocated objects and pointers with tokens that allow to reason about their temporal properties. The technique further checks pointer dereferences and detects temporal (and spatial) memory errors before they occur. The present approach has been implemented in E-ACSL – a runtime verification tool for C programs. Experimentation with E-ACSL using TempLIST benchmark comprising small C programs seeded with temporal errors shows that the suggested technique detects temporal memory errors missed by state-of-the-art memory debuggers. Further experiments with computationally intensive runs of programs from SPEC CPU indicate that the overheads of the proposed approach are within acceptable range to be used during testing or debugging.

Arvid Jakobsson, Nikolai Kosmatov, Julien Signoles
Rester statique pour devenir plus rapide, plus précis et plus mince [link]
In Journées Francophones des Langages Applicatifs (JFLA), 2015
In French

E-ACSL est un greffon de Frama-C, une plateforme d’analyse de codes C qui est développée en OCaml. Son but est de transformer un programme C formellement annoté dans le langage de spécification éponyme E-ACSL en un autre programme C dont le comportement à l’exécution est équivalent si toutes les spécifications sont dynamiquement vérifiées et qui échoue sur la première spécification fausse sinon. Pour cela, une instrumentation du programme source est notamment effectuée afin, d’une part, de conserver les informations nécessaires à l’évaluation des prédicats E-ACSL et, d’autre part, de traduire correctement ces derniers.

Cet article présente deux analyses statiques qui améliorent grandement la précision de cette transformation de programmes en réduisant l’instrumentation effectuée. Ainsi, le code généré est plus rapide et consomme moins de mémoire lors de son exécution. La première analyse est un système de types fondé sur une inférence d’intervalles et permettant de distinguer les entiers (mathématiques) pouvant être convertis en des expressions C de type “entier machine” de ceux devant être traduits vers des entiers en précision arbitraire. La seconde analyse est une analyse flot de données arrière sur-approximante paramétrée par une analyse d’alias. Elle permet de limiter l’instrumentation des opérations sur la mémoire à celles ayant un impact potentiel sur la validité d’une annotation formelle.

Nikolai Kosmatov, Guillaume Petiot, Julien Signoles
An Optimized Memory Monitoring for Runtime Assertion Checking of C Programs [link]
In Proceedings of Runtime Verification (RV), 2013

Runtime assertion checking provides a powerful, highly automatizable technique to detect violations of specified program properties. However, monitoring of annotations for pointers and memory locations (such as being valid, initialized, in a particular block, with a particular offset, etc.) is not straightforward and requires systematic instrumentation and monitoring of memory-related operations. This paper describes the runtime memory monitoring library we developed for execution support of E-ACSL, executable specification language for C programs offered by the Frama-C platform for analysis of C code. We present the global architecture of our solution as well as various optimizations we realized to make memory monitoring more efficient. Our experiments confirm the benefits of these optimizations and illustrate the bug detection potential of runtime assertion checking with E-ACSL.

Aoraï

Manuals

Nicolas Stouls
Aoraï Plug-in Tutorial [link] [BibTeX]
@manual{aorai_user_manual,
title = "Aoraï Plug-in Tutorial",
author = "Stouls, Nicolas",
url = "http://frama-c.com/download/aorai/aorai-manual.pdf",
}
The official manual of the Frama-C plug-in Aoraï.

Foundational

Julien Groslambert, Nicolas Stouls
Vérification de propriétés LTL sur des programmes C par génération d'annotations [link]
In Proceedings of Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2009
In French.

Ce travail propose une méthode de vérification de propriétés temporelles basée sur la génération automatique d’annotations de programmes. Les annotations générées sont ensuite vérifiées par des prouveurs automatiques via un calcul de plus faible précondition. Notre contribution vise à optimiser une technique existante de génération d’annotations, afin d’améliorer l’automatisation de la vérification des obligations de preuve produites. Cette approche a été outillée sous la forme d’un plugin au sein de l’outil Frama-C pour la vérification de programmes C.

Security slicing

Foundational

Benjamin Monate, Julien Signoles
Slicing for Security of Code [link]
In Proceedings of the 1st international conference on Trusted Computing and Trust in Information Technologies (TRUST), 2008

Bugs in programs implementing security features can be catastrophic: for example they may be exploited by malign users to gain access to sensitive data. These exploits break the confidentiality of information. All security analyses assume that softwares implementing security features correctly implement the security policy, i.e. are security bug-free. This assumption is almost always wrong and IT security administrators consider that any software that has no security patches on a regular basis should be replaced as soon as possible. As programs implementing security features are usually large, manual auditing is very error prone and testing techniques are very expensive. This article proposes to reduce the code that has to be audited by applying a program reduction technique called slicing . Slicing transforms a source code into an equivalent one according to a set of criteria. We show that existing slicing criteria do not preserve the confidentiality of information. We introduce a new automatic and correct source-to-source method properly preserving the confidentiality of information i.e. confidentiality is guaranteed to be exactly the same in the original program and in the sliced program.

Internal plug-ins at CEA

CFP

Foundational

Michele Alberti, Julien Signoles
Context Generation from Formal Specifications for C Analysis Tools [link]
In Logic-based Program Synthesis and Transformation (LOPSTR), 2017
Best paper award.

Analysis tools like abstract interpreters, symbolic execution tools and testing tools usually require a proper context to give useful results when analyzing a particular function. Such a context initializes the function parameters and global variables to comply with function requirements. However it may be error-prone to write it by hand: the handwritten context might contain bugs or not match the intended specification. A more robust approach is to specify the context in a dedicated specification language, and hold the analysis tools to support it properly. This may mean to put significant development efforts for enhancing the tools, something that is often not feasible if ever possible.

This paper presents a way to systematically generate such a context from a formal specification of a C function. This is applied to a subset of the ACSL specification language in order to generate suitable contexts for the abstract interpretation-based value analysis plug-ins of Frama-C, a framework for analysis of code written in C. The idea here presented has been implemented in a new Frama-C plug-in which is currently in use in an operational industrial setting.

LTest

Theses

Thibault Martin
Techniques de test pour des critères de couverture avancés [link] [BibTeX]
@phdthesis{2022_martin_phd,
title = "Techniques de test pour des critères de couverture avancés",
author = "Martin, Thibault",
year = "2022",
url = "https://www.theses.fr/2022UPASG077",
school = "Université Paris-Saclay",
}
Université Paris-Saclay, PhD Thesis, 2022

At a time where software are omnipresent in our daily life, verifying their safety and security present an important challenge for the industry. The most used technique to ensure that a software meets certain requirements is testing, where we run the program with some controlled input sets. A major issue is then to ensure that these input sets cover enough different situations. Many proposals have been made, called coverage criteria, which define test objectives through which at least one execution must pass during tests. In this thesis, we examine different possibilities to combine formal methods (mathematical techniques) and testing in order to improve the efficiency of the testing process. We focused our efforts on dataflow criteria, which observe the behavior of definitions and uses of each variables in the program, and the detection of polluting objectives for these criteria.We proposed several techniques, with their implementations and evaluations on real C programs. We then studied the impact of these dataflow criteria on test generation. Finally, we conclude by designing a method, using polluting objectives detection, to verify the effectiveness of countermeasures against fault injection attacks, and thus find errors in their implementation. This method was applied to the bootloader of WooKey, an encrypted storage device.

Foundational

Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, Matthieu Lemerre
Detection of Polluting Test Objectives for Dataflow Criteria [link]
In International Conference on Integrated Formal Methods (IFM), 2020

Dataflow test coverage criteria, such as all-defs and all-uses, belong to the most advanced coverage criteria. These criteria are defined by complex artifacts combining variable definitions, uses and program paths. Detection of polluting (i.e. inapplicable, infeasible and equivalent) test objectives for such criteria is a particularly challenging task. This short paper evaluates three detection approaches involving dataflow analysis, value analysis and weakest precondition calculus. We implement and compare these approaches, analyze their detection capacities and propose a methodology for their efficient combination. Initial experiments illustrate the benefits of the proposed approach.

Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, Virgile Prevosto
Taming Coverage Criteria Heterogeneity with LTest [link]
In International Conference on Software Testing, Verification and Validation (ICST), 2017

Automated white-box testing is a major issue in software engineering. In previous work, we introduced LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest supports a broad class of coverage criteria in a unified way (through the label specification mechanism) and covers most major parts of the testing process - including coverage measurement, test generation and detection of infeasible test objectives. However, the original version of LTest was unable to handle several major classes of coverage criteria, such as MCDC or dataflow criteria. Moreover, its practical applicability remained barely assessed. In this work, we present a significantly extended version of LTest that supports almost all existing testing criteria, including MCDC and some software security properties, through a native support of recently proposed hyperlabels. We also provide a more realistic view on the practical applicability of the extended tool, with experiments assessing its efficiency and scalability on real-world programs.

Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, Nikolai Kosmatov
An All-in-One Toolkit for Automated White-Box Testing [link]
In International Conference on Tests and Proofs (TAP), 2014

Automated white-box testing is a major issue in software engineering. Over the years, several tools have been proposed for supporting distinct parts of the testing process. Yet, these tools are mostly separated and most of them support only a fixed and restricted subset of testing criteria. We describe in this paper Frama-C/LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest provides a unified support of many different testing criteria as well as an easy integration of new criteria. Moreover, it is designed around three basic services (test coverage estimation, automatic test generation, detection of uncoverable objectives) covering most major aspects of white-box testing and taking benefit from a combination of static and dynamic analyses. Services can cooperate through a shared coverage database. Preliminary experiments demonstrate the possibilities and advantages of such cooperations.

Others

Michaël Marcozzi, Mike Papadakis, Sébastien Bardin, Nikolai Kosmatov, Virgile Prévosto, Loic Correnson
Time to Clean Your Test Objectives [link]
In International Conference On Software Engineering (ICSE), 2018

Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting eecient test suites, able to detect a maximum number of bugs with manageable eeort. To do so, they rely on coverage criteria, which deene some precise test objectives to be covered. However, many common criteria specify a signiicant number of objectives that occur to be infeasible or redundant in practice, like covering dead code or semantically equal mutants. Such objectives are well-known to be harmful to the design of test suites, impacting both the eeciency and precision of the tester’s eeort. This work introduces a sound and scalable technique to prune out a signiicant part of the infeasible and redundant objectives produced by a panel of white-box criteria. In a nutshell, we reduce this task to proving the validity of logical assertions in the code under test. The technique is implemented in a tool that relies on weakest-precondition calculus and SMT solving for proving the assertions. The tool is built on top of the Frama-C veriication platform, which we carefully tune for our speciic scalability needs. The experiments reveal that the pruning capabilities of the tool can reduce the number of targeted test objectives in a program by up to 27% and scale to real programs of 200K lines, making it possible to automate a painstaking part of their current testing process.

MetACSL

Theses

Virgile Robles
Specifying and verifying high-level requirements on large programs : application to security of C programs [link] [BibTeX]
@phdthesis{2022_robles_phd,
title = "Specifying and verifying high-level requirements on large programs : application to security of C programs",
author = "Robles, Virgile",
year = "2022",
url = "https://www.theses.fr/2022UPAST001",
school = "Université Paris-Saclay",
}
Université Paris-Saclay, PhD Thesis, 2022

Specification and verification of highlevel requirements (such as security properties like data integrity or confidentiality) remains an important challenge for the industrial practice, despite being a major part of functional specifications. This thesis presents a formal framework for their expression called meta-properties, supported by a description on an abstract programming language, focusing on properties related to memory and global invariants. This framework is then applied to the C programming language, introducing the HILARE extension to ACSL, to allow easy specification of these requirements on large C programs. Verification techniques for HILARE, based on local assertion generation and reuse of the existing Frama-C analyzers, are presented and implemented into the MetAcsl plugin for Frama-C. A complete methodology for assessing large programs is laid out, articulating meta-properties, verification techniques and quirks specific to the C programming language. This methodology is illustrated to a complex case study involving the bootloader of WooKey, a secure USB storage device. Finally, we explore another way to verify a high-level requirement deducing it from others, through a formal system proven in Why3 and integrated in MetAcsl.

Foundational

Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties [link]
In Tests and Proofs (TAP), 2019

A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their support in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. This is demonstrated by applying these techniques on two illustrative case studies.

Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall
MetAcsl: Specification and Verification of High-Level Properties [link]
In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2019

Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related properties of a whole software module are actually established, making it very difficult to assess them. To address this issue, this paper proposes a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in two illustrative case studies.

PathCrawler

Manuals

PathCrawler Automatic Test Generation Tool For C Programs User Manual [link] [BibTeX]
@manual{pathcrawler_user_manual,
title = "PathCrawler Automatic Test Generation Tool For C Programs User Manual",
url = "http://frama-c.com/download/frama-c-pathcrawler.pdf",
}
The user manual of the Frama-C plug-in PathCrawler.

Foundational

Nicky Williams, Bruno Marre, Patricia Mouy, Muriel Roger
PathCrawler: automatic generation of path tests by combining static and dynamic analysis [link]
In European Dependable Computing Conference (EDCC), 2005

We present the PathCrawler prototype tool for the automatic generation of test-cases satisfying the rigorous all-paths criterion, with a user-defined limit on the number of loop iterations in the covered paths. The prototype treats C code and we illustrate the test-case generation process on a representative example of a C function containing data-structures of variable dimensions, loops with variable numbers of iterations and many infeasible paths. PathCrawler is based on a novel combination of code instrumentation and constraint solving which makes it both efficient and open to extension. It suffers neither from the approximations and complexity of static analysis, nor from the number of executions demanded by the use of heuristic algorithms in function minimisation and the possibility that they fail to find a solution. We believe that it demonstrates the feasibility of rigorous and systematic testing of sequential programs coded in imperative languages.

Nicky Williams, Bruno Marre, Patricia Mouy
On-the-fly generation of k-paths tests for C functions: towards the automation of grey-box testing [link]
In International Conference on Automated Software Engineering (ASE), 2004

We present a method for the automatic generation of tests satisfying the all-paths criterion, with a user-defined limit, k, on the number of loop iterations in the covered paths. We have implemented a prototype for C code. We illustrate our approach on a representative example of a C function containing data-structures of variable dimensions, loops with variable numbers of iterations and many infeasible paths.

We explain why our method is efficient enough to scale up to the unit testing of ealistic programs. It is flexible enough to take into account certain specifications of the tested code. This is why we believe that it could become the cornerstone of a fully automatic grey-box testing process, based on the novel combination of code instrumentation and constraint solving described here.

Tutorials

Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro
A Lesson on Structural Testing with PathCrawler-online.com [link]
In International Conference on Tests and Proofs (TAP), 2012

PathCrawler is a test generation tool developed at CEA LIST for structural testing of C programs. The new version of PathCrawler is developed in an entirely novel form: that of a test-case generation web service which is freely accessible at PathCrawler-online.com. This service allows many test-case generation sessions to be run in parallel in a completely robust and secure way. This tool demo and teaching experience paper presents PathCrawler-online.com in the form of a lesson on structural software testing, showing its benefits, limitations and illustrating the usage of the tool on simple examples.

Nicky Williams, Nikolai Kosmatov
Structural Testing with PathCrawler. Tutorial Synopsis [link]
In International Conference on Quality Software (QSIC), 2012

Automatic testing tools allow huge savings but they do not exonerate the user from thinking carefully about what they want testing to achieve. To successfully use the Path Crawler-online structural testing tool, the user must provide not only the full source code, but also must set the test parameters and program the oracle. This demands a different“mindset” from that used for informal functional-style manual testing, as we explain with the help of several examples.

Others

Nikolai Kosmatov, Bernard Botella, Muriel Roger, Nicky Williams
Online Test Generation with PathCrawler. Tool demo. [link]
In International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA), 2011
Best demo award

This demonstration presents a new version of Path Crawler developed in an entirely novel form: that of a test-case server which is freely accessible online.

Nicky Williams
Abstract path testing with PathCrawler [link]
In International Workshop on Automation of Software Test (AST), 2010

PathCrawler is a tool developed by CEA List for the automatic generation of test inputs to ensure the coverage of all feasible execution paths of a C function. Due to its concolic approach and depth-first exhaustive search strategy implemented in Prolog, PathCrawler is particularly efficient in the generation of tests to cover the fully expanded tree of feasible paths. However, for many tested functions this coverage criterion demands too many tests and a weaker criterion must be used. In order to efficiently generate tests for a new criterion whilst still using a concolic approach, we must modify the search strategy. To facilitate the definition and comparison of different coverage criteria, we propose a new type of tree, trees of abstract paths, and define the different types of abstract node in these trees. We demonstrate how several criteria can be conveniently defined in terms of coverage of these new trees. Moreover, efficient generation of tests to satisfy these criteria using the concolic approach can be designed as different strategies to explore these trees.

Nikolai Kosmatov
On Complexity of All-Paths Test Generation. From Practice to Theory [link]
In Testing: Academic and Industrial Conference - Practice and Research Techniques (TAIC PART), 2009

Automatic structural testing of programs becomes more and more popular in software engineering. Among the most rigorous structural coverage criteria, all-paths coverage re-quires to generate a set of test cases such that every fea-sible execution path of the program under test is executed by one test case. This article addresses different aspects of computability and complexity of constraint-based all-paths test generation for C programs from the practitioner’s point of view, and tries to bridge the gap between mathematical theory and practical computation problems arising in this domain. We focus on two particular classes of programs impor-tant for practice. We show first that for a class containing the simplest programs with strong restrictions, all-paths test generation in polynomial time is possible. For a wider class of programs in which inputs may be used as array indices (or pointer offsets), all-paths test generation is shown to be NP-hard. Some experimental results illustrating test gener-ation time for programs of these classes are provided.

Nicky Williams, Muriel Roger
Test Generation Strategies to Measure Worst-Case Execution Time [link]
In International Workshop on Automation of Software Test (AST), 2009

Under certain conditions, the worst-case execution time (WCET) of a function can be found by measuring the effective execution time for each feasible execution path. Automatic generation of test inputs can help make this approach more feasible. To reduce the number of tests, we define two partial orders on the execution paths of the program under test. Under further conditions, these partial orders represent the relation between the execution times of the paths. We explain how we modified the strategy of the PathCrawler structural test-case generation tool to generate as few tests as possible for paths which are not maximal in these partial orders, whilst ensuring that the WCET is exhibited by at least one case in the set. The techniques used could also serve in the implementation of other test generation strategies which have nothing to do with WCET.

Bernard Botella, Mickaël Delahaye, Stéphane Hong-Tuan-Ha, Nikolai Kosmatov, Patricia Mouy, Muriel Roger, Nicky Williams
Automating Structural Testing of C Programs: Experience with PathCrawler [link]
In International Workshop on Automation of Software Test (AST), 2009

Structural testing is widely used in industrial verification processes of critical software. This report presents PathCrawler, a structural test generation tool that may be used to automate this activity, and several evaluation criteria of automatic test generation tools for C programs. These criteria correspond to the issues identified during our ongoing experience in the development of PathCrawler and its application to industrial software. They include issues arising for some specific types of software. Some of them are still difficult open problems. Others are (partially) solved, and the solution adopted in PathCrawler is discussed. We believe that these criteria must be satisfied in order for the automation of structural testing to become an industrial reality.

Nikolai Kosmatov
All-paths test generation for programs with internal aliases [link]
In International Symposium on Software Reliability Engineering (ISSRE), 2008

In structural testing of programs, the all-paths coverage criterion requires to generate a set of test cases such that every possible execution path of the program under test is executed by one test case. This task becomes very complex in presence of aliases, i.e. different ways to address the same memory location. In practice, the presence of aliases may result in enumeration of possible inputs, generation of several test cases for the same path and/or a failure to generate a test case for some feasible path. This article presents the problem of aliases in the context of classical depth-first test generation method. We classify aliases into two groups: external aliases, existing already at the entry point of the function under test (due to pointer inputs), and internal ones, created during its symbolic execution. This paper focuses on internal aliases.We propose an original extension of the depth-first test generation method for C programs with internal aliases. It limits the enumeration of inputs and the generation of superfluous test cases. Initial experiments show that our method canconsiderably improve the performances of the existing tools on programs with aliases.

Patricia Mouy, Bruno Marre, Nicky Williams, Pascale Le Gall
Generation of all-paths unit test with function calls [link]
In International Conference on Software Testing, Verification, and Validation (ICST), 2008

Structural testing is usually restricted to unit tests and based on some clear definition of source code coverage. In particular, the all-paths criterion, which requires at least one test-case per feasible path of the function under test, is recognised as offering a high level of software reliability. This paper deals with the difficulties of using structural unit testing to test functions which call other functions. To limit the resulting combinatorial explosion in the number of paths, we choose to abstract the called functions by their specification. We incorporate the functional information on the called functions within the structural information on the function under test, given as a control flow graph (CFG). This representation combining functional and structural descriptions may be viewed as an extension of the classic CFG and allows us to characterise test selection criteria ensuring the coverage of the source code of the function under test. Two new criteria will be proposed. The first criterion corresponds to the coverage of all the paths of this new representation, including all the paths arising from the functional description of the called functions. The second criterion covers all the feasible paths of the function under test only. We describe how we automate test-data generation with respect to such grey-box (combinations of black- box and white-box) test selection strategies, and we apply the resulting extension of our PathCrawler tool to examples coded in the C language.

Nicky Williams
WCET measurement using modified path testing [link]
In International Workshop on Worst-Case Execution Time Analysis (WCET), 2005

Prediction of Worst Case Execution Time (WCET) is made increasingly difficult by the recent developments in micro-processor architectures. Instead of predicting the WCET using techniques such as static analysis, the effective execution time can be measured when the program is run on the target architecture ir a cycle-accurate simulator. However, exhaustive measurments on all possible input values are usually prohibited by the numer of possible input values. As a first step towardsa solution, we propose path testing using the PathCrawler tool to automatically generate test inputs for all feasible execution paths in C source code. For programs containing too many execution paths for this approach to be feasible, we propose to modify PathCrawler’s strategy in order to cut down on the number of generated tests while still ensuring measurment of the path with the longest execution time.

RPP

Theses

Lionel Blatter
Relational properties for specification and verification of C programs in Frama-C [link] [BibTeX]
@phdthesis{2019_thesis_blatter,
title = "Relational properties for specification and verification of C programs in Frama-C",
author = "Blatter, Lionel",
year = "2019",
url = "http://www.theses.fr/2019SACLC065",
school = "University of Paris Saclay",
}
University of Paris Saclay, PhD Thesis, 2019

Foundational

Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto, Guillaume Petiot
Static and Dynamic Verification of Relational Properties on Self-composed C Code [link]
In In Tests and Proofs - 12th International Conference (TAP), 2018

Function contracts are a well-established way of formally specifying the intended behavior of a function. However, they usually only describe what should happen during a single call. Relational properties, on the other hand, link several function calls. They include such properties as non-interference, continuity and monotonicity. Other examples relate sequences of function calls, for instance, to show that decrypting an encrypted message with the appropriate key gives back the original message. Such properties cannot be expressed directly in the traditional setting of modular deductive verification, but are amenable to verification through self-composition. This paper presents a verification technique dedicated to relational properties in C programs and its implementation in the form of a FRAMA-C plugin called RPP and based on self-composition. It supports functions with side effects and recursive functions. The proposed approach makes it possible to prove a relational property, to check it at runtime, to generate a counterexample using testing and to use it as a hypothesis in the subsequent verification. Our initial experiments on existing benchmarks confirm that the proposed technique is helpful for static and dynamic analysis of relational properties.

Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto
RPP: Automatic Proof of Relational Properties by Self-composition [link]
In Tools and Algorithms for the Construction and Analysis of Systems23rd International Conference, TACAS, 2017

Self-composition provides a powerful theoretical approach to prove relational properties, i.e. properties relating several program executions, that has been applied to compare two runs of one or similar programs (in secure dataflow properties, code transformations, etc.). This tool demo paper presents RPP, an original implementation of self-composition for specification and verification of relational properties in C programs in the FRAMA-C platform. We consider a very general notion of relational properties invoking any finite number of function calls of possibly dissimilar functions with possible nested calls. The new tool allows the user to specify a relational property, to prove it in a completely automatic way using classic deductive verification, and to use it as a hypothesis in the proof of other properties that may rely on it.

SecureFlow

Theses

Mounir Assaf
From qualitative to quantitative program analysis: permissive enforcement of secure information flow [link] [BibTeX]
@phdthesis{2015_thesis_assaf,
title = "From qualitative to quantitative program analysis: permissive enforcement of secure information flow",
author = "Assaf, Mounir",
year = "2015",
url = "http://www.theses.fr/2015REN1S003",
school = "University of Rennes 1",
}
University of Rennes 1, PhD Thesis, 2015

Foundational

Gergö Barany, Julien Signoles
Hybrid Information Flow Analysis for Real-World C Code [link]
In International Conference on Tests and Proofs (TAP), 2017

Information flow analysis models the propagation of data through a software system and identifies unintended information leaks. There is a wide range of such analyses, tracking flows statically, dynamically, or in a hybrid way combining both static and dynamic approaches.

We present a hybrid information flow analysis for a large subset of the C programming language. Extending previous work that handled a few difficult features of C, our analysis can now deal with arrays, pointers with pointer arithmetic, structures, dynamic memory allocation, complex control flow, and statically resolvable indirect function calls. The analysis is implemented as a plugin to the Frama-C framework.

We demonstrate the applicability and precision of our analyzer by applying it to an open-source cryptographic library. By combining abstract interpretation and monitoring techniques, we verify an information flow policy that proves the absence of control-flow based timing attacks against the implementations of many common cryptographic algorithms. Conversely, we demonstrate that our analysis is able to detect a known instance of this kind of vulnerability in another cryptographic primitive.

Mounir Assaf, Julien Signoles, Éric Totel, Frédéric Tronel
Program transformation for non-interference verification on programs with pointers [link]
In International Information Security and Privacy Conference (SEC), 2013

Novel approaches for dynamic information flow monitoring are promising since they enable permissive (accepting a large subset of executions) yet sound (rejecting all unsecure executions) enforcement of non-interference. In this paper, we present a dynamic information flow monitor for a language supporting pointers. Our flow-sensitive monitor relies on prior static analysis in order to soundly enforce non-interference. We also propose a program transformation that preserves the behavior of initial programs and soundly inlines our security monitor. This program transformation enables both dynamic and static verification of non-interference.

External plug-ins

Conc2Seq

Theses

Allan Blanchard
Aide à la vérification de programmes concurrents par transformation de code et de spécifications [link] [BibTeX]
@phdthesis{2016_blanchard_phd,
title = "Aide à la vérification de programmes concurrents par transformation de code et de spécifications",
author = "Blanchard, Allan",
year = "2016",
url = "https://www.theses.fr/2016ORLE2073",
school = "University of Orléans",
}
University of Orléans, PhD Thesis, 2016

Formal verification of concurrent programs is a hard task. There exists different methods to perform such a task, but very few are applied to the verification of programs written using real life programming languages. On the other side, formal verification of sequential programs is successfully applied for many years, and allows to get high confidence in our systems. As an alternative to dedicated concurrent program analyses, we propose a method to transform concurrent programs into sequential ones to make them analyzable by tools dedicated to sequential programs. This work takes place within the analysis framework FRAMA-C, dedicated to the analysis of C code specified with ACSL. The different analyses provided by FRAMA-C are plugins to the framework, which are currently mostly dedicated to sequential programs. We apply this method to the verification of a concurrent code taken from an hypervisor. We describe the automation of the method implemented by a new plugin to FRAMAC that allow to produce, from a specified concurrent program, an equivalent specified sequential program. We present the basis of a formalization of the method with the objective to prove its validity. This validity is admissible only for the class of sequentially consistent programs. So, we finally propose a prototype of constraint solver for weak memory models, which is able to determine whether a program is in this class or not, depending on the targeted hardware.

Foundational

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation [link]
In Fifth International Workshop on Verification and Program Transformation (VPT), 2017

Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed conc2seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program transformation principle behind conc2seq, and present an effort towards the full mechanization of both the for- malization and proofs with the proof assistant Coq.

Allan Blanchard, Nikolai Kosmatov, Matthieu Lemerre, Frédéric Loulergue
Conc2Seq: A Frama-C Plugin for Verification of Parallel Compositions of C Programs [link]
In 16th International Working Conference on Source Code Analysis and Manipulation (SCAM), 2016

Frama-C is an extensible modular framework for analysis of C programs that offers different analyzers in the form of collaborating plugins. Currently, Frama-C does not support the proof of functional properties of concurrent code. We present Conc2Seq, a new code transformation based tool realized as a Frama-C plugin and dedicated to the verification of concurrent C programs. Assuming the program under verification respects an interleaving semantics, Conc2Seq transforms the original concurrent C program into a sequential one in which concurrency is simulated by interleavings. User specifications are automatically reintegrated into the new code without manual intervention. The goal of the proposed code transformation technique is to allow the user to reason about a concurrent program through the interleaving semantics using existing Frama-C analyzers.

Others

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Concurrent Program Verification by Code Transformation: Correctness [link]
In LIFO Research Report RR-2017-03, 2017
Complete version of "From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation"

Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed Conc2Seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program transformation principle behind Conc2Seq, and present an effort towards the full mechanization of both the formalization and proofs with the proof assistant Coq.

CELIA

Foundational

Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea, Mihaela Sighireanu
Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data [link]
In International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2012

We describe a framework for reasoning about programs with lists carrying integer numerical data. We use abstract domains to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, on the multisets of data stored in these lists, and on the data at their different positions. Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called Celia and experimented successfully on a large benchmark of programs.

Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea, Mihaela Sighireanu
On inter-procedural analysis of programs with lists and data [link]
In Proceedings of the 32nd Conference on Programming Language Design and Implementation (PLDI), 2011

We address the problem of automatic synthesis of assertions on sequential programs with singly-linked lists containing data over infinite domains such as integers or reals. Our approach is based on an accurate abstract inter-procedural analysis. Program configurations are represented by graphs where nodes represent list segments without sharing. The data in these list segments are characterized by constraints in abstract domains. We consider a domain where constraints are in a universally quantified fragment of the first-order logic over sequences, as well as a domain constraining the multisets of data in sequences.

Our analysis computes the effect of each procedure in a local manner, by considering only the reachable part of the heap from its actual parameters. In order to avoid losses of information, we introduce a mechanism based on unfolding/folding operations allowing to strengthen the analysis in the domain of first-order formulas by the analysis in the multisets domain.

The same mechanism is used for strengthening the sound (but incomplete) entailment operator of the domain of first-order formulas. We have implemented our techniques in a prototype tool and we have shown that our approach is powerful enough for automatic (1) generation of non-trivial procedure summaries, (2) pre/post-condition reasoning, and (3) procedure equivalence checking.

Cost

Foundational

Nicolas Ayache, Roberto M. Amadio, Yann Régis-Gianas
Certifying and reasoning on cost annotations in C programs [link]
In Proceedings of the 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), 2012

We present a so-called labelling method to enrich a compiler in order to turn it into a “cost annotating compiler”, that is, a compiler which can lift pieces of information on the execution cost of the object code as cost annotations on the source code. These cost annotations characterize the execution costs of code fragments of constant complexity. The first contribution of this paper is a proof methodology that extends standard simulation proofs of compiler correctness to ensure that the cost annotations on the source code are sound and precise with respect to an execution cost model of the object code. As a second contribution, we demonstrate that our label-based instrumentation is scalable because it consists in a modular extension of the compilation chain. To that end, we report our successful experience in implementing and testing the labelling approach on top of a prototype compiler written in OCaml for (a large fragment of) the C language. As a third and last contribution, we provide evidence for the usability of the generated cost annotations as a mean to reason on the concrete complexity of programs written in C. For this purpose, we present a Frama-C plugin that uses our cost annotating compiler to automatically infer trustworthy logic assertions about the concrete worst case execution cost of programs written in a fragment of the C language. These logic assertions are synthetic in the sense that they characterize the cost of executing the entire program, not only constant-time fragments. (These bounds may depend on the size of the input data.) We report our experimentations on some C programs, especially programs generated by a compiler for the synchronous programming language Lustre used in critical embedded software.

DeadlockF

Others

Tomáš Dacík, Tomáš Vojnar
Static Analysis in the Frama-C Environment Focused on Deadlock Detection [link]
Brno University of Technology, Faculty of Information Technology, 2020
Bachelor thesis describing principles and implementation of the DeadlockF analyser.

This thesis presents a design of a new static analyser focused on deadlock detection, implemented as a plugin of the Frama-C platform. Together with the core algorithm of deadlock detection, we also present a light-weight method that allows one to analyse (not only for the purposes of deadlock detection) multithreaded programs using sequential analysers of Frama-C. Results of experiments show that our tool is able to handle real-world C code with high precision. Moreover, we demonstrate its extensibility by so-far experimental implementation of data race detection.

Fan-C

Foundational

Pascal Cuoq, David Delmas, Stéphane Duprat, Victoria Moya Lamiel
Fan-C, a Frama-C plug-in for data flow verification [link]
In Proceedings of Embedded Real Time Software and Systems (ERTS²), 2012

DO-178B compliant avionics development processes must both define the data and control flows of embedded software at design level, and verify flows are faithfully implemented in the source code. This verification is traditionally performed during dedicated code reviews, but such intellectual activities are costly and error-prone, especially for large and complex software. In this paper, we present the Fan-C plug-in, developed by Airbus on top of the abstract-interpretation-based value and dataflow analyses of the Frama-C platform, in order to automate this verification activity for C avionics software. We therefore describe the Airbus context, the Frama-C platform, its value analysis and related plug-ins, the Fan-C plug-in, and discuss analysis results and ongoing industrial deployment and qualification activities.

Jessie

Manuals

Jessie ressources [link] [BibTeX]
@manual{jessie_manual,
title = "Jessie ressources",
url = "http://krakatoa.lri.fr/",
}
The main web page, including the manual and many other resources.

Theses

François Bobot
Logique de séparation et vérification déductive [link] [BibTeX]
@phdthesis{2011_thesis_bobot,
title = "Logique de séparation et vérification déductive",
author = "Bobot, François",
year = "2011",
url = "http://proval.lri.fr/publications/bobot11these.pdf",
school = "University of Paris Sud",
}
University of Paris Sud, PhD Thesis, 2011
Romain Bardou
Verification of Pointer Programs Using Regions and Permissions. [link] [BibTeX]
@phdthesis{2011_thesis_bardou,
title = "Verification of Pointer Programs Using Regions and Permissions.",
author = "Bardou, Romain",
year = "2011",
url = "http://proval.lri.fr/publications/bardou11phd.pdf",
school = "University of Paris Sud",
}
University of Paris Sud, PhD Thesis, 2011
Yannick Moy
Automatic Modular Static Safety Checking for C Programs [link] [BibTeX]
@phdthesis{2009_thesis_moy,
title = "Automatic Modular Static Safety Checking for C Programs",
author = "Moy, Yannick",
year = "2009",
url = "http://www.lri.fr/~marche/moy09phd.pdf",
school = "University of Paris Sud",
}
University of Paris Sud, PhD Thesis, 2009

Foundational

Sylvie Boldo, Thi Minh Tuyen Nguyen
Proofs of numerical programs when the compiler optimizes [link]
In Innovations in Systems and Software Engineering, 2011

On certain recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. Our goal is to formally prove properties about numerical programs that are true for multiple architectures and compilers. We propose an approach that states the rounding error of each floating-point computation whatever the environment and the compiler choices. This approach is implemented in the Frama-C platform for static analysis of C code. Small case studies using this approach are entirely and automatically proved.

Yannick Moy, Claude Marché
Modular inference of subprogram contracts for safety checking [link]
In Journal of Symbolic Computation, 2010

Contracts expressed by logic formulas allow one to formally specify expected behavior of programs. But writing such specifications manually takes a significant amount of work, in particular for uninteresting contracts which only aim at avoiding run-time errors during the execution. Thus, for programs of large size, it is desirable to at least partially infer such contracts. We propose a method to infer contracts expressed as boolean combinations of linear equalities and inequalities by combining different kinds of static analyses: abstract interpretation, weakest precondition computation and quantifier elimination. An important originality of our approach is to proceed modularly, considering subprograms independently. The practical applicability of our approach is demonstrated on experiments performed on a library and two benchmarks of vulnerabilities of C code.

Ali Ayad
On formal methods for certifying floating-point C programs [link]
In Research Report RR-6927, INRIA, 2009

This paper presents an implementation of an extension of the ACSL specication language in the Frama-C tool in order to prove the correctness of floating-point C programs. A first model checks that there is no over flow, i.e., proof obligations are generated by the Why tool to prove that the result of a fl oating-point operation is not greater than the maximal fl oat allowed in the given type, this model is called the Strict model. A second model, called the Full model, extends the Strict model. The Full model allows over flows and deals with special values: signed infinities, NaNs (Not-a-Number) and signed zeros as in the IEEE-754 Standard. The verification conditions generated by Why are (partially) proved by automatic theorem provers: Alt-Ergo, Simplify, Yices, Z3, CVC3 and Gappa or discharged in the interactive proof assistant Coq using two existing Coq formalization of fl oating-point arithmetic. When the Why proof obligations are written in the syntax of the Gappa library, we can use the gappa and interval tactics to achieve the proof. Several examples of fl oating-point C programs are presented in the paper to prove the efficiency of this implementation.

Yannick Moy
Sufficient Preconditions for Modular Assertion Checking [link]
In Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2008

Assertion checking is the restriction of program verification to validity of program assertions. It encompasses safety checking, which is program verification of safety properties, like memory safety or absence of overflows. In this paper, we consider assertion checking of program parts instead of whole programs, which we call modular assertion checking. Classically, modular assertion checking is possible only if the context in which a program part is executed is known. By default, the worst-case context must be assumed, which may impair the verification task. It usually takes user effort to detail enough the execution context for the verification task to succeed, by providing strong enough preconditions. We propose a method to automatically infer sufficient preconditions in the context of modular assertion checking of imperative pointer programs. It combines abstract interpretation, weakest precondition calculus and quantifier elimination. We instantiate this method to prove memory safety for C and Java programs, under some memory separation conditions.

Yannick Moy
Checking C Pointer Programs for Memory Safety [link]
In INRIA Research Report n°6334, 2007

We propose an original approach for checking memory safety of C pointer programs that do not include casts, structures, double indirection and memory deallocation. This involves first identifying aliasing and strings, which we do in a local setting rather than through a global analysis as it is done usually. Our separation analysis in particular is a totally new treatment of non-aliasing. We present for the first time two abstract lattices to deal with local pointer aliasing and local pointer non-aliasing in an abstract interpretation framework. The key feature of our work is to combine abstract interpretation techniques and deductive verification. The approach is modular and contextual, thanks to the use of Hoare-style annotations (pre- and postconditions), allowing to verify each C function independently. Abstract interpretation techniques are used to automatically generate such annotations, in an idiomatic way: standard practice of C programming is identified and incorporated as heuristics. Abstract interpretation and deductive verification are both used to check these annotations in a sound way. Our first contribution is the design of an abstract domain for implications, which makes it possible to build efficient contextual analyses. Our second contribution is an efficient back-and-forth propagation method to generate contextual annotations in a modular way, in the framework of abstract interpretation. It considers the safety conditions to prove as a starting point, which focuses the analysis on the paths of interest. Thanks to previously unknown loop refinement operators, this propagation method does not require iterating around loops. We implemented our method in Caduceus, a tool for the verification of C programs, and successfully verified automatically the C standard string library functions.

Yannick Moy, Claude Marché
Inferring local (non-)aliasing and strings for memory safety [link]
In Proceedings of Heap Analysis and Verification (HAV), 2007

We propose an original approach for checking memory safety of C pointer programs, by combining deductive verification and abstract interpretation techniques. The approach is modular and contextual, thanks to the use of Hoare-style annotations (pre- and postconditions), allowing us to verify each C function independently. Deductive verification is used to check these annotations in a sound way. Abstract interpretation techniques are used to automatically generate such annotations, in an idiomatic way: standard practice of C programming is identified and incorporated as heuristics. Our first contribution is a set of techniques for identifying aliasing and strings, which we do in a local setting rather than through a global analysis as it is done usually. Our separation analysis in particular is a totally new treatment of non-aliasing. We present for the first time two abstract lattices to deal with local pointer aliasing and local pointer non-aliasing in an abstract interpretation framework. Our second contribution is the design of an abstract domain for implications, which makes it possible to build efficient contextual analyses. Our last contribution is an efficient back-and-forth propagation method to generate contextual annotations in a modular way, in the framework of abstract interpretation. We implemented our method in Caduceus, a tool for the verification of C programs, and successfully generated appropriate annotations for the C standard string library functions.

Thierry Hubert, Claude Marché
Separation analysis for deductive verification [link]
In Proceedings of Heap Analysis and Verification (HAV), 2007
Yannick Moy
Union and Cast in Deductive Verification [link]
In Proceedings of the C/C++ Verification Workshop (CCV), 2007

Deductive verification based on weakest-precondition calculus has proved effective at proving imperative programs, through a suitable encoding of memory as functional arrays (a.k.a. the Burstall-Bornat model). Unfortunately, this encoding of memory makes it impossible to support features like union and cast in C. We show that an interesting subset of those unions and casts can be encoded as structure subtyping, on which it is possible to extend the Burstall- Bornat encoding. We present an automatic translation from C to an intermediate language Jessie on which this extended interpretation is performed

Tutorials

Nikolai Kosmatov, Virgile Prevosto, Julien Signoles
A Lesson on Proof of Programs with Frama-C [link]
In International Conference on Runtime Verification (RV), 2013

Recent advances on proof of programs based on deductive methods allow verification tools to be successfully integrated into industrial verification processes. However, their usage remains mostly confined to the verification of the most critical software. One of the obstacles to their deeper penetration into industry is the lack of engineers properly trained in formal methods. A wider use of formal verification methods and tools in industrial verification requires their wider teaching and practical training for software engineering students as well as professionals.

This tutorial paper presents a lesson on proof of programs in the form of several exercises followed by their solutions. It is based on our experience in teaching at several French universities over the last four years. This experience shows that, for the majority of students, theoretical courses (like lectures on Hoare logic and weakest precondition calculus) are insufficient to learn proof of programs. We discuss the difficulties of the lesson for a student, necessary background, most frequent mistakes, and emphasize some points that often remain misunderstood. This lesson assumes that students have learned the basics of formal specification such as precondition, postcondition, invariant, variant, assertion.

Nikolai Kosmatov, Virgile Prevosto, Julien Signoles
Specification and Proof of Programs with Frama-C [link]
In 28th Symposium on Applied Computing (SAC), 2013

Others

Alwyn Goodloe, César A. Muñoz, Florent Kirchner, Loïc Correnson
Verification of Numerical Programs: From Real Numbers to Floating Point Numbers [link]
In NASA Formal Methods (NFM), 2013

Usually, proofs involving numerical computations are conducted in the infinitely precise realm of the field of real numbers. However, numerical computations in these algorithms are often implemented using floating point numbers. The use of a finite representation of real numbers introduces uncertainties as to whether the properties verified in the theoretical setting hold in practice. This short paper describes work in progress aimed at addressing these concerns. Given a formally proven algorithm, written in the Program Verification System(PVS), the Frama-C suite of tools is used to identify sufficient conditions and verify that under such conditions the rounding errors arising in a C implementation of the algorithm do not affect its correctness. The technique is illustrated using an algorithm for detecting loss of separation among aircraft.

Murat Torlakcik
Contracts in OpenBSD [link]
In University College Dublin, Master Report, 2010
Jochen Burghardt, Jens Gerlach, Hans Pohl, Juan Soto
An Experience Report on the Verification of Algorithms in the C++ Standard Library using Frama-C
In First Proceedings of International Conference of Formal Verification of Object-Oriented Software (FoVeOOS), 2010

Over the past few years, we have been conducting assessment studies to determine the utility of the Frama-C/Jessie platform of software analyzers (in conjunction with automatic theorem provers) for the formal verification of software. In this experience report, we discuss experiments in the verification of algorithms in the C++ Standard Library based on tool-supported Hoare-style weakest precondition computations to formally prove ACSL (ANSI/ISO C Specification Language) properties. Often automated provers are unable to perform inductive proofs. Hence, we introduce an approach to guide automated provers to find an inductive proof using auxiliary C-code corresponding to the proof structure. We also present a method to verify that a function only permutes the contents of an array, and obtain the relation between the pre- and post-index for each array element for use in later specification properties. Furthermore, we describe an approach to prove the essential properties of a function independent of each other, supplying for each task only the assumptions actually needed, i.e., related to the current goal. This approach reduces the proof search space and leads to higher verification rates for automatic provers. However, additional methods and tool support are desired to overcome drawbacks from a software engineering point of view. Finally, we sketch some ideas for an extension of ACSL for C++.

Stéphane Duprat, Pierre Gaufillet, Victoria Moya Lamiel, Frédéric Passarello
Formal verification of SAM state machine implementation [link]
In Proceedings of Embedded Real Time Software and Systems (ERTS²), 2010

This paper reports the results of an experiment about the formal verification of source code made according to an EMF model. Models define the semantics of a system whereas the source code defines its implementation. We applied this solution to a model of Automaton in SAM language and its C language implementation. The technical environment is close to an industrial operational context and all the tools are available. The experimentation has succeeded and has to be consolidated with bigger cases before an introduction in the operational development process. More generally, this solution must be extended to other model languages.

Franck Butelle, Florent Hivert, Micaela Mayero, Frédéric Toumazet
Formal Proof of SCHUR Conjugate Function [link]
In Symposium on the Integration of Symbolic Computation and Mechanised Reasoning (CALCULEMUS), 2010

The main goal of our work is to formally prove the correctness of the key commands of the SCHUR software, an interactive program for calculating with characters of Lie groups and symmetric functions. The core of the computations relies on enumeration and manipulation of combinatorial structures. As a first “proof of concept”, we present a formal proof of the conjugate function, written in C. This function computes the conjugate of an integer partition. To formally prove this program, we use the Frama-C software. It allows us to annotate C functions and to generate proof obligations, which are proved using several automated theorem provers. In this paper, we also draw on methodology, discussing on how to formally prove this kind of program.

PILAT

Theses

Steven de Oliveira
Finding constancy in linear routines [link] [BibTeX]
@phdthesis{2018_deoliveira_phd,
title = "Finding constancy in linear routines",
author = "de Oliveira, Steven",
year = "2018",
url = "https://www.theses.fr/2018SACLS207",
school = "Université Paris-Saclay",
}
Université Paris-Saclay, PhD Thesis, 2018

The criticality of programs constantly reaches new boundaries as they are relied on to take decisions in place of the user (autonomous cars, robot surgeon, etc.). This raised the need to develop safe programs and to verify the already existing ones.Anyone willing to formally prove the soundness of a program faces the two challenges of scalability and undecidability. Million of lines of code, complexity of the algorithm, concurrency, and even simple polynomial expressions are part of the issues formal verification have to deal with. In order to succeed, formal methods rely on state abstraction to analyze approximations of the behavior of the analyzed program.The analysis of loops is a full axis of formal verification, as this construction is still today not well understood. Though some of them can be easily handled when they perform simple operations, there still exist some seemingly basic loops whose behavior has not been solved yet (the Syracuse sequence for example is suspected to be undecidable).The most common approach for the treatment of loops is the use of loop invariants, i.e. relations on variables that are true at the beginning of the loop and after every step. In general, invariants are expected to use the same set of expressions used in the loop: if a loop manipulates the memory on a structure for example, invariants will naturally use expressions involving memory operations. However, there exist loops containing only linear instructions that admit only polynomial invariants (for example, the sum on integers ∑_{i=0}^n i can be computed by a linear loop and is a degree 2 polynomial in n), hence using expressions that are syntacticallyabsent of the loop. Is the previous remark wrong then ?This thesis presents new insights on loops containing linear and polynomial instructions. It is already known that linear loops are polynomially expressive, in the sense that if a variable evolves linearly, then any monomial of this variable evolves linearly. The first contribution of this thesis is the extraction of a class of polynomial loops that is exactly as expressive as linear loops, in the sense that there exist a linear loop with the exact same behavior. Then, two new methods for generating invariants are presented.The first method is based on abstract interpretation and is focused on a specific kind of linear loops called linear filters. Linear filters play a role in many embedded systems (plane sensors for example) and require the use of floating point operations, that may be imprecise and lead to errors if they are badly handled. Also, the presence of non deterministic assignments makes their analysis even more complex.The second method treats of a more generic subject by finding a complete set of linear invariants of linear loops that is easily computable. This technique is based on the linear algebra concept of eigenspace. It is extended to deal with conditions, nested loops and non determinism in assignments.Generating invariants is an interesting topic, but it is not an end in itself, it must serve a purpose. This thesis investigates the expressivity of invariantsgenerated by the second method by generating counter examples for the Kannan-Lipton Orbit problem.It also presents the tool PILAT implementing this technique and compares its efficiency technique with other state-of-the-art invariant synthesizers. The effective usefulness of the invariants generated by PILAT is demonstrated by using the tool in concert with CaFE, a model-checker for C programs based on temporal logics.

Foundational

Steven de Oliveira, Virgile Prevosto, Peter Habermehl, Saddek Bensalem
Left-Eigenvectors Are Certificates of the Orbit Problem. [link]
In Reachability Problems (RP), 2018

This paper investigates the connexion between the Kannan-Lipton Orbit Problem and the polynomial invariant generator algorithm PILA based on eigenvectors computation. Namely, we reduce the problem of generating linear and polynomial certificates of non-reachability for the Orbit Problem for linear transformations with rational coefficients to the generalized eigenvector problem. Also, we prove the existence of such certificates for any transformation with integer coefficients, which is not the case with rational coefficients.

Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
Synthesizing invariants by solving solvable loops [link]
In Automated Technology for Verification and Analysis (ATVA), 2017
Extension of the PILAT technique to polynomial inequalities

Formal program verification faces two problems. The first problem is related to the necessity of having automated solvers that are powerful enough to decide whether a formula holds for a set of proof obligations as large as possible, whereas the second manifests in the need of finding sufficiently strong invariants to obtain correct proof obligations. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial and non deterministic assignments. This technique is based on the eigenvector generation for a given linear transformation and on the polynomial optimization problem, which we implemented on top of the open-source tool Pilat.

Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
Polynomial Invariants by Linear Algebra [link]
In Automated Technology for Verification and Analysis (ATVA), 2016
Presentation of a loop invariant generation technique to discover polynomial relations between numerical variables

We present in this paper a new technique for generating polynomial invariants, divided in two independent parts: a procedure that reduces polynomial assignments composed loops analysis to linear loops under certain hypotheses and a procedure for generating inductive invariants for linear loops. Both of these techniques have a polynomial complexity for a bounded number of variables and we guarantee the completeness of the technique for a bounded degree which we successfully implemented for C programs verification.

SANTE

Foundational

Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti, Jacques Julliand
Program slicing enhances a verification technique combining static and dynamic analysis [link]
In Proceedings of the 27th Symposium On Applied Computing (SAC), 2012

Recent research proposed efficient methods for software verification combining static and dynamic analysis, where static analysis reports possible runtime errors (some of which may be false alarms) and test generation confirms or rejects them. However, test generation may time out on real-sized programs before confirming some alarms as real bugs or rejecting some others as unreachable. To overcome this problem, we propose to reduce the source code by program slicing before test generation. This paper presents new optimized and adaptive usages of program slicing, provides underlying theoretical results and the algorithm these usages rely on. The method is implemented in a tool prototype called sante (Static ANalysis and TEsting). Our experiments show that our method with program slicing outperforms previous combinations of static and dynamic analysis. Moreover, simplifying the program makes it easier to analyze detected errors and remaining alarms.

Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti, Jacques Julliand
The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging [link]
In Proceedings of the 5th International Conference on Tests & Proofs (TAP), 2011

This short paper presents a prototype tool called SANTE (Static ANalysis and TEsting) implementing an original method combining value analysis, program slicing and structural test generation for verification of C programs. First, value analysis is called to generate alarms when it can not guarantee the absence of errors. Then the program is reduced by program slicing. Alarm-guided test generation is then used to analyze the simplified program(s) in order to confirm or reject alarms.

Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti, Jacques Julliand
Combining static analysis and test generation for C program debugging [link]
In Proceedings of the 4th International Conference on Tests & Proofs (TAP), 2010

This paper presents our ongoing work on a tool prototype called SANTE (StaticANalysis and TEsting), implementing a combination of static analysis and structural program testing for detection of run-time errors in C programs. First, a static analysis tool (Frama-C) is called to generate alarms when it cannot ensure the absence of run-time errors. Second, these alarms guide a structural test generation tool (PathCrawler) trying to confirm alarms by activating bugs on sometest cases.Our experiments on real-life software showthat this combination can outperform the use of each technique independently.

Omar Chebaro
Outil SANTE : Détection d’erreurs par analyse statique et test structurel des programmes C
In Proceedings of 10iemes Journées Francophones Internationales sur les Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2010
In French.

Ce papier présente un prototype appelé SANTE (Static ANalysis and TEsting), qui implémente une nouvelle méthode combinant l’analyse statique et le test structurel pour la détection des erreurs à l’exécution dans les programmes C. Tout d’abord, un outil d’analyse statique (Frama-C) est appelé pour générer des alarmes lorsqu’il ne peut pas garantir l’absence d’erreurs à l’exécution. Ensuite ces alarmes guident la génération de tests structurels dans PathCrawler qui va essayer de confirmer les alarmes en activant des bugs sur certains cas de test.

SIDAN

Foundational

Jonathan-Christopher Demay, Éric Totel, Frédéric Tronel
SIDAN: a tool dedicated to Software Instrumentation for Detecting Attacks on Non-control-data [link]
In 4th International Conference on Risks and Security of Internet and Systems (CRISIS), 2009

Anomaly based intrusion detection systems rely on the build of a normal behavior model. When a deviation from this normal behavior is detected, an alert is raised. This anomaly approach, unlike the misuse approach, is able to detect unknown attacks. A basic technique to build such a model for a program is to use the system call sequences of the process. To improve the accuracy and completeness of this detection model, we can add information related to the system call, such as its arguments or its execution context. But even then, attacks that target non-control-data may be missed and attacks on control-data may be adapted to bypass the detection mechanism using evasion techniques. We propose in this article an approach that focuses on the detection of non-control-data attacks. Our approach aims at exploiting the internal state of a program to detect a memory corruption on non-control-data that could lead to an illegal system call. To achieve this, we propose to build a data-oriented detection model by statically analyzing a program source code. This model is used to instrument the program by adding reasonableness checks that verify the consistent state of the data items the system calls depend on. We thus argue that it is possible to detect a program misuse issued by a non-control-data attack inside the program during its execution. While keeping a low overhead, this approach allows to detect non-control-data attacks.

STAC

Foundational

Dumitru Ceara, Laurent Mounier, Marie-Laure Potet
Taint Dependency Sequences: a characterization of insecure execution paths based on input-sensitive cause sequences [link]
In Modeling and Detecting Vulnerabilities workshop (MDV), 2010

Numerous software vulnerabilities can be activated only with dedicated user inputs. Taint analysis is a security check which consists in looking for possible dependency chains between user inputs and vulnerable statements (like array accesses). Most of the existing static taint analysis tools produce some warnings on potentially vulnerable program locations. It is then up to the developer to analyze these results by scanning the possible execution paths that may lead to these locations with unsecured user inputs. We present a Taint Dependency Sequences Calculus, based on a fine-grain data and control taint analysis, that aims to help the developer in this task by providing some information on the set of paths that need to be analyzed. Following some ideas introduced in, we also propose some metrics to characterize these paths in term of “dangerousness”. This approach is illustrated with the help of the Verisec Suite and by describing a prototype, called STAC.

StaDy

Foundational

Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand
How testing helps to diagnose proof failures [link]
In Formal Aspects of Computing, vol. 30 issue 6, 2018
Extended version of "Your Proof Fails? Testing Helps to Find the Reason".

Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a C program formally specified in an executable specification language into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in StaDy, a plugin of the software analysis platform Frama-C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures.

Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand
Your Proof Fails? Testing Helps to Find the Reason [link]
In International Conference on Tests and Proofs (TAP), 2016

Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedback in case of proof failures. Along with a non-compliance between the code and its specification (due to an error in at least one of them), possible reasons of a proof failure include a missing or too weak specification for a called function or a loop, and lack of time or simply incapacity of the prover to finish a particular proof. This work proposes a complete methodology where test generation helps to identify the reason of a proof failure and to exhibit a counterexample clearly illustrating the issue. We define the categories of proof failures, introduce two subcategories of contract weaknesses (single and global ones), and examine their properties. We describe how to transform a formally specified C program into C code suitable for testing, and illustrate the benefits of the method on comprehensive examples. The method has been implemented in StaDy, a plugin of the software analysis platform Frama-C. Initial experiments show that detecting non-compliances and contract weaknesses allows to precisely diagnose most proof failures.

Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand
How Test Generation Helps Software Specification and Deductive Verification in Frama-C [link]
In International Conference on Tests and Proofs (TAP), 2014

This paper describes an incremental methodology of deductive verification assisted by test generation and illustrates its benefits by a set of frequent verification scenarios. We present StaDy, a new integration of the concolic test generator PathCrawler within the software analysis platform Frama-C . This new plugin treats a complete formal specification of a C program during test generation and provides the validation engineer with a helpful feedback at all stages of the specification and verification tasks.

Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti, Jacques Julliand
Instrumentation of Annotated C Programs for Test Generation [link]
In 14th International Working Conference on Source Code Analysis and Manipulation (SCAM), 2014

Software verification and validation often rely on formal specifications that encode desired program properties. Recent research proposed a combined verification approach in which a program can be incrementally verified using alternatively deductive verification and testing. Both techniques should use the same specification expressed in a unique specification language. This paper addresses this problem within the Frama-C framework for analysis of C programs, that offers ACSL as a common specification language. We provide a formal description of an automatic translation of ACSL annotations into C code that can be used by a test generation tool either to trigger and detect specification failures, or to gain confidence, or, under some assumptions, even to confirm that the code is in conformity with respect to the annotations. We implement the proposed specification translation in a combined verification tool Study. Our initial experiments suggest that the proposed support for a common specification language can be very helpful for combined static-dynamic analyses.

Taster

Foundational

David Delmas, Stéphane Duprat, Victoria Moya Lamiel, Julien Signoles
Taster, a Frama-C plug-in to enforce Coding Standards [link]
In Proceedings of Embedded Real Time Software and Systems (ERTS²), 2010

Enforcing Coding Standards is part of the traditional concerns of industrial software developments. In this paper, we present a framework based on the open source Frama-C platform for easily developing syntactic, typing (and even some semantic) analyses of C source code, among which conformance to Coding Standards. We report on our successful attempt to develop a Frama-C plug-in named Taster, in order to replace a commercial, off-the-shelf, legacy tool in the verification process of several Airbus avionics software products. We therefore present the types of coding rules to be verified, the Frama-C platform and the Taster plug-in. We also discuss ongoing industrial deployment and qualification activities.

Theses related to Frama-C

Virgile Robles
Specifying and verifying high-level requirements on large programs : application to security of C programs [link] [BibTeX]
@phdthesis{2022_robles_phd,
title = "Specifying and verifying high-level requirements on large programs : application to security of C programs",
author = "Robles, Virgile",
year = "2022",
url = "https://www.theses.fr/2022UPAST001",
school = "Université Paris-Saclay",
}
Université Paris-Saclay, PhD Thesis, 2022

Specification and verification of highlevel requirements (such as security properties like data integrity or confidentiality) remains an important challenge for the industrial practice, despite being a major part of functional specifications. This thesis presents a formal framework for their expression called meta-properties, supported by a description on an abstract programming language, focusing on properties related to memory and global invariants. This framework is then applied to the C programming language, introducing the HILARE extension to ACSL, to allow easy specification of these requirements on large C programs. Verification techniques for HILARE, based on local assertion generation and reuse of the existing Frama-C analyzers, are presented and implemented into the MetAcsl plugin for Frama-C. A complete methodology for assessing large programs is laid out, articulating meta-properties, verification techniques and quirks specific to the C programming language. This methodology is illustrated to a complex case study involving the bootloader of WooKey, a secure USB storage device. Finally, we explore another way to verify a high-level requirement deducing it from others, through a formal system proven in Why3 and integrated in MetAcsl.

Thibault Martin
Techniques de test pour des critères de couverture avancés [link] [BibTeX]
@phdthesis{2022_martin_phd,
title = "Techniques de test pour des critères de couverture avancés",
author = "Martin, Thibault",
year = "2022",
url = "https://www.theses.fr/2022UPASG077",
school = "Université Paris-Saclay",
}
Université Paris-Saclay, PhD Thesis, 2022

At a time where software are omnipresent in our daily life, verifying their safety and security present an important challenge for the industry. The most used technique to ensure that a software meets certain requirements is testing, where we run the program with some controlled input sets. A major issue is then to ensure that these input sets cover enough different situations. Many proposals have been made, called coverage criteria, which define test objectives through which at least one execution must pass during tests. In this thesis, we examine different possibilities to combine formal methods (mathematical techniques) and testing in order to improve the efficiency of the testing process. We focused our efforts on dataflow criteria, which observe the behavior of definitions and uses of each variables in the program, and the detection of polluting objectives for these criteria.We proposed several techniques, with their implementations and evaluations on real C programs. We then studied the impact of these dataflow criteria on test generation. Finally, we conclude by designing a method, using polluting objectives detection, to verify the effectiveness of countermeasures against fault injection attacks, and thus find errors in their implementation. This method was applied to the bootloader of WooKey, an encrypted storage device.

Dara Ly
Formalisation d'un vérificateur dynamique de propriétés mémoire pour programmes C [link] [BibTeX]
@phdthesis{2022_ly_phd,
title = "Formalisation d'un vérificateur dynamique de propriétés mémoire pour programmes C",
author = "Ly, Dara",
year = "2022",
url = "https://www.theses.fr/s265339",
school = "University of Orléans",
}
University of Orléans, PhD Thesis, 2022

Runtime Assertion Checking is a program verification technique allowing to monitor programs during their execution, in order to check their validity with respect to some specification expressed as assertions, that is, formal annotations inserted in the source code. Assertions are translated into executable code through a process called instrumentation, thus implementing an inline monitor for the program. During execution, the monitor checks whether the program complies with its assertions, and aborts the execution in case of violation of an assertion. If no such violation occurs, the program’s functional behavior is unchanged. Instrumenting a program is a process whose implementation complexity is strongly related to the expressiveness of the annotation language. For C programs, the E-ACSL plugin of Frama-C, an open-source analysis platform for C programs, can express properties related to the memory state of the program, at the cost of a complex instrumentation. In this thesis, we present a formalization of the instrumentation process, that is, a description accurate enough to enable formal reasoning about the semantic properties of the instrumentation. The problem is modeled as a translation, from a source language with logical assertions, to a target language. The latter has no logical assertions, instead featuring a data-structure we call observation memory, which is designed to keep track of memory properties. We present an axiomatic characterization of observation memory, and use it to define the translation’s target language semantics. The translation is then proved correct with regards to the respective semantics of source and target languages. In addition, we study an optimization of the instrumentation through data-flow analysis. This optimization is implemented in E-ACSL in order to mitigate the performance costs of the instrumentation. The analysis aims at identifying a minimal subset of memory locations, whose instrumentation suffices for the monitor to evaluate the program’s assertions soundly. We define such an analysis and prove its soundness, meaning that restricting the instrumentation to memory locations computed by the analysis does not threaten the validity of the monitor’s verdicts.

Lionel Blatter
Relational properties for specification and verification of C programs in Frama-C [link] [BibTeX]
@phdthesis{2019_thesis_blatter,
title = "Relational properties for specification and verification of C programs in Frama-C",
author = "Blatter, Lionel",
year = "2019",
url = "http://www.theses.fr/2019SACLC065",
school = "University of Paris Saclay",
}
University of Paris Saclay, PhD Thesis, 2019
Steven de Oliveira
Finding constancy in linear routines [link] [BibTeX]
@phdthesis{2018_deoliveira_phd,
title = "Finding constancy in linear routines",
author = "de Oliveira, Steven",
year = "2018",
url = "https://www.theses.fr/2018SACLS207",
school = "Université Paris-Saclay",
}
Université Paris-Saclay, PhD Thesis, 2018

The criticality of programs constantly reaches new boundaries as they are relied on to take decisions in place of the user (autonomous cars, robot surgeon, etc.). This raised the need to develop safe programs and to verify the already existing ones.Anyone willing to formally prove the soundness of a program faces the two challenges of scalability and undecidability. Million of lines of code, complexity of the algorithm, concurrency, and even simple polynomial expressions are part of the issues formal verification have to deal with. In order to succeed, formal methods rely on state abstraction to analyze approximations of the behavior of the analyzed program.The analysis of loops is a full axis of formal verification, as this construction is still today not well understood. Though some of them can be easily handled when they perform simple operations, there still exist some seemingly basic loops whose behavior has not been solved yet (the Syracuse sequence for example is suspected to be undecidable).The most common approach for the treatment of loops is the use of loop invariants, i.e. relations on variables that are true at the beginning of the loop and after every step. In general, invariants are expected to use the same set of expressions used in the loop: if a loop manipulates the memory on a structure for example, invariants will naturally use expressions involving memory operations. However, there exist loops containing only linear instructions that admit only polynomial invariants (for example, the sum on integers ∑_{i=0}^n i can be computed by a linear loop and is a degree 2 polynomial in n), hence using expressions that are syntacticallyabsent of the loop. Is the previous remark wrong then ?This thesis presents new insights on loops containing linear and polynomial instructions. It is already known that linear loops are polynomially expressive, in the sense that if a variable evolves linearly, then any monomial of this variable evolves linearly. The first contribution of this thesis is the extraction of a class of polynomial loops that is exactly as expressive as linear loops, in the sense that there exist a linear loop with the exact same behavior. Then, two new methods for generating invariants are presented.The first method is based on abstract interpretation and is focused on a specific kind of linear loops called linear filters. Linear filters play a role in many embedded systems (plane sensors for example) and require the use of floating point operations, that may be imprecise and lead to errors if they are badly handled. Also, the presence of non deterministic assignments makes their analysis even more complex.The second method treats of a more generic subject by finding a complete set of linear invariants of linear loops that is easily computable. This technique is based on the linear algebra concept of eigenspace. It is extended to deal with conditions, nested loops and non determinism in assignments.Generating invariants is an interesting topic, but it is not an end in itself, it must serve a purpose. This thesis investigates the expressivity of invariantsgenerated by the second method by generating counter examples for the Kannan-Lipton Orbit problem.It also presents the tool PILAT implementing this technique and compares its efficiency technique with other state-of-the-art invariant synthesizers. The effective usefulness of the invariants generated by PILAT is demonstrated by using the tool in concert with CaFE, a model-checker for C programs based on temporal logics.

Julien Signoles
From Static Analysis to Runtime Verification with Frama-C and E-ACSL [link] [BibTeX]
@phdthesis{2018_thesis_signoles,
title = "From Static Analysis to Runtime Verification with Frama-C and E-ACSL",
author = "Signoles, Julien",
year = "2018",
url = "https://julien-signoles.fr/publis/hdr.pdf",
school = "University of Paris Sud",
}
University of Paris Sud, Habilitation Thesis, 2018
David Bühler
EVA, an Evolved Value Analysis for Frama-C: structuring an abstract interpreter through value and state abstractions [link] [BibTeX]
@phdthesis{2017_thesis_buhler,
title = "EVA, an Evolved Value Analysis for Frama-C: structuring an abstract interpreter through value and state abstractions",
author = "Bühler, David",
year = "2017",
url = "http://www.theses.fr/2017REN1S016",
school = "University of Rennes 1",
}
University of Rennes 1, PhD Thesis, 2017
Allan Blanchard
Aide à la vérification de programmes concurrents par transformation de code et de spécifications [link] [BibTeX]
@phdthesis{2016_blanchard_phd,
title = "Aide à la vérification de programmes concurrents par transformation de code et de spécifications",
author = "Blanchard, Allan",
year = "2016",
url = "https://www.theses.fr/2016ORLE2073",
school = "University of Orléans",
}
University of Orléans, PhD Thesis, 2016

Formal verification of concurrent programs is a hard task. There exists different methods to perform such a task, but very few are applied to the verification of programs written using real life programming languages. On the other side, formal verification of sequential programs is successfully applied for many years, and allows to get high confidence in our systems. As an alternative to dedicated concurrent program analyses, we propose a method to transform concurrent programs into sequential ones to make them analyzable by tools dedicated to sequential programs. This work takes place within the analysis framework FRAMA-C, dedicated to the analysis of C code specified with ACSL. The different analyses provided by FRAMA-C are plugins to the framework, which are currently mostly dedicated to sequential programs. We apply this method to the verification of a concurrent code taken from an hypervisor. We describe the automation of the method implemented by a new plugin to FRAMAC that allow to produce, from a specified concurrent program, an equivalent specified sequential program. We present the basis of a formalization of the method with the objective to prove its validity. This validity is admissible only for the class of sequentially consistent programs. So, we finally propose a prototype of constraint solver for weak memory models, which is able to determine whether a program is in this class or not, depending on the targeted hardware.

Mounir Assaf
From qualitative to quantitative program analysis: permissive enforcement of secure information flow [link] [BibTeX]
@phdthesis{2015_thesis_assaf,
title = "From qualitative to quantitative program analysis: permissive enforcement of secure information flow",
author = "Assaf, Mounir",
year = "2015",
url = "http://www.theses.fr/2015REN1S003",
school = "University of Rennes 1",
}
University of Rennes 1, PhD Thesis, 2015
François Bobot
Logique de séparation et vérification déductive [link] [BibTeX]
@phdthesis{2011_thesis_bobot,
title = "Logique de séparation et vérification déductive",
author = "Bobot, François",
year = "2011",
url = "http://proval.lri.fr/publications/bobot11these.pdf",
school = "University of Paris Sud",
}
University of Paris Sud, PhD Thesis, 2011
Romain Bardou
Verification of Pointer Programs Using Regions and Permissions. [link] [BibTeX]
@phdthesis{2011_thesis_bardou,
title = "Verification of Pointer Programs Using Regions and Permissions.",
author = "Bardou, Romain",
year = "2011",
url = "http://proval.lri.fr/publications/bardou11phd.pdf",
school = "University of Paris Sud",
}
University of Paris Sud, PhD Thesis, 2011
Yannick Moy
Automatic Modular Static Safety Checking for C Programs [link] [BibTeX]
@phdthesis{2009_thesis_moy,
title = "Automatic Modular Static Safety Checking for C Programs",
author = "Moy, Yannick",
year = "2009",
url = "http://www.lri.fr/~marche/moy09phd.pdf",
school = "University of Paris Sud",
}
University of Paris Sud, PhD Thesis, 2009