The VESSEDIA project has received funding from the European Union's Horizon 2020 research and innovation programme under grant agreement No. 731453.
Public RTD Deliverables
D1.1 “Security requirements for connected medium security-critical applications“ [September 2017]
This deliverable reports the general methodology developed in T1.1., in which general guidelines for requirement analyses will be reviewed and particularized with respect to the project scope.
D1.3 “Modelling framework Description“ [June 2018]
This document describes the model-based language resulting from T1.2.
D3.1 „Methodological report for modular reasoning for system validation and verification“ [June 2018]
This report will contain the methodology about modular reasoning for system validation and verification (task 3.1).
D4.1 “Metrics for VESSEDIA tools in quality assurance“ [June 2018]
In this deliverable, the definition of metrics defined in Task 4.1. are stated and described.
D4.2 “VESSEDIA approach for security evaluation“ [June 2018]
D4.2 includes the analysis on using VESSEDIA results in security evaluation methodologies (Task 4.2).
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
Abstract: With the wide expansion of multiprocessor architectures, the analysis and reasoning for programs under weak memory models has become an important concern. This work presents MMFilter, an original constraint solver for generating program behaviors respecting a particular memory model. It is implemented in Prolog using CHR (Constraint Handling Rules). The CHR formalism provides a convenient generic solution for specifying memory models. It benefits from the existing optimized implementations of CHR and can be easily extended to new models. We present MMFilter design, illustrate the encoding of memory model constraints in CHR and discuss the benefits and limitations of the proposed technique.
A. Peyrard, N. Kosmatov, S. Duquennoy, S. Raza, "RED-IOT 2018 - Workshop on Recent advances in secure management of data and resources in the IoT", February 2018
Abstract: The number of Internet of Things (IoT) applications is rapidly increasing and allows embedded devices today to be massively connected to the Internet. This raises software security questions. This paper demonstrates the usage of formal verification to increase the security of Contiki, a popular open-source operating system for the IoT. We present a case study on deductive verification of encryption-decryption modules of Contiki (namely, AES–CCM*) using Frama-C, a software analysis platform for C code.
D. Pariente, J. Signoles, "SSTIC - Symposium sur la sécurité des technologies de l'information et des communications", June 2017
Abstract: This paper presents a methodology which combines static analysis and runtime assertion checking in order to automatically generate counter-measures, and execute them whenever a flaw in the code which may compromise the security of an application is detected during execution. Static analysis pinpoints alarms that must be converted into runtime checks. Therefore the verifier is able to only monitor the security critical points of the application. This method allows to strengthen a security-critical source code in a cost-effective manner. We implemented it in the Frama-C framework and experimented it on a real use case based on Apache web server. The paper ends with preliminary considerations on potential perspectives for security evaluation and certification.
J. Burghardt, R. Clausecker, J. Gerlach, H. Pohl, for Frama-C Silicon, April 2017
Abstract: This report provides various examples for the formal specification, implementation, and deductive verification of C programs using the ANSI/ISO-C Specification Language and the Frama-C/WP plug-in of Frama-C (Framework for Modular Analysis of C programs). We have chosen our examples from the C++ standard library whose initial version is still known as the Standard Template Library (STL). The STL contains a broad collection of generic algorithms that work not only on C arrays but also on more elaborate container data structures. For the purposes of this document we have selected representative algorithms, and converted their implementation from C++ function templates to C functions that work on arrays of type int. We will continue to extend and refine this report by describing additional STL algorithms and data structures. Thus, step by step, this document will evolve from an ACSL tutorial to a report on a formally specified and deductively verified standard library for ANSI/ISO-C. Moreover, as ACSL is extended to a C++ specification language, our work may be extended to a deductively verified C++ Standard Library.