Retour à l'OSIS

Frama-C & SPARK Day - Formal Analysis and Proof for Programs in C and Ada

30 Mai 2017 — Frama-C & SPARK Day - Formal Analysis and Proof for Programs in C and Ada

09h-17h

Amphithéâtre Buffon, Paris "Qualité logicielle"

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/), Inria joint lab `ProofInUse' (http://www.spark-2014.org/proofinuse), and Université Paris-Diderot.

This workshop will take place in the context of the event `Open Source Innovation Spring 2017' (http://www.open-source-innovation-spring.org/) initiated by thematic group `Logiciel libre' of the cluster Systematic-Paris-Region and IRILL (`Initiative de Recherche et Innovation sur le Logiciel Libre').

Direction de programme

Programme dirigé par Yannick Moy, AdaCore ; Claude Marché, Inria Saclay ; Florent Kirchner et Nikolai Kosmatov, LIST CEA Tech ; et Mihaela Sighireanu, Université Paris-Diderot.

Description détaillée

Featuring :

  • talks by the Frama-C and SPARK community
  • talks on current developments by the Frama-C and SPARK teams
  • the flair from a central Parisian location

Programme résumé

  • 08:30: Welcome Coffee & Registration
  • 09:00: Deductive Verification in Frama-C and SPARK 2014: Past, Present and Future

    Claude Marché (Inria)

  • 09:30: From Learning Examples to High-Integrity Middleware, Comparing ACSL and SPARK

    Christophe Garion, Jérôme Hugues (ISAE)

  • 10:00: Implementing Formal Code Verification: Feedbacks from Thales Early Adopters

    Jean-Marc Mota (Thales Research & Technologies)

  • 10:30: Coffee Break
  • 11:00: From 80% to 99% : An Industrial Collaboration for Automating Frama-C/WP

    Loïc Correnson (CEA List)

  • 11:30: Replicated Synchronization for Imperative BSP Programs

    Arvid Jakobsson (Huawei Technologies France)

  • 12:00: Specifying and Proving Correctness of Linux Kernel Components with ACSL

    Alexey Khoroshilov, Mikhail Mandrykin (Linux Verification Center, ISPRAS)

  • 12:30: Lunch Break
  • 14:00: CubedOS: A Verified CubeSat Operating System

    Carl Brandon, Peter Chapin (Vermont Technical College)

  • 14:30: Remove Before Flight: Defect-Free Software and Agile Development in SPARK 2014

    Martin Becker (TU München)

  • 15:00: Development of Security-Critical Software with SPARK/Ada at secunet

    Stefan Berghofer (secunet)

  • 15:30: Coffee Break
  • 16:00: Real Behavior of Floating Point Numbers

    François Bobot (CEA List)

  • 16:30: Structuring an Abstract Interpreter through State and Value Abstractions

    David Bühler (CEA List)

  • 17:00: Wrap-up & Open Mic Session

    Claude Marché (Inria), Florent Kirchner (CEA), Yannick Moy (AdaCore)

  • 17:30: Cocktail

Lieu

Amphithéâtre Buffon

Ville: Paris


Programme détaillé

  • 08:30 - Welcome Coffee & Registration
  • 09:00 - Deductive Verification in Frama-C and SPARK 2014: Past, Present and Future

    Claude Marché (Inria)

    The activities of formal proof (a.k.a. deductive verification) within Frama-C and SPARK 2014 share a common basis: Why3. The Why3 verification tool offers the unique ability to dispatch generated verification conditions to many different theorem provers. Nevertheless, the specification languages in which a user can formally specify the expected behavior of her C or Ada program significantly differ in their design. These differences affect the way verification conditions are generated, and consequently the level of proof success. We review these differences, and draw some perspectives on possible evolutions of the tool chains that could improve the level of automation one could get in proving activities, and more generally to improve the usability of deductive verification techniques within Frama-C and SPARK 2014.

  • 09:30 - From Learning Examples to High-Integrity Middleware, Comparing ACSL and SPARK

    Christophe Garion, Jérôme Hugues (ISAE)

    In this talk, we report on two experiments using ACSL and SPARK. In the first part, we introduce SPARK-by-Example, a SPARK translation of the well-known ACSL-by-Example booklet. This work has been started to learn more about the SPARK2014 language. In the second part, we report on an ongoing effort to port an AADL runtime, a middleware meant for safety-critical systems. ISAE has implemented two variants of this runtime: one targeting typical C/RTOS (FreeRTOS, RTEMS, RT-POSIX), and one targeting Ada 2005 (Ravenscar profile and high-integrity restrictions). As part of the TASTE and ESROCOS projects, we want to demonstrate absence of runtime errors. The two runtimes share common algorithms, but leverage different constructs (pointers, OS APIs vs native language constructs). We report on the current status of both activities, and required blocks to complete this task.

  • 10:00 - Implementing Formal Code Verification: Feedbacks from Thales Early Adopters

    Jean-Marc Mota (Thales Research & Technologies)

    During 2016, three different business units of Thales have experienced the use of formal code verification. Among those experiments, two of them have been focused on the implementation of SPARK 2014 and the third  one on the implementation of Frama-C. This talk aims at sharing with the SPARK & Frama-C community some feedbacks coming from early adopters. After briefly introducing the three different case studies used to evaluate the relevance of implementing formal code verification, we will present you how the assessments were conducted, the results regarding the initials expectations and the resulting recommendations. Based on these preliminary results, we will conclude by the next steps to be carried out, both at units and group level, which lead to industrially deploy formal code verification within Thales.

  • 10:30 - Coffee Break
  • 11:00 - From 80% to 99% : An Industrial Collaboration for Automating Frama-C/WP

    Loïc Correnson (CEA List)

    This talk reports on a long-term collaboration between CEA and our partner ecosystem to make Frama-C/WP mature enough for certifying critical embedded softwares in industrial contexts. Building on the previous success story on using Caveat at AIRBUS for similar certification campaigns, the original goal was to manage the obsolescence of this tool chain and to prepare a switch to Frama-C/WP. Such a process saw the emergence of many technical issues and engineering changes. Interestingly, solving these issues was responsible for many improvements in the new platform, which became much more powerful than Caveat in some areas. Finally, thanks to the most recent improvements, engineers were able to autonomously solve the last percent of the proof effort.

  • 11:30 - Replicated Synchronization for Imperative BSP Programs

    Arvid Jakobsson (Huawei Technologies France)

    The BSP model (Bulk Synchronous Parallel) simplifies the construction and evaluation of scalable parallel algorithms, with its simplified synchronization structure and cost model. The BSPlib library is commonly used to write imperative BSP programs in C. However, BSPlib programs are susceptible to synchronization errors.  We have designed and implemented a static data-flow analysis as a Frama-C plugin which verifies the absence of such errors in BSPlib programs, by enforcing a correct synchronization structure.  This plugin is the first component in a platform for statically verifying the safety and the performance characteristics of BSPlib programs.

  • 12:00 - Specifying and Proving Correctness of Linux Kernel Components with ACSL

    Alexey Khoroshilov, Mikhail Mandrykin (Linux Verification Center, ISPRAS)

    The talk presents our experience in deductive verification of Linux kernel components using Frama-C with AstraVer plugin (a fork of Jessie). It includes an overview of new features that were required to verify kernel code and a discussion of possible improvements in ACSL specification. Particularly, ACSL suggests unbounded semantics for operations on integral numbers in specifications and also does not provide special constructs for specifying relatively complex proofs, e.g. inductive proofs through lemma functions. Our experience has shown benefits of using different integer semantics and lemma functions, in particular for fragments involving complicated bit-twiddling tricks used for bit-counting, checksum computation, byte reorderings etc.

    Currently we are working on an experimental extension of ACSL with operations on bounded integers (interpreted as bit-vectors), full support for ghost (lemma) functions and possibly different semantics for logic functions and predicates with support of inlined axiomatic definitions. We are going to present our preliminary results in proving correctness of some bit-twiddling algorithms e.g. Gray decoding and Kernighan's bitcount using only an extension of ACSL, a deductive verification plugin, and Why3 IDE, without resorting to interactive theorem provers e.g. Coq or Isabelle.

  • 12:30 - Lunch Break
  • 14:00 - CubedOS: A Verified CubeSat Operating System

    Carl Brandon, Peter Chapin (Vermont Technical College)

    In this paper we present CubedOS, a lightweight application framework for CubeSat flight software. CubedOS is written in SPARK and verified free of certain classes of runtime errors. It consists of a collection of interacting, concurrent modules that communicate via message passing over a microkernel based on Ada's Ravenscar tasking model. It provides core services such as communication protocol processing and publish/subscribe message handling. In addition, application-specific modules can be added to provide both high level functions such as navigation and power management, as well as low level device drivers for mission-specific hardware. Here we present the architecture of CubedOS, and describe Lunar IceCube, the first mission to use CubedOS.

  • 14:30 - Remove Before Flight: Defect-Free Software and Agile Development in SPARK 2014

    Martin Becker (TU München)

    Development and verification of safety-critical software requires trained experts and takes its time. We challenged this opinion by developing an entire flight stack for a high-altitude glider in Ada/SPARK 2014 within only a few months of time. We started implementation with an initial software design and continuously applied static analysis to eliminate defects, adapt the design to verification needs, and to ensure a goal-oriented progress during the implementation phase. This talk introduces the project, explains the workflow that has been established, and reflects on project progress, final results and remaining challenges of verifying SPARK programs.

  • 15:00 - Development of Security-Critical Software with SPARK/Ada at secunet

    Stefan Berghofer (secunet)

    In this talk, we describe how the SPARK/Ada language and toolset is used for the development of component-based high-security systems at secunet Security Networks AG. To make the complexity of assessing the security of these systems manageable, the components are running on top of the Muen separation kernel, which ensures that they can only communicate with each other via designated channels. We give an overview of our methodology for verifying trusted components using a combination of the SPARK tools and the interactive proof assistant Isabelle, which is used for solving proof obligations that are beyond reach of automatic provers. We illustrate the methodology using selected correctness properties of a cryptographic library.

  • 15:30 - Coffee Break
  • 16:00 - Real Behavior of Floating Point Numbers

    François Bobot (CEA List)

    Floating point numbers are pervasively used in programs, yet when one starts to look into them it becomes clear that they are nothing like reals. There are a lot of counter-examples of simple real number properties that are completely wrong for floating point numbers. Yet, actual C or SPARK developers are using floating point numbers and expect their code to behave like reals! and in many cases they are indeed right. However it is difficult for state-of-the-art program verification tools to prove that the floating point properties they are using are true. We will show the result of the fruitful collaboration done in the SOPRANO project that allowed the Frama-C and SPARK tools to tackle these problems orders of magnitude faster than before.

  • 16:30 - Structuring an Abstract Interpreter through State and Value Abstractions

    David Bühler (CEA List)

    The new abstract interpreter of Frama-C, EVA, enjoys a modular and extensible architecture, where new analysis domains may be plugged-in. These domains can interact through different means to achieve maximal precision. First, they work cooperatively to emit the alarms that exclude the undefined behaviors of the program. Second, they exchange information through abstractions of the possible values of expressions. Those value abstractions are themselves extensible, should two domains require a novel form of cooperation. In this talk, we present this communication system and illustrate how the different domains of EVA benefit from it.

  • 17:00 - Wrap-up & Open Mic Session

    Claude Marché (Inria), Florent Kirchner (CEA), Yannick Moy (AdaCore)

  • 17:30 - Cocktail

Organisateurs et/ou sponsors

  • AdaCore

    AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. One of its flagship products is the SPARK Pro verification environment, a toolset based on formal methods and oriented toward high-assurance system.

  • ProofInUse

    ProofInUse originates from the sharing of resources and knowledge between the Toccata research team from Inria and AdaCore, with the objective to provide verification tools, based on mathematical proof, to industry users. These tools are aimed at replacing or complementing the existing test activities, whilst reducing costs.

Organisateurs (2017)

Co-organisateurs et sponsors (2017)

Ils parlent de l'OSIS (2017)