The Open Source
Innovation Spring 2019

Qualité logicielle | IoT | Cloud | Big Data | Systèmes d'information

Mars-juin 2019, Paris - Châtillon

Présidence : Roberto Di Cosmo, vice-président du GTLL, directeur de l’Irill, directeur de recherche Inria, Professeur à l’Université Paris-Diderot

Organisé par : logo Systematic & logo IRILL

Retour à l'OSIS

Frama-C & SPARK Day 2019

3 Juin 2019 — Frama-C & SPARK Day 2019

09h-17h

La Fabrique Événementielle, 52 ter Rue des Vinaigriers, 75010 Paris SPARK,Frama-C,Safety,Security,Software

Résumé

This one-day workshop aims at gathering both academic and industrial users of the environments Frama-C and SPARK, for sharing experiences and discussing perspectives. It is co-organized by CEA List (http://www-list.cea.fr/en/), AdaCore (http://www.adacore.com/), TrustInSoft (https://trust-in-soft.com/) and Inria joint lab 'ProofInUse' (https://www.adacore.com/proofinuse).

Direction de programme

François Bobot (CEA), Claire Dross (AdaCore), Florent Kirchner (CEA), Nikolai Kosmatov (CEA), Claude Marché (Inria), Benjamin Monate (TrustInSoft), Yannick Moy (AdaCore)

Description détaillée

Frama-C & SPARK Day 2019 is a one-day workshop gathering researchers and engineers around shared experiences and new perspectives of the environments Frama-C and SPARK. It continues the series of previous similar events FCD 2015, FCD 2016, FCSD 2017, and SSAS 2018.

Speakers at the Frama-C & SPARK Day will demonstrate and discuss innovative approaches to software analysis, from both academic and industrial points of views. In addition to invited presentations, this workshop will feature space for community discussions, updates on new developments and upcoming projects.

The talks are organised in four sessions:

  1. a keynote on the Why3 technology used in SPARK and Frama-C followed by a talk on teaching with SPARK and Frama-C
  2. three talks on the application of formal verification in autonomous driving industry
  3. three talks on the application of formal verification to embedded software
  4. three talks on the application of formal verification for safety

Programme résumé

  • 09:00: The Why3 tool for deductive verification and verified OCaml libraries

    Jean-Christophe Filliâtre – CNRS

  • 10:00: Teaching formal methods through Frama-C & SPARK

    Christophe Garion – ISAE-SUPAERO

  • 10:30: Coffee Break

  • 11:00: [Autonomy 1] Deductive verification of industrial automotive C code

    Christian Lidström – KTH Royal Institute of Technology

  • 11:30: [Autonomy 2] SPARK in an automotive context

    Florian Schanda – Zenuity

  • 12:00: [Autonomy 3] Security & safety of autonomous vehicles: a case study with TIS Analyzer

    Benjamin Monate – TrustInSoft
    David Wagner – EasyMile

  • 12:30: Lunch Break

  • 14:00: [Embedded 1] uberSpark: Towards Piecemeal, Automated, and Composable Verification of Commodity System Software Stacks

    Amit Vasudevan – Carnegie Mellon University

  • 14:30: [Embedded 2] Software for a total artificial heart

    Nils Brynedal Ignell – Scandinavian Real Heart

  • 15:00: [Embedded 3] Continuous deductive verification with Frama-C

    Denis Efremov – Ivannikov Institute for System Programming
    Jens Gerlach – Fraunhofer FOKUS

  • 15:30: Coffee Break

  • 16:00: [Safety 1] Proof and test with rich SPARK 2014 contracts

    Thomas Wilson – Altran UK

  • 16:30: [Safety 2] Numerical Accuracy Analysis of Source Code in Thales Entities

    Romain Soulat – Thales Research & Technology

  • 17:00: [Safety 3] Bringing Deductive Verification to Factory Automation developers

    Denis Cousineau – Mitsubishi Electric R&D Centre Europe

  • 17:30: Cocktail

Lieu

La Fabrique Événementielle

Ville: 52 ter Rue des Vinaigriers, 75010 Paris


Programme détaillé

  • 09:00 - 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.

  • 10:00 - 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.

  • 10:30 - Coffee Break

  • 11:00 - [Autonomy 1] 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.

  • 11:30 - [Autonomy 2] 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.

  • 12:00 - [Autonomy 3] Security & safety of autonomous vehicles: a case study with TIS Analyzer

    Benjamin Monate – TrustInSoft
    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.

  • 12:30 - Lunch Break

  • 14:00 - [Embedded 1] 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.

  • 14:30 - [Embedded 2] 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.

  • 15:00 - [Embedded 3] Continuous deductive verification with Frama-C

    Denis Efremov – Ivannikov Institute for System Programming
    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.

  • 15:30 - Coffee Break

  • 16:00 - [Safety 1] 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.

  • 16:30 - [Safety 2] 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.

  • 17:00 - [Safety 3] 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.

  • 17:30 - Cocktail

Intervenants

  • Amit Vasudevan

    Amit Vasudevan is a Computer Scientist at the Software Engineering Institute (SEI), Carnegie Mellon University (CMU).

    He received his Ph.D. and M.S degrees from the Computer Science Department at UT Arlington and spent three years as a Post-doctoral fellow at CyLab, Carnegie Mellon University. Before that, he obtained his B.E. from the Computer Science Department at the BMS College of Engineering, Bangalore, India.

    His research interests include secure (embedded) systems and IoT, virtualization, trusted computing, formal methods, malware analysis and operating systems. His present research focuses on building formally verifiable and trustworthy computing systems. He is the principal force behind the design and development of uberSpark, – an innovative architecture and framework for compositional formal verification of security properties of commodity system software; and the uber eXtensible Micro-Hypervisor Framework (uberXMHF), – an open-source, extensible and formally verifiable micro-hypervisor framework which forms the foundation for a new class of (security-oriented) micro-hypervisor based applications (“uberapps”) on commodity computing platforms.

    When low-level tinkering with computing platforms, IoTs, drones, and such get too much for him, he can be found spending time with his wife and kids, meditating and wood-working amidst the Texas ranches and longhorns.

  • Benjamin Monate

    Benjamin Monate is co-founder and CTO of TrustInSoft, the start-up company industrializing the Frama-C source code analyzing framework. He is the initial inventor of Frama-C and lead its research & development team for almost ten years at the CEA.

  • Christian Lidström

    Currently, Christian Lidström is a PhD student at KTH Royal Institute of Technology, in the area of deductive verification. Former consultant at Scania, within research projects focused on the application of formal methods in the automotive industry.

  • Christophe Garion

    Christophe Garion is an Associate Professor at ISAE-SUPAERO. He holds a PhD and an engineer degree in Computer Science. He is now interested in how to introduce formal methods (and more generally theoretical computer science) to engineering students.

  • David Wagner

    David Wagner is R&D Engineer at EasyMile who focuses on software quality, development infrastructure and build systems. He is keen on building code bases atop of solid foundations.

  • Denis Cousineau

    Denis Cousineau is a researcher in Communication & Information Systems department of Mitsubishi Electric R&D Centre Europe. He received his PhD from Ecole Polytechnique in the domain of proof theory. After working on proof systems for temporal logic and proof automation at Inria and Microsoft research (joint lab), he embraced various aspects of formal methods applications at Prove&Run and IRT SystemX, and is now focusing his research on how to integrate formal methods in industrial processes concerning critical systems (railway, factory automation, automotive...), in an efficient and confident way.

  • Denis Efremov

    Denis Efremov is working as a researcher at Ivannikov Institute for System Programming of the Russian Academy of Sciences (ISP RAS). Main areas are formal methods, Linux kernel and their application for verification of an industrial access control system in AstraVer project. He worked with Dr. Jens Gerlach on verification of IoT OS Contiki during an internship at Fraunhofer FOKUS.

  • Florian Schanda

    Florian Schanda has previously developed and maintained the SPARK tools and language, and is now working for Zenuity as an AD feature/software developer.

    He has a background in theoretical computer science. Current research interests include formal methods and their industrial application, languages, and floating point reasoning.

  • Jean-Christophe Filliâtre

    Jean-Christophe did a PhD from 1995 to 1999 under the supervision of Christine Paulin, regarding verification of imperative programs in the system Coq. Right after his PhD, in fall 1999, he redesigned the architecture of Coq, to isolate a kernel. Then he left for a post-doc at SRI, in the PVS team, where he started the development of the ICS decision procedure. When he returned to France, Jean-Christophe started in 2001 the development of a tool for program verification called Why, used for the proof of C programs (in the Caduceus tool, now subsumed by Frama-C) and for the proof of Java programs in the Krakatoa tool. In 2010, the Why tool became Why3.

  • Jens Gerlach

    Jens Gerlach is a senior researcher at Fraunhofer FOKUS, Berlin. His main area of research is deductive verification of critical software. He is also the main author of “ACSL by Example” – a collection of formally verified classic algorithms. In the context of the Vessedia project he is currently participating in the verification of parts of IoT operating system Contiki.

  • Nils Brynedal Ignell

    Nils Brynedal Ignell graduated from Mälardalen University in Västerås, Sweden, in 2014 with a Master of Science in Engineering degree in the field of robotics. His educational background includes computer science, electronics, mathematics and physics.

    Since the beginning of 2017, Nils has been tasked with the development of the software for total artificial heart that Scandinavian Real Heart is developing, as well as other tasks such as research and testing.

  • Romain Soulat

    Romain Soulat is research engineer at Thales Research & Technology. He earned his PhD from Ecole Normale Supérieure de Paris-Saclay on the formal verification of timed automata and system controllers. He then went to work at Thales to help Thales Business Units integrate formal verification in their toolchains. With the help of Formal Lab, the CEA/Thales joint lab on formal methods, he worked on numerous topics for Thales entities including model checking, abstract interpretation, deductive verification and numerical accuracy analysis.

  • Thomas Wilson

    Thomas Wilson is Technical Authority for Research and Technology at the Intelligent Systems division of Altran UK. This involves overseeing all of the division’s research into the use of Formal Methods in Software Engineering. He received a BSc in Computing Science and PhD in Applied Formal Methods from University of Stirling. His PhD involved the production of a new formal language and range of supporting verification tools combining the use of proof and test. Thomas joined Altran UK in 2007 and has worked on projects within the aerospace, defence and rail sectors, whilst continuing to pursue his research interests. He has over 10 years of commercial experience of formal specification, proof and testing of high-integrity systems.

Organisateurs et/ou sponsors

Organisateurs (2019)

Co-organisateurs et sponsors (2019)

Ils parlent de l'OSIS (2019)