Frama-C Days 2024 Gallery

Abstract

In this talk, I have given an overview of how VerCors is used for the verification of concurrent software. Some small examples were shown to illustrate the approach. Then I zoomed in on some subprojects. First, I discussed how Alpinist, a tool which takes as input a verified program, and then optimises both the program and specification, such that the resulting program can be verified again. Then we discussed the Vesuv tool, which encodes SystemC programs into input for the VerCors verifier. A particular challenge here is that we wish to verify properties that relate multiple processes. Finally, we discussed how we are working on support for the verification LLVM programs, as a way to build verifiers for multiple programming languages in an easy way. Finally, I concluded the talk by an outlook of multiple future research directions.

About the author

Abstract

We present the brand new Guide to Software Verification with Frama-C, a collective effort over several years to get a guidebook that 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.

About the authors

Abstract

We present Ivette, the new graphical user interface for Frama-C. Ivette is a complete redesign of our oldish frama-c-gui. Based on a modern web-originated software stack, Ivette offers much more flexibility, benefits from a wide ecosystem, and allows us to welcome external contributors much more easily than its predecessor.

Moreover, contrarily to our old frama-c-gui, the new design of Ivette is based on a clear separation from the Frama-C side (OCaml based, sequential) and the User Interface side (Typescript & React based, asynchronous). The Frama-C side, supported by its new Server plug-in, allows for further integration in other contexts, typically code editors.

Frama-C Server requests are auto-documented and easy to implement by Frama-C plug-in developers. Ivette is built upon React and Electron, and is easily extensible in Typescript thanks to a rich toolkit of ready-to-used components named Dome. A rich middleware is available, which makes using Frama-C Server requests straightforward and quite efficient.

Currently, Ivette has built-in support for only EVA and WP and it is still under active development. Although, we already use it on a day-to-day basis for all of our new projects and we plan to deprecate the old frama-c-gui very quickly.

About the author

Abstract

This presentation is the support for some live demos of plugins and tools available in Frama-C, to help the user understand what a given code does, how to navigate it, and how to explore analysis results.

Associated book chapter: Tools for Program Understanding.

About the author

Abstract

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

Associated book chapter: Runtime Annotation Checking with Frama-C: The E-ACSL Plug-in.

About the author

Abstract

Cegarmc is a Frama-C plugin for integrating software model checking into Frama-C. The name is derived from CEGAR, or counterexample guided abstraction refinement, which is one of the main techniques used by software model checking to handle the state space explosion problem (However there are others as well, such as bounded model checking and k-induction). The Cegarmc plugin interoperates with other Frama-C plugins, such as EVA in order to provide sound static analysis results to aid the model checking procedure.

Associated book chapter: Combining Analyses Within Frama-C.

About the author

Abstract

This talk presents two Frama-C plugins designed for the lightweight detection of data races (RacerF) and deadlocks (DeadlockF) in multi-threaded C programs. Both plugins can operate in a fast mode, utilizing only syntactic information, or in a more precise mode, leveraging results from the value analysis computed by EVA. Our experimental evaluation on medium-sized programs demonstrates that both plugins can detect known bugs while maintaining a very low false positive rate.

About the author

Abstract

The many bugs found regularly in the Linux kernel suggests that formal verification of some core components could be valuable. However, a major stumbling block is that fact that the rapid rate of change of Linux kernel code implies that any such proof is soon out of date. We would like to investigate the kinds of changes that occur in practice and the practical impact of these changes on proofs. In this talk, we describe an initial case study, using Frama-C and the WP plugin, considering the entire history of the Linux kernel scheduler function should_we_balance.

About the author

Abstract

This talk, which is an introduction to Chap. 10 of the Frama-C book presents three Frama-C plug-ins that provide Domain-Specific Languages (DSL) for expressing different kinds of properties that are difficult to state as plain ACSL annotations. First, MetAcsl is dedicated to pervasive properties, that need to be checked at many points of the program. Second, RPP lets the user state relational properties, that express a relation between several function calls, as opposed to a function contract that only describe a single call. Finally, Aoraï focuses on temporal properties, and more precisely on the sequences of calls that are supposed to happen during the program execution.

Associated book chapter: Specification and Verification of High-Level Properties.

About the author

Abstract

