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.

D2.1. “Basic analyzers intermediate release“[June 2018]
Initial version of front-ends and specification libraries, improved analyzers and prototypes of new analyzers.

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

Period 2

D1.5 “Analyses choice methodology report” [December 2018]
This report presents the findings of T1.4 “Flexible selection of static analyses” regarding a cost-efficient trade-off between basic and sophisticated analyses.

D1.6 Economic Rationale and metrics report [March 2019]
Economic rationale and metrics report of the effectiveness and efficiency of the use of VESSEDIA outcomes This deliverable consists of an academic publication on the topic of the economic rationale (effectiveness and efficiency) on the incentives for the advanced use of VESSEDIA outcomes based on use cases.

D1.7 “Vulnerability discovery methodology” [December 2018]
This report presents ways to detect the most common vulnerabilities using Frama-C.

D3.3 “Guidelines for combination of static and dynamic analyses” [December 2018]
This report is the output of task 3.2 and will contain guidelines for combination of static and dynamic analyses.

D3.2 Preliminary version of the platforms [August 2018]
This deliverable will contain the first prototypes of an environment of technologies to enable modular system verifications and of the “verification as a service” (tasks 3.1 and 3.3)

The VESSEDIA project uses Zenodo as its open research data repository, in order to grant Open Access to scientific publications. Check out our Zenodo community VESSEDIA!

      2019

Tame your annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, and Pascale Le Gall , TAP Conference
[ More ]


Abstract: A common way to specify software properties is to associate a contract to each function, allowing the use of various techniques to assess (e.g. to prove or to test) that the implementation is valid with respect to these contracts. However, in practice, high-level properties are not always easily expressible through function contracts. Furthermore, such properties may span across multiple functions, making the specification task tedious, and its assessment difficult and error-prone, especially on large code bases. To address these issues, we propose a new specification mechanism called meta-properties. Meta-properties are enhanced global invariants specified for a set of functions, capable of expressing predicates on values of variables as well as memory related conditions (such as separation) and read or write access constraints. This paper gives a detailed presentation of meta-properties and their support in a dedicated Frama-C plugin MetAcsl, and shows that they are automatically amenable to both deductive verification and testing. This is demonstrated by applying these techniques on two illustrative case studies.

The Future is Ours: Prophecy Variables in Separation Logic
Ralf Jung, Rodolphe Lepigre, Gaurav Parthasarathy, Marianna Rapoport, Amin Timany, Derek Dreyer, and Bart Jacobs, 47th ACM SIGPLAN Symposium on Principles of Programming Languages
[ More ]


Abstract: Early in the development of Hoare logic, Owicki and Gries introduced auxiliary variables as a way of encoding information about the history of a program’s execution that is useful for verifying its correctness. Over a decade later, Abadi and Lamport observed that it is sometimes also necessary to know in advance what a program will do in the future. To address this need, they proposed prophecy variables, originally as a proof technique for refinement mappings between state machines. However, despite the fact that prophecy variables are a clearly useful reasoning mechanism, there is (surprisingly) almost no work that attempts to integrate them into Hoare logic. In this paper, we present the first account of prophecy variables in a Hoare-style program logic that is flexible enough to verify logical atomicity (a relative of linearizability) for classic examples from the concurrency literature like RDCSS and the Herlihy-Wing queue. Our account is formalized in the Iris framework for separation logic in Coq. It makes essential use of ownership to encode the exclusive right to resolve a prophecy, which in turn enables us to enforce soundness of prophecies with a very simple set of proof rules.

Starvation-free monitors
Jafar Hamin , "16th International Colloquium on Theoretical Aspects of Computing (ICTAC 2019), LNCS
[ More ]


