Frama-C is a popular open-source toolset for analysis and verification of C programs, largely used for teaching, experimental research, and industrial applications. With the growing complexity and ubiquity of modern software, there is increasing interest in code analysis tools at various levels of formalization to ensure safety and security of software products. Acknowledging the fact that no single technique will ever be able to fit all software verification needs, the Frama-C platform features a wide set of plug-ins that can be used or combined for solving specific verification tasks.

This guidebook presents a large panorama of basic usages, research results, and concrete applications of Frama-C since the very first open-source release of the platform in 2008. It covers the ACSL specification language, core verification plug-ins, advanced analyses and their combinations, key ingredients for developing new plug-ins, as well as successful industrial case studies in which Frama-C has helped engineers verify crucial safety or security properties.

This chapter presents ACSL, the ANSI/ISO C Specification Language, focusing on its current implementation within the Frama-C framework. As its name suggests, ACSL is meant to express precisely and unambiguously the expected behavior of a piece of C code. It plays a central role in Frama-C, as nearly all plug-ins eventually manipulate ACSL specifications, either to generate properties that are to be verified, or to assess that the code is conforming to these specifications. It is thus very important to have a clear view of ACSL’s semantics in order to be sure that what you check with Frama-C is really what you mean. This chapter describes the language in an agnostic way, independently of the various verification plug-ins that are implemented in the platform, which are described in more details in other chapters. It contains many examples and exercises that introduce the main features of the language and insists on the most common pitfalls that users, even experienced ones, may encounter.

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.

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.

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.

This chapter provides an overview of the Frama-C distribution, including its main plugins that are covered in depth by other chapters. It mainly focuses on the Frama-C kernel and the main services that it offers to the user. This includes notably passing proper arguments to launch Frama-C and drive an analysis, controlling the parsing and code normalization phases of the analysis, and visualizing results.

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.

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.

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.

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.

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.

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.

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.

Frama-C can operate as an exploration framework: several plug-ins and scripts have been created to enable tool-assisted code exploration and understanding. Unassisted reviews of C code require deep expertise and knowledge of many of C’s pitfalls; Frama-C should help overcome many of its quirks, to help ensure that “all bugs are shallow”. Whether you want some simple metrics and an overview; or you need to quickly evaluate code written by others; or you seek deep understanding about the origin of a complex bug, several Frama-C plug-ins are available to help you. This chapter presents these plug-ins and provides pointers for further details.

One of the key features of Frama-C is its extensibility. More precisely, the platform is based on a kernel, which provides the core services and data structures that are needed for analyzing C programs, including in particular parsing C and ACSL code. Analyses themselves are then implemented by plug-ins, that use the kernel’s API to, among other things, access the code under analysis, perform some code transformation, add ACSL annotations, and validate (or invalidate) other ACSL annotations. Furthermore, plug-ins can also export their own API to be used by other plug-ins. In this chapter, we will give an overview of Frama-C’s general architecture and describe the main functionalities of the kernel, using as example a small plug-in that we build step by step during the course of the chapter.

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

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.

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

• Frama-C Overview: Slides, Simple plugin
• Value Analysis: Slides and Examples
• WP: Slides and Examples

Examples

This chapter provides an overview of the Eva plug-in of Frama-C, a static analyzer based on abstract interpretation, intended to automatically prove the absence of runtime errors in critical software. It aims at giving users a good understanding of how Eva works, by describing the theoretic principles underlying its analysis and by detailing its most important features. More practically, it also explains how to use Eva, set up an analysis and exploit its results.

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.

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.

This chapter presents how Frama-C verifies some complex loop invariant for numerical embedded code and how to produce such invariants. Numerical embedded code usually defines an endless loop that takes inputs from sensors and that emits outputs for actuators. Moreover, such a code commonly uses some floating-point global memories to keep track of the input or output values from the previous loop cycles. These memories store a summary of previous values to filter the input or the output over time. Hence, recursive linear or Infinite Impulse Response (IIR) filters are very common in such code. Among such filters, low-pass filters are challenging for Frama-C since finding a loop invariant with complex relationships between the variables is never an evident task for the engineer. Hence, this chapter presents different approaches to find and organize inductive invariants for such numerical reactive systems and shows how Frama-C can prove them with its Eva and Wp plug-ins. It also exposes optimal theoretical results for first-order and higher-order filters to compare the quality of results of the different solutions. Several examples and several concrete solutions illustrate the generation/writing of such inductive invariants and their formal verification.

