Frama-C & SPARK Day 2019

Abstracts of the talks
Session 1. Introduction

The Why3 tool for deductive verification and verified OCaml libraries

Jean-Christophe Filliâtre, CNRS

Why3 is a platform for deductive program verification. It provides a rich specification language and a dedicated ML-like programming language. Once a program is verified, it can be translated to OCaml automatically. In this talk, we present an ongoing project that aims at building a verified OCaml library of general-purpose data structures and algorithms using Why3.

Teaching formal methods through Frama-C & SPARK

Christophe Garion, ISAE-Supaero

How can we educate future engineers about formal methods in few hours when they do not have a strong background in theoretical Computer Science? That is a challenge we are trying to take up at ISAE-SUPAERO in the critical systems architecture curriculum. We will present some feedback on what the students can learn and do in less than 15 hours and also present SPARK by Example, an adaptation of ACSL by Example mainly developed by two undergraduates in less than 3 months.

Session 2. Application of formal verification in autonomous driving industry

Deductive verification of industrial automotive C code

Christian Lidström, KTH Royal Institute of Technology

While deductive verification could potentially increase confidence in the correctness of software over standard industrial practices such as testing, the technique is still not in widespread use within the automotive industry. For the past 3 years, work has been ongoing on incorporating deductive verification at Scania, a manufacturer of trucks based in Sweden. Frama-C is one of the tools that has been employed to this end. This talk will present what has been achieved so far, what challenges there have been, and what is planned for the future.

SPARK in an automotive context

Florian Schanda, Zenuity

Development of self-driving vehicles is a challenging task. Verification (are we building it right?) and validation (are we building the right thing?) are essential activities for demonstrating the system is safe and fit for purpose. The safety standard ISO 26262 is an important software safety standard in the automotive industry.

In this talk we discuss how SPARK can fit into this context. We focus on two aspects: the difficulties to demonstrate robustness for ISO 26262 and how formal methods can help, and integration issues for new languages and tools in larger software ecosystems that are typically found in automotive companies.

Security & safety of autonomous vehicles: a case study with TIS Analyzer

Benjamin Monate, TrustInSoft and David Wagner, EasyMile

First, we will briefly present TrustInSoft Analyzer, a commercial static analyzer based on Frama-C that helps its users gain incrementally the highest level of confidence in C and C++ software thanks to formal methods.

We will subsequently present the EasyMile experience feedback on using TrustInSoft Analyzer on the C and C++ code base of its autonomous vehicles. We will describe the challenges specific to this domain. Then, examples from the real code base will be used to present the results as well as the work that one needs to perform in order to achieve the analysis.

Session 3. Application of formal verification to embedded software

uberSpark: Towards Piecemeal, Automated, and Composable Verification of Commodity System Software Stacks

Amit Vasudevan, Carnegie Mellon University

uberSpark is an innovative system architecture, programming principle, and development framework geared towards piecemeal, automated, and compositional verification of security properties of commodity (extensible) system software stacks written in low-level programming languages (e.g., C and Assembly).

uberSpark comprises two key ideas: (i) provide a verifiable object abstraction (uberObject) to endow low-level system software stacks with abstractions found in higher-level languages (e.g., objects, interfaces, function-call semantics, serialization, access-control etc.) and enforce uberObject abstractions using a combination of commodity hardware mechanisms, light-weight static analysis and formal verification; and (ii) interfacing with platform hardware by programming in Assembly using an idiomatic style (called CASM) and employing a hardware model of the platform that is verifiable via tools aimed at C (e.g., Frama-C), while retaining performance and low-level access to hardware. After verification, the C code is compiled using a certified compiler while the CASM code is translated into its corresponding Assembly instructions.

Collectively, these innovations enable piecemeal, automated, and compositional verification of security invariants of commodity system software stacks without sacrificing performance. We describe our experience using uberSpark to build and verify security invariants of the uber eXtensible Micro-Hypervisor Framework (uberXMHF), an open-source commodity micro-hypervisor. We used Frama-C as our verification framework and verified uberXMHF and several of its extensions, demonstrating only minor performance overhead with low verification costs.

Software for a total artificial heart

Nils Brynedal Ignell, Scandinavian Real Heart

Heart failure is a deadly condition affecting large amounts of people each year. Methods for heart transplantation are very sophisticated but a shortage of donors cause many patients to die while waiting for a donated heart. Scandinavian Real Heart is developing a total artificial heart (TAH) intended to extend the patient's life until a donor heart is available.

