Report

Teaser, summary, work performed and final results

Periodic Reporting for period 1 - VESSEDIA (VERIFICATION ENGINEERING OF SAFETY AND SECURITY CRITICAL DYNAMIC INDUSTRIAL APPLICATIONS)

Teaser

VESSEDIA aims at enhancing and scaling up modern software analysis tools to use them on medium-criticality applications such as IoT.To achieve this goal several technical goals have been set:• Improve the security and reliability of connected embedded software applications...

Summary

VESSEDIA aims at enhancing and scaling up modern software analysis tools to use them on medium-criticality applications such as IoT.
To achieve this goal several technical goals have been set:
• Improve the security and reliability of connected embedded software applications, using formal methods that have proven their efficiency in life/mission critical applications.
• Promote Formal methods and make them more accessible for other application domains sharing a certain number of limiting characteristics.
• Build a flexible methodology for safety and security analysis based on formal methods.
• Testing specific formal methods on some representative IoT.
• Provide tool support for the security evaluation and certification processes.
Therefore, the following lower level objectives were set:
• Quantification of the verification process: VESSEDIA develops measures enabling to quantify a V&V process and thus the progress achieved and remaining
• Building collaborative and smart user interfaces: state of the art tools, such as those used and developed in VESSEDIA, need modern user-interfaces and architectures.
• High-level models for V&V: abstract models are provided by modelling tools. VESSEDIA is researching to construct and refine design models and express and verify security properties.
• Building strong links with Common Criteria for the certification for medium criticality applications. VESSEDIA is researching how the techniques and tools can support CC certification and, vice-versa, what are the needs in terms of tools.
• ISO standardisation: VESSEDIA will provide a new ISO standard providing the categories and capabilities of V&V tools, allowing to choose the right tool for the right application.

Work performed

During the period leading from M1 to M18, the project has achieved significant work that can be described in different research streams:
• Three use-cases are running in parallel and performed the following tasks:
o Definition of the precise perimeter for analysis and of high level security and safety properties.
o Set up of the project analysis tools and training.
o First round of analyses (on-going).
• Research and development to solve the technical problems in the analysis tools. This includes the following tasks that are under way:
o Connections between modelling and formal verification tools.
o Improvements of the core tools Frama-C, VeriFast, Diversity, Contiki, and FlowArmor.
o Improvements of related plug-ins, such as E-ACSL and Frama-clang.
o Connections between formal analysis tool Frama-C and testing tool AFL and between Frama-C and modelling tool Diversity.
o Development of new GUI and a client-server proof architecture for Frama-C.
o Improvements of the ACSL++ specification language for C++.
• Research on methodologies by integrating the end-users’ concrete needs, the economic concerns and the quality measurements.
• In parallel dissemination activities.

Final results

In terms of progress beyond the state of the art, we expect to advance in the following areas:
• Improved formal methods usability and stability: Frama-C has been experimented since 2005 on numerous applications from different domains improve the tool and its methodology. In VESSEDIA we tackle the field of IoT through three IoT use-cases. The same experimental approach holds for the VeriFast, Diversity, Contiki, and FlowArmor tools that have evolved along experiments and applications.
• 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.
• Standardisation: In the ISO JTC1 VESSEDIA will produce in three years a normative ISO standard for V&V tools.
• Improved modularity and abstraction: programming languages have improved significantly with abstraction means at the language level allowing more efficient programming and less error prone programs. In VESSEDIA, the connections between design and formal methods will help in the same manner by 1) more abstract descriptions of systems, 2) system-level security properties and their refinements, and 3) integration of detailed specifications at design level.
• Methodology: a proper methodology will be proposed for using the tools, taking into account the environment and the economic and certification constraints.
The expected results of the project concern mainly the analysis of safety and security analysis of IoT applications. We expect the following main results at M36:
- Experimental results from the use-cases: approach to V&V, target of verification, analysis results, quantitative data, and recommendations for other similar applications.
- 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 in the analysis of C++ source code: we expect to improve the ACSL++ specification language to cover the complex traits of C++.
- Certification help through support of the CC certification activities and integration of the VESSEDIA methodology into existing national certification schemes.
- Help for security evaluation through tool support to software evaluation process.
- A new ISO standard on V&V tools.
- On the dissemination side, we expect an enlarged community of users of the project tools, new partnerships with industry on software safety and security, notoriety of project partners in the IoT security domain, improved security evaluation processes and new security training material.

In terms of potential impacts, the project expects 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.
- More users’ trust in ICT products and services through higher level of security and privacy.
- More resilient critical infrastructures and services by a systems approach.
- Systems-oriented metrics allowing managers to assess and predict the level of security of their software.
- Economic impact and European competitiveness by implementing security in software developments right from the start avoiding costly remediation measures.
- Dissemination of results through all available channels and actors.
- Standardisation through the production of a new ISO standard.
- New releases of the project’s core toolkits.

Website & more info

More info: https://vessedia.eu/.