Mitsubishi Electric R&D Centre Europe (MERCE), the advanced European research laboratory of Mitsubishi Electric group, has been carrying research activity on Formal Methods for more than 10 years now. MERCE applied various formal methods in its projects and, among them, MERCE conducted several extensive experiments with Frama-C, from safety to security applications, in different industrial domains. Through three of these experiments, namely industrial code verification, automated test generation and verification of an industrial firewall, this chapter gives some feedback on several Frama-C’s capabilities based on the plug-ins Eva, PathCrawler and Wp. Demonstrating the tractability of the solutions in industrial context is one of the leading issues when MERCE evaluates tools and methods. Frama-C appears as a mature technology which can be operated in very different contexts from classical testing to full-fledged formal functional verification.

The verification process is mandatory in the critical software realm. To improve this process, static analysis tools can make significant contributions. Static analysis meets a variety of goals, including error detection, security analysis, and program verification, which is why standards for critical software development recommend the use of static analysis to identify errors that are difficult to detect at run-time. Thus, this chapter presents a case study on the use of Frama-C as a static analyzer for formal verification of critical software and a lightweight semantic-extractor tool; the former uses an abstract interpretation technique, and the latter allows for the extraction of semantic information to provide a better understanding of source code. In practical terms, the chapter shows how Frama-C can support the development life cycle of an inertial system in aerospace applications, reporting a list of pros and cons. The final results indicate the benefits obtained in terms of software safety, software quality assurance and, consequently, the software verification process.

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.

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.

This chapter presents how to prove ACSL properties of C programs with the Wp plug-in of Frama-C using deductive verification and SMT solvers or Proof Assistants. Specifically, this chapter explores the internals of the Wp plug-in, with a specific focus on how ACSL and C are encoded into classical first-order logic, including its various memory models. Then, the internal proof strategy of Wp is described, which leads to a discussion on specification methodology and proof engineering, and how to interact with the Wp plug-in. Finally, we compare Wp with a selection of other amazing systems and logics for the deductive verification of C programs.

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.

• WebPage of the tutorial
• French PDF version
• French Online version
• GitHub

GitHub repository

LIFO’s website

Annotated files

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

Annotated files

Deductive verification provides a proof that, under the provided pre-conditions, each terminating execution of a given function satisfies the stated post-conditions. In general, pre- and post-conditions are expressed in a logical specification language and typically rely on theories including abstract definitions, axioms and lemmas. As they are written by humans, errors may be introduced into specifications. Some errors can be detected when the proof fails, but sometimes, they remain unnoticed due to misleading proofs: most of the program may become dead code under the provided pre-conditions, or the proof may succeed because of inconsistencies in hypotheses and axioms. In this tool paper, we explore how to detect such unwanted situations by using deductive verification techniques and describe the smoke test mechanism in Frama-C/WP, a popular deductive verifier for C code. We show that, while the intuitive idea is simple, making it practical requires optimizations to scale up, and report on experiments with critical industrial code. Although our method is based on proof techniques, it is not complete and is similar to testing. In the end, can we ever be sure that our programs are proved well enough?

Modern deductive verification tools succeed in automatically proving the great majority of program annotations thanks in particular to constantly evolving SMT solvers they rely on. The remaining proof goals still require interactively created proof scripts. This tool demo paper presents a new solution for an automatic creation of proof scripts in Frama-C/WP, a popular deductive verifier for C programs. The verification engineer defines a proof strategy describing several initial proof steps, from which proof scripts are automatically generated and applied. Our experiments on a large real-life industrial project confirm that the new proof strategy engine strongly facilitates the verification process by automating the creation of proof scripts, thus increasing the potential of industrial applications of deductive verification on large code bases.

