Loïc Correnson, Pascal Cuoq, Florent Kirchner, André Maroneze, Virgile Prevosto, Armand Puccetti, Julien Signoles, and Boris Yakobowski Frama-C User Manual [link] The manual introducing common features to all analyzers.
Julien Signoles, Thibaud Antignac, Loïc Correnson, Matthieu Lemerre, and Virgile Prevosto Frama-C Plug-in Development Guide [link] The manual for developing a Frama-C plug-in.
Patrick Baudin, Jean-Christophe Filliâtre, Claude Marché, Benjamin Monate, Yannick Moy, and Virgile Prevosto ACSL: ANSI/ISO C Specification Language [link] The reference manual of ACSL, the specification language used by Frama-C.
Patrick Baudin, François Bobot, David Bühler, Loïc Correnson, Florent Kirchner, Nikolai Kosmatov, André Maroneze, Valentin Perrelle, Virgile Prevosto, Julien Signoles and 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, and 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, and 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 and 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, and 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, and 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.
Allan Blanchard, Nikolai Kosmatov, and 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 and 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
Plug-ins distributed with Frama-C
Eva, an Evolved Value Analysis
David Bühler, Pascal Cuoq, Boris Yakobowski, Matthieu Lemerre, André Maroneze, Valentin Perelle, and Virgile Prevosto Eva - The Evolved Value Analysis plug-in [link]
David Bühler EVA, an Evolved Value Analysis for Frama-C: structuring an abstract interpreter through value and state abstractions [link] In University of Rennes 1, PhD Thesis, 2017
Sandrine Blazy, David Bühler and Boris Yakobowski Structuring Abstract Interpreters Through State and Value Abstractions [link] In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2019 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 and 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.
Géraud Canet, Pascal Cuoq and 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 and 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.
Patrick Baudin, François Bobot, Loïc Correnson, Zaynah Dargaye, Allan Blanchard WP Plug-in Manual [link] The official manual for the WP plug-in.
Loïc Correnson Qed. Computing What Remains to Be Proved. 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.
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 and Tim Sikatzki ACSL by Example [link] A fairly complete tour of ACSL and WP features through various functions inspired from C++ STL.
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.
Virgile Prevosto, Nikolay Kosmatov and 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.
Pascal Cuoq, Benjamin Monate, Anne Pacalet and 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.
Julien Signoles, Basile Desloges and Kostyantyn Vorobyov E-ACSL User Manual [link] The official manual of the Frama-C plug-in E-ACSL.
Julien Signoles E-ACSL: Executable ANSI/ISO C Specification Language [link] The reference manual of the E-ACSL specification language.
Julien Signoles From Static Analysis to Runtime Verification with Frama-C and E-ACSL [link] In University of Paris Sud, Habilitation Thesis, 2018
Nikolai Kosmatov, Fonenantsoa Maurica and 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, and 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 and 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 and 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.
Nikolai Kosmatov and 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.
Thibaut Benjamin, Felix Ridoux and 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, and 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 and 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, and 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 and 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 and 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 and 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 and 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.
Nicolas Stouls Aoraï Plug-in Tutorial [link] The official manual of the Frama-C plug-in Aoraï.
Julien Groslambert and 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.
Benjamin Monate and 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
Michele Alberti and 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.
Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, and 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, and 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, and 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.
Michaël Marcozzi, Mike Papadakis, Sébastien Bardin, Nikolai Kosmatov, Virgile Prévosto, and 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.
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and 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, and 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 Automatic Test Generation Tool For C Programs User Manual [link] The user manual of the Frama-C plug-in PathCrawler.
Nicky Williams, Bruno Marre, Patricia Mouy and 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 and 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.
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 and 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.
Nikolai Kosmatov, Bernard Botella, Muriel Roger and 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 and 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 and 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 and 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.
Lionel Blatter Relational properties for specification and verification of C programs in Frama-C [link] In University of Paris Saclay, PhD Thesis, 2019
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prevosto and 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 and 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.
Mounir Assaf From qualitative to quantitative program analysis: permissive enforcement of secure information flow [link] In University of Rennes 1, PhD Thesis, 2015
Gergö Barany and 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, and 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.
Allan Blanchard, Nikolai Kosmatov and 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 and 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.
Allan Blanchard, Nikolai Kosmatov and 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.
Ahmed Bouajjani, Cezara Drăgoi, Constantin Enea and 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 and 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.
Nicolas Ayache, Roberto M. Amadio and 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.
Pascal Cuoq, David Delmas, Stéphane Duprat and 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 ressources [link] The main web page, including the manual and many other resources.
François Bobot Logique de séparation et vérification déductive [link] In Université Paris-Sud, PhD Thesis, 2011
Romain Bardou Verification of Pointer Programs Using Regions and Permissions. [link] In Université Paris-Sud, PhD Thesis, 2011
Yannick Moy Automatic Modular Static Safety Checking for C Programs [link] In Université Paris-Sud, PhD Thesis, 2009
Sylvie Boldo and Thi Minh Tuyen Nguyen Hardware-independent proofs of numerical programs [link] In Proceedings of the Second NASA Formal Methods Symposium (NFM), 2010
On recent 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. 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 and 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 and 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 and 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
Nikolai Kosmatov, Virgile Prevosto and 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 and Julien Signoles Specification and Proof of Programs with Frama-C [link] In 28th Symposium on Applied Computing (SAC), 2013
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 and 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 and 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 and 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.
Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and 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 and 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 and 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.
Jonathan-Christopher Demay, Éric Totel and 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.
Dumitru Ceara, Laurent Mounier and 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.
Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti and 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 and 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 and 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 and 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.
David Delmas, Stéphane Duprat, Victoria Moya Lamiel and 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.