Abstract: Monitors are a synchronization construct which allows to keep a thread waiting until a specific resource for that thread is available. One potential problem with these constructs is starvation; a situation where a thread, competing for a resource, infinitely waits for that resource because other threads, that started competing for that resource later, get it earlier infinitely often. In this paper a modular approach to verify starvation-freedom of monitors is presented, ensuring that each time that a resource is released and its associated condition variable is notified each waiting thread approaches the front of the waiting queue; more specifically, the loop in which the wait command is executed (that checks the waiting condition) has a loop variant. To this end, we introduce notions of publishable resources and publishable obligations, which are published from the thread notifying a condition variable to all of the threads waiting for that condition variable. The publishable resources ensure the waiting threads that they are approaching the front of the waiting queue, by allowing to define an appropriate loop variant for the related loop. The publishable obligations ensure that for any thread waiting for a condition variable v there is another thread obliged to notify v, which only waits for waitable objects whose levels, some arbitrary numbers associated with each waitable object, are lower than the level of v (preventing circular dependencies). We encoded the proposed separation logic-based proof rules in the VeriFast program verifier and succeeded in verifying deadlock-freedom and starvation-freedom of two monitors, having no scheduling policy, which implement two.

Logic against Ghosts: Comparison of Two Proof Approaches for a List Module
Blanchard, Allan; Kosmatov, Nikolai; Loulergue, Frédéric, "The 34th ACM/SIGAPP Symposium On Applied Computing", Apr 2019, Limassol, Cyprus.
[ More ]


Abstract: Modern verification projects continue to offer new challenges for formal verification. One of them is the linked list module of Contiki, a popular open-source operating system for the Internet of Things. It has a rich API and uses a particular list representation that make it different from the classical linked list implementations. Being widely used in the OS, the list module is critical for reliability and security. A recent work verified the list module using ghost arrays. This article reports on a new verification effort for this module. Realized in the Frama-C/Wp tool, the new approach relies on logic lists. A logic list provides a convenient high-level view of the linked list. The specifications of all functions are now proved faster and almost all automatically, only a small number of auxiliary lemmas and a couple of assertions being proved interactively in Coq. The proposed specifications are validated by proving a few client functions manipulating lists. During the verification, a more efficient implementation for one function was found and verified. We compare the new approach with the previous effort based on ghost arrays, and discuss the benefits and drawbacks of both techniques.

Symbolic execution of transition systems with function summaries
Boudhiba, Imen; Gaston, Christophe; Le Gall, Pascale; Prévosto Virgile", 11th International Conference on Tests, 2017.
[ More ]


Abstract: Reactive systems can be modeled with various kinds of automata, such as Input Output Symbolic Transition Systems (IOSTS). Symbolic execution (SE) applied to IOSTS allows computing constraints associated to IOSTS path executions (path conditions). In this context, generating test cases amounts to finding numerical input values satisfying such constraints using solvers. This paper explores the case where IOSTS models contain functions which are outside of the scope of such solvers. We propose to use function summaries which are logical formulas built from concrete values describing some representative input/output data tuples of the function. We define algorithmic strategies to solve path conditions including such functions based on techniques using and enriching function summaries. Our method has been implemented within the Diversity tool and has been applied to several examples..

MetACSL : Specification and Verification of High-Level Properties
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto, Louis Rilling, Pascale Le Gall ", TACAS.
[ More ]


Abstract: Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related) properties of a whole software module are actually established, making it very difficult to assess them. To address this issue, this paper proposes a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in two illustrative case studies.

Specifying I/O using Abstract Nested Hoare Triples in Separation Logic
Willem Penninckx, Amin Timany, Bart Jacobs, FTfJP 2019
[ More ]


Abstract: We propose a separation logic-based approach for modular specification and verification of the I/O behavior of a program. The approach uses higher-order separation logic predicates to express abstract nested Hoare triples that abstractly associate a precondition and a postcondition with an I/O action. The approach supports verifying higher-level I/O actions built on top of lower-level ones (e.g. the I/O abstractions offered by the programming language’s standard library, implemented on top of system calls), as well as virtual I/O actions that in fact only manipulate memory, against specifications that are indistinguishable from those of the “primitive I/O actions”.

      2018

Specifying I/O using Abstract Nested Hoare Triples in Separation Logic
Willem Penninckx, Amin Timany, Bart Jacobs, FTfJP 2019
[ More ]