Security of modern software has become a major concern. One example of highly critical software is smart card software since smart cards often play a key role in user authentication and controlling access to sensitive services and data. To demonstrate the compliance of a smart card product to security requirements, its certification according to the Common Criteria is often recommended or even required. The highest, most rigorous levels of Common Criteria certification include formal verification. In this chapter, we show how an industrial smart card product—a JavaCard Virtual Machine—has been formally verified by Thales using Frama-C, a software verification platform for C code. We describe the main steps of this verification project, illustrate target security properties, present some lessons learned and discuss several directions for future work and necessary tool enhancements.

Using tools for deductive verification, such as Frama-C, typically imposes substantial work overhead in the form of manually writing annotations. In this chapter, we investigate techniques for alleviating this problem by means of automatic inference of ACSL specifications. To this end, we present the Frama-C plugin Saida, which uses the assertion-based model checker TriCera as a back-end tool for inference of function contracts. TriCera transforms the program, and specifications provided as assume and assert statements, into a set of constrained Horn clauses (CHC), and relies on CHC solvers for the verification of these clauses. Our approach assumes that a C program consists of one entry-point (main) function and a number of helper functions, which are called from the main function either directly or transitively. Saida takes as input such a C program, where the main function is annotated with an ACSL function contract, and translates the contract into a harness function, comprised mainly of assume and assert statements. The harness function, together with the original program, is used as input for TriCera and, from the output of the CHC solver, TriCera infers pre- and post-conditions for all the helper functions in the C program, and translates them into ACSL function contracts. We illustrate on several examples how Saida can be used in practice, and discuss ongoing work on extending and improving the plugin.

This chapter presents how Frama-C verifies some complex loop invariant for numerical embedded code and how to produce such invariants. Numerical embedded code usually defines an endless loop that takes inputs from sensors and that emits outputs for actuators. Moreover, such a code commonly uses some floating-point global memories to keep track of the input or output values from the previous loop cycles. These memories store a summary of previous values to filter the input or the output over time. Hence, recursive linear or Infinite Impulse Response (IIR) filters are very common in such code. Among such filters, low-pass filters are challenging for Frama-C since finding a loop invariant with complex relationships between the variables is never an evident task for the engineer. Hence, this chapter presents different approaches to find and organize inductive invariants for such numerical reactive systems and shows how Frama-C can prove them with its Eva and Wp plug-ins. It also exposes optimal theoretical results for first-order and higher-order filters to compare the quality of results of the different solutions. Several examples and several concrete solutions illustrate the generation/writing of such inductive invariants and their formal verification.

Mitsubishi Electric R&D Centre Europe (MERCE), the advanced European research laboratory of Mitsubishi Electric group, has been carrying research activity on Formal Methods for more than 10 years now. MERCE applied various formal methods in its projects and, among them, MERCE conducted several extensive experiments with Frama-C, from safety to security applications, in different industrial domains. Through three of these experiments, namely industrial code verification, automated test generation and verification of an industrial firewall, this chapter gives some feedback on several Frama-C’s capabilities based on the plug-ins Eva, PathCrawler and Wp. Demonstrating the tractability of the solutions in industrial context is one of the leading issues when MERCE evaluates tools and methods. Frama-C appears as a mature technology which can be operated in very different contexts from classical testing to full-fledged formal functional verification.

Combinations of analysis techniques and tools can help verification engineers to achieve their goals. The Frama-C verification platform offers a large range of possibilities for combining its analyzers with each other or with external tools. This chapter provides an overview of several combinations with different objectives and levels of maturity. First, we show how model checking and Counterexample Guided Refinement Abstraction (CEGAR) are used with value analysis and deductive verification for proving statement contracts. Runtime assertion checking can provide the user with useful information by checking annotations on selected test inputs. Next, test generation can be used to classify alarms, explain proof failures and generate counterexamples. Finally, static techniques are capable to optimize test generation by detecting infeasible test objectives and thus avoiding a test generation tool to waste time by trying to cover them.

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.

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

Runtime Annotation Checking (RAC) is a lightweight formal method consisting in checking code annotations written in the source code during the program execution. While static formal methods aim for guarantees that hold for any execution of the analyzed program, RAC only provides guarantees about the particular execution it monitors. This allows RAC-based tools to be used to check a wide range of properties with minimum intervention from the user. Frama-C can perform RAC on C programs with the plug-in E-ACSL. This chapter presents RAC through practical use with E-ACSL, shows advanced uses of E-ACSL leveraging the collaboration with other plug-ins, and sheds some light on the internals of E-ACSL and the technical difficulties of implementing RAC.

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.

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.

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.

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.

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.

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é.

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.

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.

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.

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.

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.

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.

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.

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.

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.