This talk presents a retrospective of four years of successful application of formal verification in an industrial context at Thales for security certification. Its achievements allowed to consolidate a stringent software development process of smart card products using deductive verification with Frama-C/WP of a JavaCard virtual machine implementation. The project evolved from initial uncertainties on feasibility at early stages up to the successful Common Criteria certification at the highest level of security assurance (EAL7). We present the verification methodology, share some results and best practices we have learned during this journey, and outline some ongoing and future work. This is a joint work with Martin Hána.

Associated book chapter: Proof of Security Properties: Application to JavaCard Virtual Machine.

About the authors

Abstract

Coma is a minimalistic algorithmic language designed for deductive verification. It adopts the continuation-passing style which allows us to express in a natural manner the standard control structures - conditionals, loops, subroutine calls, and exception handling - using only three elementary constructions.

The specification annotations in Coma take the form of assertions mixed with the rest of the program code. A special barrier tag is used to separate, inside a subroutine definition, the “interface” part of the code, which should be verified at each call, from the “implementation” part, which is verified only once, for all possible inputs. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification for different execution paths in the code. We can also forgo the barriers entirely for some (or all) of the paths, which effectively inlines the corresponding code during the computation of verification conditions.

Verification conditions for Coma programs are structurally similar to what is generated by the classical weakest-precondition calculus. However, our procedure can also factorize the instances of selected subformulas in the resulting proof obligation, which leads to more compact verification conditions in the style of Flanagan and Saxe.

About the author

Abstract

We present the experimental Saida plugin aimed at inferring ACSL functions for C programs. The plugin takes as input a program where only the main function is annotated with an ACSL contract, and then attempts to infer ACSL contracts for all functions that are called (possibly transitively) from the main function. The inference engine is the TriCera tool, which is a Horn clause based model checker for C programs. TriCera encodes the program as a set of Horn clauses and then searches for a solution. From the solution, one may extract contracts for any function that is called in the program. Naturally, model checking may always scale, but we expect that, in many cases, the contract inference technique may reduce the manual overhead when using Frama-C.

Associated book chapter: An Exercise in Mind Reading: Automatic Contract Inference for Frama-C.

About the author

Abstract

The talk discusses the fundamental role of memory analysis when analyzing general-purpose C code and how to structure a static analyzer able to analyze memory. It then discusses two advanced memory analyzes implemented as Frama-C plugins: one based on separation logic reasoning about strong invariants, and one based on advanced type systems reasoning about less strong (but more general) invariants. Both analyses are modular (analyzing functions without having to know the whole program), which is key to scalability, integrating static analysis in the development phase, or to analyze reusable code such as libraries.

Associated book chapter: Advanced Memory and Shape Analyses.

About the author

Abstract

Q Framework is a verification framework used at Sandia National Laboratories. Q is a collection of tools used to verify safety and correctness properties of high-consequence embedded systems. This correctness argument hinges on constructing refinement relations between multiple state machine models, as well as state machines and C implementations. This talk focuses on the latter refinement to C code, which is achieved via automatically generated ACSL annotations and proved via Frama-C. We give an overview of Q Framework and describe how these ACSL annotations provide a refinement relation.

About the author

Abstract

This talk presents how to produce some complex loop invariants for numerical embedded code and and how Frama-C can be used to verify them. 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. Analysing filter code with Frama-C is challenging, since finding a loop invariant with complex relationships between the variables is never an evident task. 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 to compare the quality of results of the different solutions. Several examples and several concrete solutions illustrate the generation of such inductive invariants and their formal verification.

Associated book chapter: Analysis of Embedded Numerical Programs in the Presence of Numerical Filters.

About the author

Abstract

TTC (Trust-Type Checker) is a static analyzer, designed as a Frama-C plugin, for C programs. It is compositional in the sense that when TTC analyzes a piece of code, it only uses the specification of the functions called (not the function’s definition). TTC augments C’s “type system” with a notion of trust. The analysis is akin to taint analysis, a kind of analysis found in security. It lets users specify their data using annotations. The data is either unsafe or (some flavor of) trusted, and TTC verifies that when a function is expecting trusted data, the actual parameter contains data that is at least as trusted as the function’s specification.

About the author

Abstract

This talk presents how static analysis and formal methods improve the security of the products and the situations where they are required in the French scheme for Common Criteria certification.

About the author

Abstract

This talk presents what we have done since the last Frama-C Days in 2019, in particular our work on usability through better user interfaces, better analysis feedback and improved analysis and specification methods. It also describes what we plan for the upcoming years.

About the author