Abstract: One common approach for verifying safety properties of multithreaded programs is assigning appropriate permissions, such as ownership of a heap location, and obligations, such as an obligation to send a message on a channel, to each thread and making sure that each thread only performs the actions for which it has permissions and it also fulfills all of its obligations before it terminates. Although permissions can be transferred through synchronizations from a sender thread, where for example a message is sent or a condition variable is notified, to a receiver thread, where that message or that notification is received, in existing approaches obligations can only be transferred when a thread is forked. In this paper we introduce two mechanisms, one for channels and the other for condition variables, that allow obligations, along with permissions, to be transferred from the sender to the receiver, while ensuring that there is no state where the transferred obligations are lost, i.e. where they are discharged from the sender thread but not loaded onto the receiver thread yet. We show how these mechanisms can be used to modularly verify deadlock-freedom of a number of interesting programs, such as some variations of client-server programs, fair readers-writers locks, and dining philosophers, which cannot be modularly verified without such transfer. We also encoded the proposed separation logic-based proof rules in the VeriFast program verifier and succeeded in verifying the mentioned programs.

Preprint: Verication Coverage for Combining Test and Proof
Viet Hoang Le, Lo¨ıc Correnson, Julien Signoles and Virginie Wiels, International Conference on Tests and Proofs TAP 2018
[ More ]


Abstract: The V&V practices of safety-critical industries (e.g. avionics) are currently based on either unit testing or unit proof to verify that a function satisfies its low-level requirements in order to be compliant with the highest certification levels [26] (e.g. DO-178C level A for avionic software). In this context, the verification engineer must assess sufficient coverage of both code (structural coverage) and specification (functional coverage). However, there is no shared method for test and proof to measure structural coverage. In practice, this prevents the verification engineer from combining test and automatic proof to verify low-level requirements of a common piece of code in order to mitigate the verification cost. This paper fills this gap between test and proof by introducing a new notion of verification coverage based on mutation coverage. It subsumes functional coverage and structural coverage for both unit testing and unit proof. Consequently, it allows the verification engineer to mix test tools and automatic provers in the verification process for the sake of reducing verification cost, in the sense that the more automation is used during the verification, the less resource is spent to verify the program.

Preprint: Soundness of a Dataflow Analysis for Memory Monitoring
Dara Ly, Nikolai Kosmatov, Julien Signoles, Frédéric Loulergue, ACM SIGAda Ada Letters
[ More ]


Abstract: An important concern addressed by runtime verification tools for C code is related to detecting memory errors. It requires to monitor some properties of memory locations (e.g., their validity and initialization) along the whole program execution. Static analysis based optimizations have been shown to significantly improve the performances of such tools by reducing the monitoring of irrelevant locations. However, soundness of the verdict of the whole tool strongly depends on the soundness of the underlying static analysis technique. This paper tackles this issue for the dataflow analysis used to optimize the E-ACSL runtime assertion checking tool.We formally define the core dataflow analysis used by E-ACSL and prove its soundness.

Runtime Assertion Checking and Static Verification: Collaborative Partners.
Fonenantsoa Maurica, David R. Cok, and Julien Signoles, ISOLA 2018, Limassol, Cyprus
[ More ]


Abstract: One common approach for verifying safety properties of multithreaded programs is assigning appropriate permissions, such as ownership of a heap location, and obligations, such as an obligation to send a message on a channel, to each thread and making sure that each thread only performs the actions for which it has permissions and it also fulfills all of its obligations before it terminates. Although permissions can be transferred through synchronizations from a sender thread, where for example a message is sent or a condition variable is notified, to a receiver thread, where that message or that notification is received, in existing approaches obligations can only be transferred when a thread is forked. In this paper we introduce two mechanisms, one for channels and the other for condition variables, that allow obligations, along with permissions, to be transferred from the sender to the receiver, while ensuring that there is no state where the transferred obligations are lost, i.e. where they are discharged from the sender thread but not loaded onto the receiver thread yet. We show how these mechanisms can be used to modularly verify deadlock-freedom of a number of interesting programs, such as some variations of client-server programs, fair readers-writers locks, and dining philosophers, which cannot be modularly verified without such transfer. We also encoded the proposed separation logic-based proof rules in the VeriFast program verifier and succeeded in verifying the mentioned programs.

Des listes et leurs fantômes : vérification d’un module critique de Contiki avec Frama-C
Allan Blanchardy, Nikolai Kosmatovz, and Frédéric Loulerguex, AFADL 2018, Toulouse, France
[ More ]