The ACSL specification language allows the verification engineer to specify almost any property they might want to verify at any given point in a given C program. For some complex properties, it can sometimes be done at the price of an extremely complex encoding, which could quickly become error-prone if written manually. To facilitate this task, a certain number of Frama-C plug-ins offer dedicated specification languages, targeting different kinds of properties, that are then translated into a set of ACSL annotations amenable to verification via the core analysis plug-ins (Eva, Wp, E-ACSL). In this chapter, we present three such plug-ins. The first of them, MetAcsl, is dedicated to pervasive properties that must be checked at each program point meeting some characteristics, for instance at each write access. A single MetAcsl annotation can thus be instantiated by a very large number of ACSL clauses. Second, RPP targets relational properties. In contrast to an ACSL function contract, which specifies what happens during a single function call, relational properties express relations over several calls of potentially different functions. Finally, Aoraï is dedicated to properties over sequences of function calls that can occur during an execution.

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.

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.

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

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.

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.

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.

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.

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

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.

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.

Security of modern software has become a major concern. One example of highly critical software is smart card software since smart cards often play a key role in user authentication and controlling access to sensitive services and data. To demonstrate the compliance of a smart card product to security requirements, its certification according to the Common Criteria is often recommended or even required. The highest, most rigorous levels of Common Criteria certification include formal verification. In this chapter, we show how an industrial smart card product—a JavaCard Virtual Machine—has been formally verified by Thales using Frama-C, a software verification platform for C code. We describe the main steps of this verification project, illustrate target security properties, present some lessons learned and discuss several directions for future work and necessary tool enhancements.

The ACSL specification language allows the verification engineer to specify almost any property they might want to verify at any given point in a given C program. For some complex properties, it can sometimes be done at the price of an extremely complex encoding, which could quickly become error-prone if written manually. To facilitate this task, a certain number of Frama-C plug-ins offer dedicated specification languages, targeting different kinds of properties, that are then translated into a set of ACSL annotations amenable to verification via the core analysis plug-ins (Eva, Wp, E-ACSL). In this chapter, we present three such plug-ins. The first of them, MetAcsl, is dedicated to pervasive properties that must be checked at each program point meeting some characteristics, for instance at each write access. A single MetAcsl annotation can thus be instantiated by a very large number of ACSL clauses. Second, RPP targets relational properties. In contrast to an ACSL function contract, which specifies what happens during a single function call, relational properties express relations over several calls of potentially different functions. Finally, Aoraï is dedicated to properties over sequences of function calls that can occur during an execution.

Structural testing allows validation engineers to ensure that all parts of the program source code are activated (or covered) by the executed tests. The parts of code to be covered are determined by the choice of a coverage criterion. Automated test generation tools can be used effectively to generate test inputs satisfying a selected coverage criterion. This chapter presents PathCrawler, an automatic test generation tool for structural testing of C code, available as a plug-in of the Frama-C verification platform. We present the structural testing approach and describe the method implemented in PathCrawler and its usage in practice. The freely available online test generation service PathCrawler-online is presented as well. Finally, we discuss the place of testing in software verification and validation with respect to other Frama-C plug-ins and give an overview of various research, industrial and teaching activities using PathCrawler.

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.

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.

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.

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.

Mitsubishi Electric R&D Centre Europe (MERCE), the advanced European research laboratory of Mitsubishi Electric group, has been carrying research activity on Formal Methods for more than 10 years now. MERCE applied various formal methods in its projects and, among them, MERCE conducted several extensive experiments with Frama-C, from safety to security applications, in different industrial domains. Through three of these experiments, namely industrial code verification, automated test generation and verification of an industrial firewall, this chapter gives some feedback on several Frama-C’s capabilities based on the plug-ins Eva, PathCrawler and Wp. Demonstrating the tractability of the solutions in industrial context is one of the leading issues when MERCE evaluates tools and methods. Frama-C appears as a mature technology which can be operated in very different contexts from classical testing to full-fledged formal functional verification.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

