During the period leading from M19 to M36, the project has achieved significant results:

  • Experimental results from the CEA use-case: approach to V&V, target of verification, analysis results, quantitative data, and recommendations for other similar applications are described in deliverable D5.4.
  • New and improved tools that permit easy and efficient analysis of critical applications.
  • Integrated tools that help improve the analysis work, namely by combining static with dynamic analyses, and modelling with specifications and proofs.
  • Improvements of the C++ source code analysis: improved ACSL++ specification language (with the help of David Cok, co-author of the JML specification language and its implementation OpenJML) and improved implementation frama-clang.
  • Help for vulnerabilities detection through tool support.
  • A new ISO standard on V&V tools: ISO 23643.
  • Dissemination through a large number of scientific papers, events, workshops, webinar, raising the notoriety of project partners in the IoT security domain.

The project made significant impacts in the following areas:

  • Improved static analysis tools, allowing easier and cost-effective analyses to be performed on a whole range of medium-criticality software applications.
  • Increased trust in ICT products through a higher level of security and safety.
  • More resilient critical infrastructures and services by a system-based approach, combining the best of our V&V technology.
  • Higher scientific recognition of the CEA work. For instance, the yearly Frama-C days and DIGIHALL events have displayed our achievements to industries and academia.

In terms of progress beyond the state of the art, we advanced in the following areas:

  • Improved formal methods usability: Frama-C has been developed and experimented since 2005 on numerous applications from different domains improve the tool and its methodology. We seek for a relative completeness in terms of areas covered to ensure that all users can benefit from the technology. In VESSEDIA we tackle the field of IoT through three use-cases. The same experimental approach holds for the VeriFast, Diversity, Contiki, and FlowArmor tools that have evolved along experiments.
  • Experiments: the 6LowPAN CEA use-case has studied how to use the project tools for ensuring safety and security properties of this application, that is made of C and Java code. The Frama-C and VeriFast tools have been applied and detected several issues in the code.
  • Improved usability, performance and stability through the delivery of several new releases of the tools Frama-C, E-ACSL, frama-clang, Diversity and Papyrus (see the release dates and versions in deliverable D6.5)
  • Improved scalability: VESSEDIA expects to scale up source code analysis tools by improving the efficiency of the tools and demonstrate it on the project’s use-cases. See the deliverable D5.2 that describes how Frama-C has been applied to the large Contiki code base.
  • Standardisation: In the ISO JTC1/SC7/WG4 CEA contributed to develop a normative ISO standard for V&V tools. This is a milestone as, to the best of our knowledge, no other standard presents a panorama of the V&V tools capabilities that projects can refer to. The standard is currently in FDIS status and will become final in 2020.
  • Improved modularity and abstraction: Since the beginning of software development, programming languages have improved in terms of abstraction capabilities at the language level allowing more efficient programming and less error prone programs (e.g. Pascal, Ada, OCAML, Rust). In VESSEDIA, the connections between design and formal methods help in the same manner through 1) more abstract descriptions of systems (e.g. in SysML), 2) system-level security properties and their refinements (in ACSL), and 3) integration of detailed specifications at design level.