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 Day

20 Juin 2016 — Frama-C Day

09h-17h

Maison la Recherche, Paris "Qualité logicielle"

Résumé

A one-day workshop by the Frama-C community, gathering both academic & industrial users around shared experiences and new perspectives.

Direction de programme

Programme dirigé par Florent Kirchner, directeur du laboratoire Sûreté du logiciel, CEA List.

Description détaillée

Featuring :

  • talks by the Frama-C community
  • a session on current developments by the Frama-C team
  • posters from junior researchers
  • the flair from a central Parisian location
  • an evening at Fête de la Musique

Programme résumé

  • 08:30: Welcome coffee and registration
  • 09:00: Opening comments

     F. Kirchner, List, CEA Tech

  • 09:05: Keynote: How Frama-C can help a verification & assessment body

    F. Sadmi, Bureau Veritas

  • 09:30: Automatic Generation of Counter-Measure Calling Contexts: the CURSOR Method

    D. Pariente, DASSAULT AVIATION

  • 09:30: I. INDUSTRIAL USES | Session 1
  • 10:00: Safe resource use tracking with a combination of control flow and data flow analysis

    P. Bishop & S. George, Adelard LLP

  • 10:30: Break
  • 11:00: II. INDUSTRIAL USES | Session 2
  • 11:01: TrustInSoft Analyzer: practical program analysis for guaranteed safety and security

    B. Monate, TrustInSoft

  • 11:30: SPEEDY: Specification editing, checking & discovery for C programs with ACSL specifications

    D. R. Cok, GrammaTech, Inc.

  • 12:00: Lunch
  • 14:00: III. FRAMA-C AS A RESEARCH PLATFORM
  • 14:01: Formal verification of controller implementation

    P-L. Garoche, Onera

  • 14:30: Research Challenges in Software Verification of Safety-Critical Aerospace Systems

    C. A. Muñoz, NASA

  • 15:00: Frama-C and Why3: going way back — and forward, too

    A. Paskevich - LRI, Université Paris-Saclay / Inria

  • 15:30: Break
  • 16:00: IV. NEW DEVELOPMENTS BY THE Frama-C Team
  • 16:01: Proving C code with GATeL, or how to use Frama-C, WP and Value as libraries

    L. Correnson, List, CEA Tech

  • 16:30: Evolved Value Analysis

    B. Yakobowski, List CEA Tech

  • 17:00: Frama-Clang, a C++ front-end for Frama-C

    V. Prevosto, List, CEA Tech

  • 17:30: Cocktail

Lieu

Maison la Recherche

Ville: Paris