The ACSL specification language allows the verification engineer to specify almost any property they might want to verify at any given point in a given C program. For some complex properties, it can sometimes be done at the price of an extremely complex encoding, which could quickly become error-prone if written manually. To facilitate this task, a certain number of Frama-C plug-ins offer dedicated specification languages, targeting different kinds of properties, that are then translated into a set of ACSL annotations amenable to verification via the core analysis plug-ins (Eva, Wp, E-ACSL). In this chapter, we present three such plug-ins. The first of them, MetAcsl, is dedicated to pervasive properties that must be checked at each program point meeting some characteristics, for instance at each write access. A single MetAcsl annotation can thus be instantiated by a very large number of ACSL clauses. Second, RPP targets relational properties. In contrast to an ACSL function contract, which specifies what happens during a single function call, relational properties express relations over several calls of potentially different functions. Finally, Aoraï is dedicated to properties over sequences of function calls that can occur during an execution.

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.

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.

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

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.

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.

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.

Combinations of analysis techniques and tools can help verification engineers to achieve their goals. The Frama-C verification platform offers a large range of possibilities for combining its analyzers with each other or with external tools. This chapter provides an overview of several combinations with different objectives and levels of maturity. First, we show how model checking and Counterexample Guided Refinement Abstraction (CEGAR) are used with value analysis and deductive verification for proving statement contracts. Runtime assertion checking can provide the user with useful information by checking annotations on selected test inputs. Next, test generation can be used to classify alarms, explain proof failures and generate counterexamples. Finally, static techniques are capable to optimize test generation by detecting infeasible test objectives and thus avoiding a test generation tool to waste time by trying to cover them.

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.

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.

One of the main features of C is manual management of memory, which explains the domination of C in systems and performance-critical code. The downside of manual memory management is that designing data structures requires reasoning about custom memory invariants, and that any mistake may lead to severe cybersecurity vulnerabilities. In this chapter, we present two Frama-C plug-ins, the Codex and RMA plug-ins, respectively based on physical refinement types and separation logic, that help verify properties of C programs manipulating data structures in memory with minimal guidance from the user.

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.

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

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.

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

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.

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.

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.

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.

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.

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

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.

The verification process is mandatory in the critical software realm. To improve this process, static analysis tools can make significant contributions. Static analysis meets a variety of goals, including error detection, security analysis, and program verification, which is why standards for critical software development recommend the use of static analysis to identify errors that are difficult to detect at run-time. Thus, this chapter presents a case study on the use of Frama-C as a static analyzer for formal verification of critical software and a lightweight semantic-extractor tool; the former uses an abstract interpretation technique, and the latter allows for the extraction of semantic information to provide a better understanding of source code. In practical terms, the chapter shows how Frama-C can support the development life cycle of an inertial system in aerospace applications, reporting a list of pros and cons. The final results indicate the benefits obtained in terms of software safety, software quality assurance and, consequently, the software verification process.

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.

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++.

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.

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.

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

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

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

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

Using tools for deductive verification, such as Frama-C, typically imposes substantial work overhead in the form of manually writing annotations. In this chapter, we investigate techniques for alleviating this problem by means of automatic inference of ACSL specifications. To this end, we present the Frama-C plugin Saida, which uses the assertion-based model checker TriCera as a back-end tool for inference of function contracts. TriCera transforms the program, and specifications provided as assume and assert statements, into a set of constrained Horn clauses (CHC), and relies on CHC solvers for the verification of these clauses. Our approach assumes that a C program consists of one entry-point (main) function and a number of helper functions, which are called from the main function either directly or transitively. Saida takes as input such a C program, where the main function is annotated with an ACSL function contract, and translates the contract into a harness function, comprised mainly of assume and assert statements. The harness function, together with the original program, is used as input for TriCera and, from the output of the CHC solver, TriCera infers pre- and post-conditions for all the helper functions in the C program, and translates them into ACSL function contracts. We illustrate on several examples how Saida can be used in practice, and discuss ongoing work on extending and improving the plugin.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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

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

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

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