This talk will focus on the development of the embedded software for the controller of the heart. To achieve a high degree of reliability, the software is written in Ada as well as SPARK, which provides methods for statically proving key design objectives and program integrity.

Continuous deductive verification with Frama-C

Denis Efremov, Ivannikov Institute for System Programming and Jens Gerlach, Fraunhofer FOKUS

The formal verification of software that is continuously developed faces various challenges: legacy code, different paces of development and verification, goals mismatch between developers and specifiers. Continuous development also requires continuous verification. Otherwise, the divergence between verified code and actual code may become too big to still state that the code is verified.

Continuous deductive verification necessitates automation for the maintenance of specifications to reflect code changes, frequent replays of proofs and precise tracking of differences between the original and verified code.

In this talk, we present our experience of extending continuous integration with deductive verification in the Vessedia and the AstraVer projects. While in the Vessedia project Frama-C/WP is used to formally verify parts of the IoT operating system Contiki the AstraVer project relies on Frama-C/AstraVer(Jessie) to verify a Linux security driver.

Session 4. Application of formal verification for safety

Proof and test with rich SPARK 2014 contracts

Thomas Wilson, Altran UK

In this talk we report on practical experience using SPARK 2014 contracts in the development and verification of a critical system. Key points of our approach are that: (1) we used ‘rich’ contracts which completely characterised the functional behaviour required, and (2) we used a combination of proof and testing to verify that the implementation met these contracts.The critical system on which the approach was applied was an embedded protection system. The embedded protection system monitors the operation of a wider system and ensures that the wider system remains safe by overriding behaviour if required. The embedded protected system was developed to the highest level of integrity under UK DEF STAN 00-56.

The design process used SPARK contracts and SPARK implementations. The safety functions of the system were specified in a separate formal specification notation. These were then translated to SPARK contracts. A SPARK implementation is then produced and our verification approach used to assure that it meets the SPARK contracts.

The verification approach for the system uses both proof and test.

(1) The SPARK tools are used to formally prove that the SPARK implementation meets the SPARK contracts, which correspond to the higher-level formal specification.

(2) Run-time checking of the contracts was enabled during testing. These are used in both developer and independent testing. In developer testing, the built-in run-time checks of the contracts mean that the developers need only come up with test inputs to test that their implementations meet the specification. In independent testing, the run-time checks enable functional errors in the application software implementation to be found but also provide a means of detecting low-level software, hardware and integration issues.

Run-time checks of the contracts are also enabled in deployment. This enables some hardware and software issues to be detected, providing one of the many forms of built-in test for the system.

We will discuss interesting aspects of our practical application of this approach, focussing on proof and test of rich SPARK 2014 contracts. For example, how it was key that the declarative nature of the SPARK contracts allowed the structure of the formal specification to be retained in the translation to SPARK; and how we found run-time checking of contracts useful for finding integration issues.

Numerical Accuracy Analysis of Source Code in Thales Entities

Romain Soulat, Thales Research & Technology

During the last two years, the joint lab Formal Lab (CEA/Thales) has worked on the integration of numerical analysis tools in a Thales testing and integration toolchain to assess the numerical accuracy of source code. Numerical accuracy assessment is a common need and Thales and we hope to deploy those tools on a larger scale in the incoming years. From source code verification to the actual computations on the target hardware, several tools have been used and deployed in a toolchain to be able to give different levels of confidence on the quality of numerical software.

Bringing Deductive Verification to Factory Automation developers

Denis Cousineau, Mitsubishi Electric R&D Centre Europe

Programmable logic controllers (PLC) are industrial digital computers used as automation controllers of manufacturing processes, such as assembly lines, or robotic devices. PLCs simulate via software the hard-wired relays, timers and sequencers they have replaced. Ladder Logic was the first language used to develop PLCs software, and is still widely used and very popular among developers and electrical engineers. This language uses circuits diagrams of relay logic hardware to represent PLC program with a graphical diagram. This graphical aspect makes Ladder programs hard to debug, especially when they reach industrial size with dozens of inputs, outputs and hundreds of internal memory states. We will present an overview of the quite extensive research prototype we built on top of Why3, for bringing exhaustive verification technology provided by automated deductive verification to Ladder integrated development environment.

CEA List logo AdaCore logo NIST logo