Period 1

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).


Static Analysis and Runtime-Assertion Checking: Contribution to Security Counter-Measures
D. Pariente, J. Signoles, "SSTIC - Symposium sur la sécurité des technologies de l'information et des communications", June 2017
expand[ More ]

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.

"ACSL By Example - Towards a Verified C Standard Library"
J. Burghardt, R. Clausecker, J. Gerlach, H. Pohl, for Frama-C Silicon, April 2017
expand[ More ]

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.


Background Image