Programme détaillé

  • 08:30 - Welcome coffee and registration
  • 09:00 - Opening comments

     F. Kirchner, List, CEA Tech

  • 09:05 - Keynote: How Frama-C can help a verification & assessment body

    F. Sadmi, Bureau Veritas

    As software verification activities get more and more complex and expensive, developers and users need methodologies and tools to perform them in an optimal manner. On the other hand, third-parties have to find ways to trust the verification evidence that are provided, especially regarding standards and normative requirements. In particular, Bureau Veritas has to understand the Frama-C tool in order to assess its outputs or perform directly the analysis.

  • 09:30 - Automatic Generation of Counter-Measure Calling Contexts: the CURSOR Method

    D. Pariente, DASSAULT AVIATION

    Designed during the FP7/STANCE project, the CURSOR method aims at detecting categories of common weaknesses in the source code, and generating the corresponding counter-measure calling contexts. This intends to strengthen applications potentially exposed to attacks based on identified families of flaws in the code. The method relies on a runtime-assertion checking approach, and is tooled by means of the Frama-C platform. CURSOR was successfully experimented on some Apache server libraries.

  • 09:30 - I. INDUSTRIAL USES | Session 1
  • 10:00 - Safe resource use tracking with a combination of control flow and data flow analysis

    P. Bishop & S. George, Adelard LLP

    Many dynamically allocated resources like memory, semaphores and interrupt enable/disable require a similar kind of analysis to demonstrate correct usage. To prevent long term resource starvation, any resource claim must be released on all subsequent branches of control flow. For cases where claims and releases are repeatedly made using the same resource identifier, an integrated data flow analysis is needed to complete the analysis. We have developed a prototype plug-in that performs this analysis in the context of malloc/free pairs, but is written in a generalised way that is easy to adapt to other resource claim/release patterns.

  • 10:30 - Break
  • 11:00 - II. INDUSTRIAL USES | Session 2
  • 11:01 - TrustInSoft Analyzer: practical program analysis for guaranteed safety and security

    B. Monate, TrustInSoft

    TBA

  • 11:30 - SPEEDY: Specification editing, checking & discovery for C programs with ACSL specifications

    D. R. Cok, GrammaTech, Inc.

    The SPEEDY tool intends to simplify the task of applying formal methods in the context of typical software development environments. The incarnation of SPEEDY described here targets C programs with ACSL specifications. The tool combines four elements: (a) enhancing the Eclipse development environment for C programs with first-class support for ACSL, (b) adding functionality and text to aid users in understanding how to write specifications, (c) integrating tools that check specifications, such as Frama-C, showing the success or failure of verification attempts in the Eclipse GUI, (d) integrating tools and algorithms for inferring specifications from the source code. The development of SPEEDY was supported by NASA (Contract #NNX14CL05C) and executed by GrammaTech, Inc.

  • 12:00 - Lunch
  • 14:00 - III. FRAMA-C AS A RESEARCH PLATFORM
  • 14:01 - Formal verification of controller implementation

    P-L. Garoche, Onera

    Embedded control systems are amongst the most critical systems. Their behavior is specific: they have an infinite behavior in which, at each loop iteration, a sensor input is read, computations are performed, and an output is produced on actuators. A first part of the talk will focus on proving the bounded behavior of those systems, guarantying the absence of overflow despite their infinite behavior. Those systems are typically designed using high level models such as Matlab Simulink, ANSYS Scade or Lustre. Then they are compiled into embedded C code. These models are well suited to perform functional properties verification, eg. using k-induction-based model-checkers. But the expression and the analysis of those properties is more difficult at code level. We propose a methodology to compile these model-level specification and associated model-checking proofs into C level artifacts. Once produced we rely on Frama-C/WP to revalidate them, at code level. These results benefited from numerous collaborations including X. Thirioux (IRIT), P. Roux, T. Kahsai (NASA/CMU), E. Feron (Georgia Tech), G. Davy (Onera), H. Herencia-Zapana (ex-NIA, now GE), R. Jobredeaux (ex-GT), T. Wang (ex-GT, now UTRC).

  • 14:30 - Research Challenges in Software Verification of Safety-Critical Aerospace Systems

    C. A. Muñoz, NASA

    This talk reports on formal methods research conducted under NASA’s Airspace Operations and Safety Program (AOSP). As part of this research, Frama-C has been used in the formal verification of numerical intensive software and in the formal verification of automatically generated run-time monitors. Based on this experience, the talk discusses research challenges in software verification of safety-critical systems of interest to NASA.

  • 15:00 - Frama-C and Why3: going way back — and forward, too

    A. Paskevich - LRI, Université Paris-Saclay / Inria

    Why3 is a tool for deductive verification of imperative programs. Why3 and its predecessor, Why, have a long history of collaboration, both technical and human, with Frama-C. In this talk, we revisit the roots of this collaboration, assess its current state, and venture into possible future developments. In particular, we make a case for an interface between ACSL and high-level specification facilities available in Why3, which include type polymorphism, variant types and pattern matching, fine-grained specification libraries, and a way to ensure consistency of an axiomatization by realizing it in a sceptical proof assistant like Coq or Isabelle.

  • 15:30 - Break
  • 16:00 - IV. NEW DEVELOPMENTS BY THE Frama-C Team
  • 16:01 - Proving C code with GATeL, or how to use Frama-C, WP and Value as libraries

    L. Correnson, List, CEA Tech

    Functional properties of reactive, synchrone software are naturally specified and encoded into Lustre Observers. In practice however, such an embedded software would not be completely generated from synchronous models, but would contain a large amount of manually written C code. One can thus be required to verify its Lustre properties directly from the C code.We show how to use the combined power of Value Analysis and WP interfaces to develop a Frama-C plug-in extracting a Lustre model of this synchronous behaviour from C source code, and to verify some of its properties with GaTEL. This constitutes a step forward in the proof of complex safety systems, and the very first experiment combining these three major technologies from our laboratory.

  • 16:30 - Evolved Value Analysis

    B. Yakobowski, List CEA Tech

  • 17:00 - Frama-Clang, a C++ front-end for Frama-C

    V. Prevosto, List, CEA Tech

    This talk will present the new Frama-Clang plug-in, which aims at providing a C++ front-end to Frama-C. As its name suggests, Frama-Clang relies on the Clang compiler for the parsing and type-checking of C++ code. We will see how the necessary information can be extracted from Clang's AST to build a valid Frama-C AST and how it is possible to extend Clang to parse and type-check ACSL(++) annotations together with the code itself.

  • 17:30 - Cocktail

Organisateurs et/ou sponsors

  • Frama-C

    Frama-C is an extensible and collaborative platform dedicated to source-code analysis of C software.