Abstract:Les appareils et services connectés, aussi appelés internet des objets (Internet of Things : IoT) sont de plus en plus populaires dans des domaines où la sécurité est critique. Ces questions de sécurité sont une cible de choix pour l'usage de méthodes formelles. Ce travail se concentre sur Contiki, un système d'exploitation open-source populaire pour les objets connectés, qui propose notamment une pile IPv6 pour environnements contraints. Il est implémenté en C avec une attention particulière pour l'optimisation de la consommation mémoire et énergétique, et est disponible pour de nombreuses plateformes physiques. Au début du développement de Contiki en 2002, la sécurité n'était pas un objectif central. La sécurité des communications a été ajoutée plus tard, mais la vérification formelle du code n'a commencé que très récemment. Nous présentons la vérification formelle du module de listes chaînées de Contiki. Ce module est critique pour le système d'exploitation, il est utilisé par 32 modules de Contiki et appelé plus de 250 fois dans la partie coeur du système. Son API est riche, il est possible d'ajouter ou enlever des éléments à n'importe quelle position dans la liste. Elle garantit l'unicité des éléments au sein des listes : avant toute insertion, le module s'assure de supprimer l'élément de la liste avant de l'ajouter à la position voulue. Finalement, Contiki ne permet pas l'allocation dynamique, contrairement aux implémentations classiques des listes, le module de Contiki ne fait donc pas de telle opération. La vérification formelle du module est effectuée grâce au langage de spécification ACSL et au greffon WP de la plate-forme FRAMA-C. Notre approche se base sur des tableaux fantômes (ghost) utilisés comme représentation des listes chaînées.

Synthesizing Invariants by Solving Solvable Loops
de Oliveira, Steven; Bensalem, Saddek; Prevosto, Virgile, September 2017
[ More ]


Abstract: Formal program verification faces two problems. The first problem is related to the necessity of having automated solvers that are powerful enough to decide whether a formula holds for a set of proof obligations as large as possible, whereas the second manifests in the need of finding sufficiently strong invariants to obtain correct proof obligations. This paper focuses on the second problem and describes a new method for the automatic generation of loop invariants that handles polynomial and non deterministic assignments. This technique is based on the eigen vector generation for a given linear transformation and on the polynomial optimization problem, which we implemented on top of the open-sourcetool Pilat.

Ghosts for Lists: A Critical Module of Contiki Verified in Frama-C
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
[ More ]


Abstract: Internet of Things (IoT) applications are becoming increasingly critical and require rigorous formal verification. In this paper we target Contiki, a widely used open-source OS for IoT, and present a verification case study of one of its most critical modules: that of linked lists. Its API and list representation differ from the classical linked list implementations, and are particularly challenging for deductive verification. The proposed verification technique relies on a parallel view of a list through a companion ghost array. This approach makes it possible to perform most proofs automatically using the Frama-C/WP tool, only a small number of auxiliary lemmas being proved interactively in the Coq proof assistant. We present an elegant segment-based reasoning over the companion array developed for the proof. Finally, we validate the proposed specification by proving a few functions manipulating lists.

Ghosts for Lists: from Axiomatic to Executable Specications
Frederic Loulergue, Allan Blanchard, and Nikolai Kosmatov
[ More ]


Abstract: Internet of Things (IoT) applications are becoming increasingly critical and require formal verification. Our recent work presented formal verification of the linked list module of Contiki, an OS for IoT. It relies on a parallel view of a linked list via a companion ghost array and uses an inductive predicate to link both views. In this work, a few interactively proved lemmas allow for the automatic verification of the list functions specifications, expressed in the acsl specification language and proved with the Frama-C/Wp tool. In a broader verification context, especially as long as the whole system is not yet formally verified, it would be very useful to use runtime verification , in particular, to test client modules that use the list module. It is not possible with the current specifications, which include an inductive predicate and axiomatically defined functions. In this early-idea paper we show how to define a provably equivalent non-inductive predicate and a provably equivalent non-axiomatic function that belong to the executable subset e-acsl of acsl and can be transformed into executable C code. Finally, we propose an extension of Frama-C to handle both axiomatic specifications for deductive verification and executable specifications for runtime verification.

MMFilter: A CHR-Based Solver for Generation of Executions under Weak Memory Models
Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue
[ More ]


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.

Towards Formal Verification of Contiki: Analysis of the AES–CCM* Modules with Frama-C
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
[ More ]


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.

      2017

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

Showcases

Background Image


Cookies make it easier for us to provide you with our services. With the usage of our services you permit us to use cookies.