Search

International audience; Validation and Verification (V&V) of autonomous robotic system software is becoming a critical issue. Among the V&V techniques at our disposal, formal approaches are among the most rigorous and trustworthy ones. Yet, the level of skills and knowledge required to use and deploy formal methods is usually quite high and rare. In this paper, we describe an approach that starts from a regular, but rigorous, framework to specify and deploy robotic software components, which can also automatically synthesize a formal model of these components.We describe how we can execute the resulting formal model, in place of a traditional imple- mentation, and show how this provides the opportunity to add powerful monitoring and runtime verification capabilities to a system, e.g., to prevent collisions, or trigger an emergency landing. Since the runtime used to execute formal models is specifically designed to be faithful to their se- mantics, every execution (in the implementation) can be mapped to a trace in the specification. As a result, we can also prove many interesting properties offline, using model-checking techniques. We give several examples, such as properties about schedulability, worst-case traversal time, or mutual exclusion.We believe that having a consistent workflow, from an initial specification of our system, down to a formal, executable specification is a major advance in robotics and opens the way for verification of functional components of autonomous robots and beyond. We illustrate this claim by describing a complete example based on a genuine drone flight controller.

Just-in-Time compilation is a technique to execute programs, where execution is interleaved with optimizations. Just-in-Time compilers often produce fast executions, but are particularly complex. For instance, they reuse various existing techniques: some contain both interpreters to execute programs and traditional compilers to generate optimized machine code. They also use ad hoc techniques like speculation, which consists in predicting the future behavior of the program to generate specialized code that executes particularly fast if the prediction holds. This great complexity can lead to bugs. This thesis tackles their formal verification, to develop Just-in-Time compilers in such a way that one can formally prove that they behave as prescribed by the semantics of the program they execute.We present correctness proofs for their main features, including speculation, dynamic optimizations and machine code generation. We reuse proof techniques from formally verified traditional compilers like CompCert. All our proofs have been mechanized in the Coq proof assistant.; La compilation à la volée est une technique pour exécuter des programmes, où l'exécution est mélangée à des optimisations. Les compilateurs à la volée se distinguent par leur efficacité, mais aussi par leur complexité. Par exemple, ils réutilisent des techniques variées: certains contiennent des interprètes pour exécuter leur programme, mais aussi des compilateurs traditionnels pour générer du code machine optimisé. Ils utilisent également des techniques qui leur sont propres comme la spéculation, qui consiste à prédire le comportement futur du programme et générer du code particulièrement rapide si cette prédiction s'avère vrai.Cette grande complexité peut être à l'origine de bugs. Cette thèse s'attelle à leur vérification formelle, dans le but de développer des compilateurs à la volée dont on peut prouver formellement qu'ils se comportent comme spécifié par la sémantique du programme qu'ils exécutent. Nous présentons des preuves de correction des techniques principales qu'ils utilisent, comme la spéculation, les optimisations dynamiques ou la génération de code machine. Nous réutilisons des techniques de preuves issues de compilateurs traditionnels vérifiés comme CompCert. Nos preuves sont toutes vérifiées mécaniquement dans l'assistant de preuve Coq.

This thesis addresses the problem of reasoning about programs that modify the heap and alter the control flow through effect handlers, a novel programming construct that provides a relatively simple interface to delimited control. This ability to manipulate the control flow is extremely powerful: many programming features -- such as asynchronous programming and coroutines -- that come as built-in packages of traditional programming languages can be expressed in terms of effect handlers. The status of effect handlers as a modular and expressive programming construct is attested by the development of the OCaml programming language, which will have support for handlers in its next major release. This event makes the problem of unveiling the logical principles that govern effect handlers even more pressing. In particular, how to reason abstractly about a continuation, rather than thinking concretely as a fragment of the stack? Moreover, can we reason separately about a program that performs effects and a program that handles these effects? This thesis answers these questions by introducing Hazel, a Separation Logic for effect handlers, built as an extension of Iris. Hazel introduces a novel specification language by means of which one can describe the behavior of programs, including continuations. The logic allows one to compose specifications in a modular fashion through familiar reasoning rules, such as the bind rule and the frame rule, and novel ones, such as the reasoning rules for handling and performing effects. To assess the applicability of Hazel as a tool to formally reason about programs, this thesis includes the verification of a number of case studies: (1) a program that transforms a higher-order iteration method into a lazy sequence; (2) a library for asynchronous computation; and (3) a library for reverse-mode automatic differentiation.This thesis also explores variants of the Hazel logic for different languages in the design space of effect handlers. One such variant, for example, is Maze, a logic for handlers with multi-shot continuations, i.e., continuations that can be resumed multiple times. The applicability of Maze is assessed through the verification of a simple SAT solver that uses multi-shot continuations to implement backtracking and through the design of reasoning rules for the undelimited-control operators callcc and throw. Another variant is TesLogic, a logic for a language with support for the dynamic generation of effect labels, identifiers used by both a program that performs effects and a program that handles effects as a way to specify the correspondence between these two programs.The main application of TesLogic is in the study of type systems for effect handlers. The question of devising a static type discipline for effect handlers is the subject of an open debate, which seems to suggest a dichotomy: in order to achieve simple and strong subtyping rules, one side argues in favor of imposing a restriction to lexically scoped handlers, while the opposite side argues in favor of complex programming constructs, such as effect coercions. This thesis makes a contribution to this debate by introducing Tes, a type system that is not restricted to lexically scoped handlers, and that supports powerful subtyping rules without the introduction of effect coercions. The soundness of Tes follows from the interpretation of typing judgments as specifications written in TesLogic. The results of this thesis have been formalized in the Coq Proof Assistant.; Cette thèse s'interèsse à la conception des méthodes formelles pour raisonner sur les programmes impératifs qui peuvent modifier le flot de contrôle à travers les gestionnaires d'effets, une nouvelle primitive de programmation offrant une interface relativement simple aux opérateurs de contrôle délimité. Les gestionnaires d'effets sont extrêmement puissants en tant qu'outil de programmation: plusieurs primitives et modes de programmation --tel que la programmation asynchrone -- souvant supportés par les langages traditionnels comme des parties intégrés de ces langages peuvent être implémentés à l'aide des gestionnaires d'effets. La réputation des gestionnaires d'effets en tant qu'un concept de programmation puissant et modulaire est attesté par le développement du langage OCaml, qui aura le support pour les gestionnaires d'effets dans sa prochaine version majeure. Cet événement fait de la recherche des principes logiques derrières les gestionnaires d'effets un problème encore plus pressant. En particulier, comment peut-on raisonner à propos d'une continuation de façon abstraite plutôt que de façon concrète en tant qu'un morceau de la pile d'exécution? Comment peut-on raisonner à propos d'un programme qui lance des effets séparément du programme qui attrape ces effets?Cette thèse répond à ces questions en introduisant Hazel, une Logique de Séparation pour les gestionnaires d'effets. \hazel introduit unnouveau langage de spécification permettant la description du comportement des programmes, y compris des continuations. Cette logique permet aussi la composition des spécifications de façon modulaire, soit par l'application de règles de raisonnement habituelles, tel que la règle de liaison ou la règle de l'encadrement; soit par l'application de règles nouvelles, tel que les règles pour lancer ou capturer des effets. Pour évaluer l'applicabilité de Hazel en tant qu'outil pour le raisonnement formel sur les programmes, cette thèse inclut la vérification des nombreux cas d'études: (1) la conversion générique d'une méthode d'itération d'ordre supérieur vers une séquence paresseuse; (2) une bibliotèque pour la programmation asynchrone; (3) une bibliotèque pour la différentiation automatique en arrière. Cette thèse étudie aussi des variantes de Hazel pour les différentesconceptions de gestionnaires d'effets. Une telle variante est Maze, une logique pour les gestionnaires d'effets avec des continuations à plusieurs appels (multi-shot). L'applicabilité de Maze est évaluée par (1) la vérification d'un solveur SAT simple qui utilise des continuations pour implémenter le retour sur trace et par (2) la conception des règles de raisonnement pour callcc et throw.Une autre variante est TesLogic, une logique pour raisonner sur la génération dynamique de noms d'effets. La principale application de TesLogic est dans l'étude des systèmes de types pour les gestionnaires d'effets. La conception d'un système de types pour les gestionnaires d'effets est le sujet d'un débat actif: pour offrir des règles simples et permissives de sous-typage, un coté soutient la restriction des gestionnaires d'effets aux gestionnaires d'effets de portée lexicale, tandis que l'autre coté soutient l'adoption des coercions d'effets. Cette thèse contribue à ce débat en introduisant Tes, un système de types qui (1) n'est pas restreint aux gestionnaires d'effets de portée lexicale, (2) n'introduit pas les coercions d'effets, et (3) admet des règles de sous-typage puissantes. La sûreté de Tes est prouvée à l'aide d'une interprétation des jugements de typage en tant que spécifications écrites en TesLogic. Les résultats de cette thèse sont formalisés dans l'assistant de preuve Coq.

This thesis invests the field of cybersecurity for small computer systems (embedded systems/connected objects/low-end devices, of type microcontroller) and more precisely aims to bring strong memory isolation guarantees for tasks executing on them.The heterogeneity and strong resource constraints (memory, computing power, energy) of constrained embedded systems require tailored solutions. The embedded software life cycle and the specific hardware platforms challenge us to reconsider the security schemes that leave open memory vulnerability issues, still prevailing today. Furthermore, the risk of vulnerability exploits elevates with the growing number of use cases (smart environments in general) implying increased complexity within these systems and with the burgeoning market of the Internet-of-Things (notably for remote update purposes). As a consequence, cyber attackers can take profit from these vulnerabilities to take remote control of these connected systems in a very scalable way.In this context, the thesis proposes to design a kernel for constrained objects that is able to bring strong memory isolation guarantees. It studies the blend of high flexibility and strong security for this class of devices with the aim of security-by-design without functional loss. The thesis presents two main contributions dealing with software attacks on memory.The first contribution is an Operating System (OS) kernel, named Pip-MPU, that offers a hardware-based isolation solution with a degree of flexibility outperforming current solutions. Pip-MPU is adapted from the Pip protokernel initially designed for high-end/general-purpose computers that are provided with more furnished and different hardware platforms than the ones of constrained objects. For that, the designed kernel is a complete refactoring of Pip and offers a security mechanism based on the Memory Protection Unit (MPU), a unit of the processor, which enables hardware-based access control on memory resources. Despite strong limitations due to the limited hardware platform, Pip-MPU is as flexible as its parent project Pip. With a code base size of less than 10 Kb and about 16% extra costs in terms of performance and energy consumption, Pip-MPU reduces the number of privileged operations by 99% and the attack surface of the accessible application memory by 98%.The second contribution is the demonstration of strong isolation guarantees by the use of formal methods. Several kernel services have been proved against isolation by the use of the Coq Proof Assistant. The proved properties are Pip's security properties that enforce a strict memory isolation security model. To our knowledge, no state-of-the-art solution offering MPU-based isolation has been proved before. We develop novel proof conduct techniques and propose new metrics to follow the proof effort and evaluate the hypotheses supporting the proofs.All the contributions developed in this thesis are made publicly available under open-source licences.; Cette thèse s'inscrit dans la thématique de la sécurité des petits systèmes informatiques (systèmes embarqués/objets connectés, de type microcontrôleur) et plus précisément vise à apporter des fortes garanties d'isolation mémoire pour les tâches qui s'y exécutent.L'hétérogénéité et les fortes contraintes en ressources (espace mémoire, puissance de calcul, énergie) nécessitent la mise en place de solutions sur mesure pour les systèmes embarqués contraints. Le cycle de vie des logiciels embarqués et les architectures matérielles spécifiques imposent de repenser la manière de mettre en oeuvre la sécurité qui, encore aujourd'hui, laisse ouvertes des problématiques de vulnérabilité mémoire. De plus, les risques d'exploitation de ces vulnérabilités grandissent avec l'émergence de nouveaux cas d'utilisation (environnements intelligents de manière générale) impliquant des systèmes de plus en plus complexes et l'explosion du nombre de systèmes connectés (notamment pour des besoins de mise à jour à distance). En conséquence, des cyber-attaquants peuvent tirer profit de telles vulnérabilités pour prendre le contrôle à distance de ces systèmes connectés de façon massive.Dans ce cadre, la thèse propose d'élaborer un noyau destiné aux petits objets qui soit capable d'apporter des garanties fortes d'isolation mémoire. Elle étudie l'association entre flexibilité élevée et forte sécurité au sein d'objets contraints pour une sécurité dès la conception sans perte fonctionnelle. Elle est constituée de deux contributions principales qui répondent aux attaques logicielles sur la mémoire.La première contribution est un noyau de système d'exploitation, appelé Pip-MPU, qui propose une solution d'isolation ancrée dans le matériel et offrant une flexibilité dépassant les solutions actuelles. Pip-MPU est adapté du protonoyau Pip initialement destiné à des ordinateurs généralistes dotés d'une plateforme matérielle plus fournie et différente de celle des objets contraints. Pour cela, le noyau conçu est une refonte totale de Pip et propose un mécanisme de sécurité basé sur la Memory Protection Unit (MPU), une unité du processeur, qui permet un contrôle d'accès matériel aux ressources. Malgré les fortes limitations imposées par la plateforme matérielle, Pip-MPU est aussi flexible que ce que permet la MMU en termes de sécurité. Du haut de ses 10 Ko de code et 16% de surcoût en termes de performances et de consommation d'énergie, Pip-MPU réduit le nombre d'opérations privilégiées exécutées de 99% et la surface d'attaque de la mémoire accessible depuis l'application de 98%.La deuxième contribution est l'obtention de garanties fortes de l'isolation par l'usage de méthodes formelles. Plusieurs services du noyau ont été formellement prouvés pour l'isolation à l'aide de l'assistant de preuve Coq. Les propriétés prouvées sont les propriétés de sécurité de Pip imposant son modèle de sécurité d'isolation stricte. A notre connaissance, aucun autre système de l'état de l'art proposant de l'isolation par MPU n'a été formellement prouvé auparavant. Nous développons des nouvelles techniques de conduite de preuve et proposons de nouvelles métriques permettant de suivre l'effort de preuve et d'évaluer les hypothèses soutenant les preuves.Toutes les contributions de la thèse sont en source ouverte.

Distributed systems involve processes that run independently and communicate asynchronously. While they capture a wide range of use cases and are hence, ubiquitous in our world, it is also particularly difficult to ensure their correctness. In this thesis, we model such systems using mathematical and logical formulation, and try to algorithmically verify them. In particular, we focus on FIFO (First In First Out) machines, with one or more finite-state machines communicating via unbounded reliable FIFO buffers.As most verification problems are known to be undecidable for FIFO machines, we focus on various subclasses and approximations of the model. The first model we consider are branch-well structured transition systems (branch-WSTS), a class which strictly includes the well-known class of WSTS. We study the problems of boundedness and termination for such systems, and demonstrate some examples of them. We also define another class of systems where the monotony condition is relaxed and show that a variant of the coverability problem is decidable under effectivity conditions.We then study the restriction of input-boundedness on FIFO machines, and show that rational reachability and various other properties are decidable for FIFO machines under the input-bounded restriction. In doing so, we answer a long standing open question regarding the reachability for input-bounded FIFO machines. We also derive some complexity bounds by considering the simplest case, a FIFO machine with a single channel.Another restriction that we study is synchronizability in communicating systems. In particular, we study this notion for MSCs (Message Sequence Charts), which is a model to represent executions of a communicating system. We show that if any set of MSCs can satisfy two properties, namely MSO (Monadic Second-order Logic) definability and bounded (special-)tree width, then synchronizability is decidable. Moreover, reachability and model-checking are also decidable within this framework. We also unify some classes from the literature using this framework, and for some other classes, show their undecidability.; Les systèmes distribués concernent des processus qui s’exécutent indépendamment et communiquent de manière asynchrone. Bien qu’ils couvrent un large éventail de cas d’utilisation et soient donc omniprésents dans notre monde, il est particulièrement difficile de garantir leur exactitude. Dans cette thèse, nous modélisons de tels systèmes en utilisant une formulation mathématique et logique, et nousles vérifions algorithmiquement. En particulier, nous nous concentrons sur les automates FIFO (First In First Out), et plus précisément sur des systèmes à un ou plusieurs automates finis qui communiquent via des canaux FIFO fiables pouvant contenir des mots de longueur arbitrairement grande. Comme la plupart des problèmes de vérification sont connus pour être indécidables pour les automates FIFO, nous nous concentrons sur diverses sous-classes et approximations du modèle. Le premier modèle que nous considérons est celui des systèmes de transition bien structurés sur les branches d’états accessibles (branch-WSTS), une classe qui inclut strictement la classe des WSTS. Nous étudions les problèmes de finitude des canaux et de terminaison pour de tels systèmes, et nous en montrons quelques exemples. Nous définissons également une autre classe de systèmes où la condition de monotonie est relâchée et nous montrons qu’une variante du problème de couerture est décidable sous des conditions naturelles d’effectivité. Nous étudions ensuite la restriction de la limitation de l’entrée (input-boundedness) sur les canaux FIFO et nous montrons que l’accessibilité rationnelle et diverses autres propriétés sont décidables pour les automates FIFO. Ce faisant, nous répondons à une question ouverte concernant l’accessibilité des automates FIFO limités en entrée. Nous dérivons également certaines bornes de complexité en considérant le cas le plus simple, un automate FIFO avec un seul canal. Une autre restriction que nous étudions est la synchronisabilité dans les systèmes communicants. En particulier, nous étudions cette notion pour les MSCs (Message Sequence Charts), qui est un modèle pour représenter les exécutions d’un système communicant. Nous montrons que si un ensemble quelconque de MSC satisfait les deux propriétés suivantes, à savoir la définissabilité MSO (Monadic Second-order Logic) et la (spécial) largeur d’arbre (tree-width) bornée, alors la synchronisabilité est décidable. De plus, l’accessibilité et le model checking sont également décidables dans ce cadre. Nous unifions alors certaines classes de la littérature à l’aide de ce cadre, et pour certaines autres classes, nous montrons leur indécidabilité.

Formal verification is a solution to increase the system’s implementation reliability. In our thesis work, we are interestedin using these methods to verify multi-core RTOS. We propose a model-checking approach using time Petri nets extended with colored transitions and high-level features. We use this formalism to model the Trampoline multi-core OS, compliant with the OSEK/VDX and AUTOSAR standards. We first define this formalism and show its suitability for modeling real-time concurrent systems. We then use this formalism to model the Trampoline multi-core RTOS and verify by model-checkingits conformity with the AUTOSAR standard. From this model, we can verify properties of both the OS and the application, such as the schedulability of a real-time system and the synchronization mechanisms: concurrent access to the data structures of the OS, multicore scheduling, and inter-core interrupt handling. As an illustration, this method allowed the automatic identification of two possible errors of the Trampoline OS in concurrent execution, showing insufficient data protection andfaulty synchronization.; La vérification formelle est une solution pour augmenter la fiabilité de l’implémentation du système. Dans notre travail de thèse, nous nous intéressons à l’utilisation de ces méthodes pour la vérification des systèmes d’exploitation multi-coeurs temps réel. Nous proposons une approche de model-checking utilisant les réseaux de Petri temporels, étendus avec des transitions colorées et des fonctionnalités de haut niveau. Nous utilisons ce formalisme pour modéliser le système d’exploitation multi-coeur Trampoline, conforme aux standards OSEK/VDX etAUTOSAR. Nous définissons dans un premier temps ce formalisme et montrons son adéquation avec la modélisation de systèmes concurrents temps reel. Nous utilisons ensuite ce formalisme pour modéliser le système d’exploitation multi-coeur Trampoline et vérifions par model-checking sa conformité avec le standard AUTOSAR. À partir de ce modèle, nous pouvons vérifier des propriétés aussi bien sur l’OS que sur l’application telles que l’ordonnançabilité d’un système tempsréel ainsi que les mécanismes de synchronisation : accès concurrents aux structures de données du système d’exploitation, ordonnancement multi-coeur et traitement des interruptions inter-coeur. À titre d’illustration, cette méthode a permis l’identification automatique de deux erreurs possibles de l’OS Trampoline dans l’exécution concurrente, montrant une protection insuffisante des données et une synchronisation défectueuse.

Computing has become omnipresent in daily life through tools that are technologically enriched and increasingly connected to the Internet. When these objects stop working due to a combination of circumstances, it can have dramatic consequences on the safety of people who depend on them. Their functioning can also be altered by a malicious will to harm and which, during an attack, will create a situation conducive to a targeted malfunction. In this work, we explore the use of formal methods in an embedded and cyber-physical environment. First, we use F* to model the safety of programs on an Arduino. In a second step, we implement LIO (Library Input Output) in F* in a system or embedded context. We put forward an approach that allows to choose between a static verification and a dynamic verification in order to reduce the proof load or the cost at runtime. We also propose a mechanization of the non-interference proof using metaprogramming. This proof focuses on the interaction between the program and the library rather than on the library only.; L’informatique est devenue omniprésente dans la vie de tous les jours au travers d’outils de plus en plus riches technologiquement et de plus en plus connectés à internet. Lorsque ces objets arrêtent de fonctionner suite à un concours de circonstances, cela peut avoir des conséquences dramatiques sur la sûreté des personnes qui en dépendent. Leur fonctionnement peut être aussi altéré par une volonté malveillante de nuire et qui lors d’une attaque créera la situation propice à un dysfonctionnement ciblé. Dans ce travail, nous explorons l’utilisation des méthodes formelles dans un environnement embarqué et cyber-physique. Dans un premier temps, nous utilisons F* pour modéliser la sûreté des programmes sur une Arduino. Puis nous implémentons LIO (Library Input Output) en F* dans un contexte système ou embarqué. Nous mettons ici en avant une approche qui permet de choisir entre une vérification statique et une vérification dynamique afin de réduire la charge de preuve ou le coût à l’exécution. Nous proposons également une mécanisation de la preuve de non-interférence en utilisant la métaprogrammation. Cette preuve porte sur l’interaction entre le programme et la librairie plutôt que sur la librairie seulement.

International audience; This paper introduces a formal workflow for modeling software/hardware systems in order to explore the effects of fault injections and evaluate the robustness to fault injection attacks. We illustrate this workflow on four versions of a PIN authentication code, embedding different software countermeasures. The code is symbolically evaluated on two implementations of the RISC-V CV32E40P core: the original implementation from the OpenHW group and an implementation that integrates protection of the pipeline control signals. On the original, unprotected core, our formal workflow exposes various vulnerabilities, including previously unknown ones, whereas, on the protected core, it confirms the effectiveness of the proposed countermeasures.

Tensor compilers are used in domains such as image processing and deep learning to generate efficient low-level code from high-level specifications on multidimensional tensors. After the application of both loop transformations and algebraic simplifications to the specification, the resulting low-level code can have a drastically different structure. This makes the formal verification of tensor compilers an arduous task, unsuitable for standard bisimulation techniques. I propose a new method for the verification of tensor compilers in the presence of loop and algebraic transformations. This method draws inspiration from polyhedral techniques for program representation, and relies on a refinement mapping from assignments in the low-level code to tensor definition in the specifications provided by the tensor compiler. Each run of the compiler is verified by an independent verification tool implemented in OCaml, making the method an instance of translation validation. This verification tool is tested on Halide, an industrial-grade tensor compiler.; Les compilateurs de tenseurs sont utilisés dans des domaines comme le traitement d'image et l'apprentissage profond pour générer du code bas niveau efficace à partir de spécification de haut niveau sur des tenseurs multi-dimensionnels. Le code généré peut présenter une structure drastiquement différente de celle de la spécification suite à l'application de transformations de boucles et de simplifications algébriques. La vérification formelle des compilateurs de tenseurs est donc une tâche ardue, qui ne peut être traitée par les techniques standard à base de bisimulations. Je propose une nouvelle méthode pour la vérification de compilateurs de tenseurs en présence de transformations algébriques et de boucles. Cette méthode s'inspire des techniques polyédriques de représentation de programmes, et s'appuie sur une association de raffinement depuis les affectations dans le code bas niveau vers les définitions de tenseurs dans la spécification fournie par le compilateur. Chaque exécution du compilateur est vérifiée par un outil de vérification indépendant implanté en OCaml, faisant donc de la méthode un validateur de traduction. Cet outil de vérification est testé sur Halide, un compilateur de tenseurs de niveau industriel.

International audience; TAMARIN is a popular tool dedicated to the formal analysis of security protocols. One major strength of the tool is that it offers an interactive mode, allowing to go beyond what pushbutton tools can typically handle. TAMARIN is for example able to verify complex protocols such as TLS, 5G, or RFID protocols. However, one of its drawback is its lack of automation. For many simple protocols, the user often needs to help TAMARIN by writing specific lemmas, called "sources lemmas", which requires some knowledge of the internal behaviour of the tool. In this paper, we propose a technique to automatically generate sources lemmas in TAMARIN. Following the intuition of manually written sources lemmas, our lemmas try to keep track of the origin of a term by looking into emitted messages or facts. We prove formally that our lemmas indeed hold, for arbitrary protocols that make use of cryptographic primitives that can be modelled with a subterm convergent equational theory (modulo associativity and commutativity). We have implemented our approach within TAMARIN. Our experiments show that, in most examples of the literature, we are now able to generate suitable sources lemmas automatically, in replacement of the handwritten lemmas. As a direct application, many simple protocols can now be analysed fully automatically, while they previously required user interaction.

Fault diagnosis is a crucial and chal- lenging task in the automatic control of complex systems, whose efficiency depends on a system property called diagnosability. Diagnosability describes the system property allowing one to determine at design stage whether a given fault occurring online will be identifiable with certainty based on the available observations, which is an alternative to testing that can only show the presence of failures without guaranteeing their absence. The diagnosability problem of discrete event systems has received considerable attention in the literature, but little work takes into account explicit time constraints during this analysis. However such constraints are naturally present in real-life systems and cannot be neglected considering their impact on this property. We proposed in our master work a new SMT (Satisfiability Modulo Theories)- based approach to verify bounded time diagnosability on timed automata. The idea is to encode in SMT the necessary and sufficient condition for diagnosability. In order to improve the efficiency of our method (the problem is PSPACE- complete), we propose now an incremental extension of it based on the use of parameterized over- and under-approximations generalizing the CEGAR (CounterExample-Guided Abstraction Refinement) method. We show the improvement provided through experimental results. Nevertheless, diagnosability is a quite strong property, which generally requires a high number of sensors. Consequently, it is not rare that developing a diagnosable system is too expensive. In order to guarantee from design an adequate level of safety in an economical and efficient way, we propose two approaches. The first one consists in designing diagnosable discrete event systems by using delay blocks. Indeed, what if a system is revealed as non- diagnosable? One classical way is to add sensors. We propose a new non-intrusive way to make diagnosable a non-diagnosable system by merely adding delay blocks on some observable events, thus deferring their observations. As far as we know, this is the first attempt to remove non- diagnosability with delay blocks without using controllable events or changing the structure of systems. Our approach is encoded into an SMT for- mula, whose correctness and efficiency are demonstrated by our experimental results. The second one consists in analyzing a new system property called manifestability, that is a weaker requirement on system observations for having a chance to identify online fault occurrence and can be verified at design stage. Intuitively, this property makes sure that a faulty system can- not always appear healthy, i.e., has at least one future behavior after fault occurrence observably distinguishable from all normal behaviors. We first define the manifestability of finite state automata for discrete event systems and propose an algo- rithm with PSPACE complexity to automatically verify it and prove that the problem of manifestability verification itself is PSPACE-complete. The experimental results show the feasibility of our algorithm from a practical point of view. Then we define the manifestability of real-time systems modeled by timed automata by taking into account time constraints, and extend our approach to verify manifestability for these systems, proving that it is undecidable in general but, under some restricted conditions, becomes PSPACE-complete. Finally we encode this property into an SMT for- mula, whose satisfiability witnesses manifestability, before presenting experimental results showing the scalability of our approach.; Le diagnostic de pannes est une tâche cruciale et difficile dans le contrôle automatique des systèmes complexes, dont l’efficacité dépend d’une propriété du système appelée diagnosticabilité. La diagnosticabilité décrit la propriété du système permettant de déterminer dès la phase de conception si un défaut donné se produisant en ligne sera identifiable avec certitude sur la base des observations disponibles, ce qui est une alternative aux tests qui ne peuvent que montrer la présence de défaillances sans garantir leur absence. Le problème de diagnosticabilité des systèmes à événements discrets a reçu une attention considérable dans la littérature, mais peu nombreux sont les travaux qui prennent en compte des contraintes de temps explicites lors de cette analyse. Or de telles contraintes sont naturellement présentes dans les systèmes réels et ne peuvent être négligées compte tenu de leur impact sur cette propriété. Nous avons proposé dans notre travail de master une nouvelle approche à base de SMT (Satisfiability Modulo Theories) pour vérifier la diagnosticabilité en temps borné sur les automates temporisés. Afin d’améliorer l’efficacité de notre méthode (le problème est PSPACE-complet), nous en proposons à présent une extension incrémentale fondée sur l’utilisation de sur- et sous-approximations paramétrées dans une généralisation de la méthode CEGAR (raffinement d’abstraction guidé par un contre-exemple). Nous montrons l’amélioration apportée au travers de résultats expérimentaux. Néanmoins, la diagnosticabilité est une propriété assez forte, qui nécessite généralement un nombre élevé de capteurs. Par conséquent, il n’est pas rare que le développement d’un système diagnosticable soit trop coûteux. Afin de garantir dès la conception un certain niveau de sûreté de fonctionnement de manière économique et efficace, nous proposons deux approches. La première consiste à concevoir des systèmes à événements discrets diagnosticables en utilisant des blocs de retard. En effet, que se passe-t-il si un système se révèle comme non diagnosticable ? Une manière classique est d’ajouter des capteurs. Nous proposons une nouvelle manière non intrusive de rendre diagnosticable un système non diagnosticable en ajoutant simplement des blocs de retard sur certains événements observables, reportant ainsi leurs observations. Notre approche est codée dans une formule SMT, dont l’exactitude et l’efficacité sont démontrées par nos résultats expérimentaux. La seconde consiste à analyser une nouvelle propriété du système appelée manifestabilité, qui est une exigence plus faible sur les observations du système pour avoir une chance d’identifier l’occurrence des défauts en ligne et peut être vérifiée au stade de la conception. Intuitivement, cette propriété garantit qu’un système défectueux ne peut pas toujours apparaître sain, c’est-à-dire qu’il a au moins un comportement futur après l’apparition d’un défaut qui se distingue par l’observation de tous les comportements normaux. Nous définissons d’abord la manifestabilité des automates à états finis pour les systèmes à événements discrets et proposons un algorithme de complexité PSPACE pour la vérifier automatiquement et prouvons que le problème de vérification de la manifestabilité lui-même est PSPACE- complet. Les résultats expérimentaux montrent la faisabilité de notre algorithme d’un point de vue pratique. Ensuite, nous définissons la manifestabilité des systèmes temps-réel modélisés par des automates temporisés en tenant compte des contraintes de temps, et étendons notre approche pour vérifier la manifestabilité de ces systèmes, prouvant qu’elle est indécidable en général mais, sous certaines conditions restreintes, devient PSPACE- complet. Enfin, nous encodons cette propriété dans une formule SMT, dont la satisfaisabilité témoigne de la manifestabilité, avant de présenter des résultats expérimentaux montrant le passage à l’échelle de notre approche.

International audience; In this paper, we present our ongoing work on verification activities of the software used in a safety-critical embedded system dedicated to autonomous vehicles. These activities are focused on the use of formal methods for the verification of functional properties on the embedded code, and statistical methods for the analysis of its Worst-Case Execution Time (WCET). The project's goal is to address some technical barriers of software verification that will impact the safety demonstration of future autonomous driving systems. These barriers are challenging because of the high complexity of an embedded hardware and software, and appeal for methods and tools reaching the highest level of rigorousness.

Many security-critical applications need efficient and secure implementations of cryptographic algorithms. To address this demand, general-purpose cryptographic libraries like OpenSSL include dozens of mixed assembly-C implementations for each primitive, highly optimized for multiple popular platforms. Most of these optimizations exploit single-instruction, multiple-data (SIMD) parallelism that significantly changes the structure of the code, making it no longer resemble the original scalar algorithm. However, despite years of careful design and implementation, bugs and attacks continue to be found in such optimized code. These include memory safety errors, timing leaks, and functional correctness bugs. The probability of catching such bugs by testing is extremely low, but they still can be exploited to conduct an attack. We advocate the use of formal verification to mathematically prove the absence of such implementation bugs. Unlike other approaches, such as testing and auditing, it provides strong guarantees that code is memory safe, functionally correct against its high-level specification, and secret independent (``constant-time'') to protect against certain timing side-channel attacks. The challenge is to verify hundreds of thousands of lines of highly-optimized code, and, hence, a more systematic approach is needed. This thesis presents a new approach towards building a formally verified high-performance multi-platform cryptographic library that compiles generic verified code written in F* to optimized C code for different platforms, composable with verified assembly. Our approach reduces programming and verification effort by sharing code between implementations of an algorithm for different platforms and between implementations of different cryptographic primitives. Our library incorporates the results of three projects, each described in its own chapter. First, we show how to write verified portable C and mixed assembly-C implementations for the Curve25519 elliptic curve. Second, we show how to write verified vectorized implementations for platforms that support 128-bit, 256-bit, and 512-bit SIMD vector instructions for the ChaCha20 encryption algorithm, the Poly1305 one-time MAC, and the SHA-2 and Blake2 families of hash algorithms. Third, we show how to write verified portable C implementations for the RSA-PSS and Ed25519 signature schemes and for the Finite-Field Diffie-Hellman key exchange over standard groups. Hence, we developed a new version of the open-source cryptographic library HACL*, which now includes the first verified implementations of, for example, RSA-PSS and the first verified vectorized implementations on ARM Neon and AVX512. Our work closes the performance gap between verified and high-performance unverified cryptographic implementations. Various algorithms from our verified cryptographic library are already deployed in Mozilla's NSS cryptographic library, the Wireguard VPN, the Zinc crypto library for the Linux Kernel, the Tezos blockchain, ElectionGuard, and msQuic. The library can be further improved with respect to side-channels protections and performance. Future work can build upon our results to provide high-assurance implementations of newly designed constructions for post-quantum and lightweight cryptography and coming standards for multi-party threshold cryptography.; Beaucoup de logiciels critiques d'un point de vue sécurité ont besoin d'implémentations d'algorithmes cryptographiques sûres et performantes. Pour répondre à ce besoin, des bibliothèques cryptographiques généralistes comme OpenSSL incluent des douzaines d'implémentations hybrides C/Assembleurs pour chaque primitive, chacune de ces implémentations étant spécialisée et optimisée pour une plateforme répandue. La plupart des optimisations présentes dans ces implémentations exploitent le parallélisme Single Instruction, Multiple Data (SIMD) qui nécessite de changer de manière significative la structure du code, de telle sorte qu'il ne ressemble plus que très peu à l'algorithme scalaire originel. Cependant, et malgré des années de conception et d'implémentation méticuleuse, des bugs et attaques continuent d'être trouvées dans ces bases de code optimisées. Ces bugs et attaques incluent des erreurs de sûreté mémoire, des fuites d'information par attaque temporelle et des bugs de correction fonctionnelle. La probabilité de détecter ces bugs par des méthodes de test est extrêmement faible, mais ils peuvent quand même être exploités pour conduire une attaque. Nous défendons l'utilisation de méthodes formelles afin de prouver mathématiquement l'absence de tels bugs dans les implémentations. À l'inverse d'autres approches comme le test ou l'audit, l'utilisation de méthodes formelles apporte des garanties forte concernant la sûreté mémoire du code, sa correction fonctionnelle par rapport à une spécification haut-niveau, et enfin son indépendance par rapport aux données secrètes (constant-time) qui protège contre certaines attaques temporelles par canaux auxiliaires. Le défi est ici de vérifier des centaines de milliers de lignes de code extrêmement optimisées ; nous avons donc besoin d'une approche systématique à ce problème. Cette dissertation présente une nouvelle approche pour la construction d'une bibliothèque cryptographique multi-plateforme formellement vérifiée qui compile du code générique vérifié écrit en F* vers du code C optimisé pour différentes plateformes, que l'on peut également composer avec de l'assembleur vérifiée. Notre approche réduit l'effort de programmation et de vérification en partageant le code entre les implémentations d'un même algorithme pour différentes plateformes, et entre les implémentations de primitives cryptographiques différentes. Notre bibliothèque incorpore les résultats de trois projets qui sont chacun décrit dans leur propre chapitre. Premièrement, nous montrons comment écrire des implémentations de la courbe elliptique Curve25519 en C pur (pour la portabilité) et en un mélange de C et d'assembleur. Deuxièmement, nous montrons comment écrire des implémentations vérifiées et vectorisées de l'algorithme de chiffrement Chacha20, de l'algorithme d'authentification à usage unique Poly13015, et des familles d'algorithmes de hash SHA-2 et Blake2, pour des plateformes qui supportent des vecteurs SIMD de 128, 256 et 512 bits. Troisièmement, nous montrons comment écrire des implémentations vérifiées en C pur (pour la portabilité) pour les schémas de signature RSA-PSS et Ed25519 pour l'échange de clés en champ fini Diffie-Hellman sur des groupes standards. Ainsi, nous développons une nouvelle version de la bibliothèque cryptographique open-source HACL*, qui inclue par exemple désormais les premières implémentations vérifiées de RSA-PSS et les premières implémentations vectorisées vérifiées sur ARM Neon et AVX512. Notre travail réduit l'écart de performance entre les versions vérifiées et non-vérifiées des implémentations cryptographiques à haute performance. De nombreux algorithmes de notre bibliothèque cryptographique vérifiée sont déjà déployés dans la bibliothèque cryptographique NSS de Mozilla, dans le VPN Wireguard, dans la bibliothèque cryptographique vérifiée Zinc du noyau Linux, dans la blockchain Tezos, ainsi que dans ElectionGuard et msQuic. La bibliothèque pourra être encore améliorée en termes de protection contre les attaques par canaux auxiliaires, ainsi qu'en termes de performance. Notre futur travail sur le sujet pourra construire sur les résultats présentés ici pour apporter des implémentations à haut niveau d'assurance de constructions cryptographiques nouvellement conçues pour la cryptographie post-quantique et légère, ainsi que pour les standards à venir de la cryptographie multi-acteurs à seuil.

The timing behavior of real-time systems is often validated through timing analyses, which are yet jeopardized by execution phenomena called timing anomalies (TAs). A counter-intuitive TA manifests when a local speedup eventually leads to a global slowdown, and an amplification TA, when a local slowdown leads to an even larger global slowdown.While counter-intuitive TAs threaten the soundness/scalability of timing analyses, tools to systematically detect them do not exist. We set up a unified formal framework for systematically assessing the definitions of TAs, concluding the lack of a practical definition, mainly due to the absence of relations between local and global timing effects. We address these relations through the causality, which we further use to revise the formalization of these TAs. We also propose a specialized instance of the notions for out-of-order pipelines. We evaluate our subsequent detection procedure on illustrative examples and standard benchmarks, showing that it allows accurately capturing TAs.The complexity of the systems demands that their timing analyses be able to cope with the large resulting state space. A solution is to perform compositional analyses, specifically threatened by amplification TAs. We advance their study by showing how a specialized abstraction can be adapted for an industrial processor, by modeling the timing-relevant features of such a hardware with appropriate reductions. We also illustrate from this class of TAs how verification strategies can be used towards the obtainment of TA patterns., Les systèmes temps-réel sont souvent validés par des analyses temporelles, qui sont mises en péril par des anomalies temporelles (AT). Une AT contre-intuitive a lieu quand une accélération locale conduit à un ralentissement global, et une AT d'amplification, quand un ralentissement local entraîne un ralentissement encore plus grand.Alors que les AT contre-intuitives menacent le bien-fondé ou la flexibilité des analyses, il n'existe pas d'outils pour les détecter de manière systématique. Nous proposons une structure formelle unifiée pour évaluer les définitions des AT, concluant au manque d'une définition pratique, principalement dû à l'absence de relations entre les effets temporels locaux et globaux. Nous y répondons par la causalité, que nous utilisons pour revoir la formalisation de ces AT. Nous proposons aussi une instance des notions spécialisée pour les pipelines out-of-order. Nous évaluons notre procédure de détection subséquente sur des exemples illustratifs et bancs de tests, montrant qu'elle permet de capturer précisément les AT.La complexité des systèmes exige que leurs analyses gèrent l'important espace d'états résultant. Une solution est de réaliser des analyses compositionnelles, précisément menacées par les AT d'amplification. Nous faisons progresser leur étude en montrant comment une abstraction spécialisée peut être adaptée pour un processeur industriel, en modélisant les caractéristiques temporelles clés avec des réductions appropriées. Nous illustrons aussi à partir de cette classe d'AT comment des stratégies de vérification peuvent être utilisées en vue de l'obtention de motifs d'AT.

A Finite Discrete-time Dynamical System (DDS) consists of a finite set X , called state space, and a function f, called next-state map (which associates to a state v the state f(v)). DDS are a formal tool for modelling phenomena that appear in Physics, Mathematics, Biology, and, of course, in Computer Science. While the mathematical formalisation and the results that have been found up to nowadays are elegant and meaningful, often they are not very suitable in practice because of their high computational cost. In the literature, it is known that DDS equipped with appropriate sum and product operations form a commutative semiring. This algebraic structure allows us to write polynomial equations in which the coefficients and unknowns are DDS. In particular, if we are interested in some dynamics derived from experimental data, we can write an equation with this as a constant right-hand term and model assumptions about the function f (or its properties) in a polynomial left-hand term. Finding solutions to this equation allow us to better understand the phenomenon and its properties. This approach is interesting but it has important limitations from a computational point of view. Solving a polynomial equation (with several variables) is, in general, undecidable, and even if we focus on the case of hypothesis validation, the computational cost remains high. The idea is then to look for approximations that give relevant information about the solutions of the original equation. It is possible to introduce three abstractions (simpler equations) to identify: the number of states of the variables, the asymptotic behaviour, or the transient behaviour (what happens before the system stabilises). Each one is built from a theoretical and algorithmic point of view to introduce a method to perform hypothesis validation on DDS. In this thesis, it is shown that through algebraic transformations, it is possible to enumerate the solutions of a polynomial equation with a constant term by enumerating a finite number of simpler equations. Finally, the connection between the solution of these simple equations and the cancellation problem known in graph theory is explored. This allowed us to find a linear upper bound on the number of solutions., Un Système Dynamique Fini à temps Discret (SDD) est constitué d'un ensemble fini X, dit espace des états, et d'une fonction f, dite fonction de mise à jour (associant à un état v l'état f(v)). Les SDD sont un outil formel pour modéliser de nombreux phénomènes en physique, en mathématique, en biologie, et, bien sûr en informatique. Si la formalisation mathématique et les résultats qui en découlent sont élégants et parlants, souvent, ces résultats sont peu applicables en pratique à cause de leur coût computationnel élevé. Dans la littérature, il est connu que les SDD équipés d'opérations de somme et de produit appropriées forment un semi-anneau commutatif. Cette structure algébrique nous permet d'écrire des équations polynomiales dans lesquelles les coefficients et les inconnues sont des SDD. En particulier, si nous sommes intéressés par une certaine dynamique dérivée de données expérimentales, nous pouvons écrire une équation avec celle-ci comme terme de droite constant et modéliser des hypothèses sur la fonction f (ou ses propriétés) dans un terme de gauche polynomial. Trouver des solutions à cette équation permet de mieux comprendre le phénomène et ses propriétés. Cette approche est intéressante mais pose des limites computationnelles importantes. En effet, résoudre une équation polynomiale (à plusieurs variables) est, en général, indécidable et même en se concentrant sur le cas de la validation des hypothèses, le coût computationnel reste élevé. L'idée est alors de chercher des approximations donnant des informations pertinentes sur les solutions de l'équation originale. Trois abstractions (équations plus simples) sont introduites afin d'identifier : le nombre d'états des variables, le comportement asymptotique ou le comportement transient (comportement avant que le système se stabilise). Chaque abstraction est construite d'un point de vue théorique et algorithmique dans le but d'introduire une méthode pour effectuer la validation d'hypothèses sur SDD. Dans cette thèse, il est montré qu'au moyen de transformations algébriques, il est possible d'énumérer les solutions d'une équation polynomiale avec un terme droit constant par l'énumération d'un nombre fini d'équations plus simples. Enfin, le lien entre la résolution ces équations simples et le problème de la cancellation connu en théorie des graphes est exploré. Cela a permis de trouver une borne supérieure linéaire sur le nombre de solutions.

Our society is increasingly dependent on computer systems. Ensuring their security is essential to avoid the dramatic consequences of attacks against these systems. In this thesis, we focus on a class of attacks called timing sidechannel attacks. We study existing protections against these attacks, such as the constant-time and the constant-resource policies, and focus on their interaction with compilation. Compilation is the process of transforming a program written by a human in a source language, into machine code executable by a computer. Our goal is to ensure that compilation does not introduce any vulnerability in the compiled code, with respect to the security policies we focus on; this is called secure compilation. Our work also relies on formal methods to give formal guarantees on the results we present. One of our contribution relies on the formally verified CompCert compiler. All the results presented in this thesis are mechanically verified using the Coq proof assistant.; Notre société est de plus en plus dépendante des systèmes informatiques. Assurer leur sécurité est essentiel pour éviter les conséquences dramatiques des attaques contre ces systèmes. Dans cette thèse, nous nous concentrons sur une classe d’attaques appelée attaques par canaux cachés temporels. Nous étudions les protections existantes contre ces attaques, telles que les politiques constant-time et constant-resource, et nous nous concentrons sur leur interaction avec la compilation. La compilation est le processus de transformation d’un programme écrit par un humain dans un langage source, en code machine exécutable par un ordinateur. Notre objectif est de s’assurer que la compilation n’introduit aucune vulnérabilité dans le code compilé, par rapport aux politiques de sécurité auxquelles nous nous intéressons ; c’est ce qu’on appelle la compilation sécurisée. Notre travail s’appuie également sur des méthodes formelles pour donner des garanties formelles sur les résultats que nous présentons. Une de nos contributions s’appuie sur le compilateur formellement vérifié CompCert. Tous les résultats présentés dans cette thèse sont également vérifiés mécaniquement en utilisant l’assistant de preuve Coq.

The increasing complexity of embedded systems renders software verification more complex, requiring monitoring and formal techniques, like model-checking. However, to use such techniques, system engineers usually need formal expertise to express the software requirements in a formal language. To facilitate the use of model-checking tools by system engineers, our approach uses a UML model interpreter through which the software requirements can directly be expressed in UML as well. Formal requirements are encoded as UML state machines with the transition guards written in a specific observation language, which expresses predicates on the execution of the system model. Each such executable UML specification can model either a Buchi automaton or an observer automaton, and is synchronously composed with the system, to follow its execution during model-checking. Formal verification can continue at runtime for all deterministic observer automata used during offline verification by deploying them on real embedded systems. Our approach has been evaluated on multiple case studies and is illustrated, in this paper, through the user interface model of a cruise-control system. The automata-based verification results are in line with the verification of the equivalent LTL properties. The runtime overhead during monitoring is proportional to the number of monitors.

Formal methods provide systematic and rigorous techniques for software development. We strongly believe that they must be taught in computer science curricula. In this paper we present the pedagogic rationale and the concrete implementation of two courses on the use of formal methods, sharing some material. These courses promote the usage of formal verification to ensure safety and security of software, exemplified in the domain of the Internet of Things., Comment: In Proceedings AppFM 2021, arXiv:2111.07538

International audience; Complex systems and systems of systems (SoS) are systems characterized by the interconnection of a large number of components or subsystems. The complexity of such systems increases with the number of components and their manner of connectivity. The global behaviour of complex systems and SoS exhibits some properties that cannot be predicted by analysing components or subsystems in isolation. The verification of these properties called "emergent properties" is considered a crucial issue when engineering such systems. The purpose of this paper is to give an overview and verify emergent properties. In a first step, we have taken the blinker and the traffic light of the game of life as examples to verify emergence by using refinement techniques; in a second step, since the refinement is not straightforward, we have taken another example, the Boids model, and by using timed automata and UPPAAL model checking techniques, we have been able to simulate and verify emergent properties. Povzetek: Prispevek podaja pregled emergentnih lastnosti v kompleksnih sistemih.

The development of critical systems requires the definition of a rigorous design approach enabling to check these systems before a real operation. This paper presents a component-based approach that combines UML and BIP languages for the specification and formal verification of systems. We begin by modeling the system architecture and behavior using UML. The UML models are then translated into a formal specification expressed in BIP. Finally, the SBIP framework is used for verifying the correctness of the system using Statistical Model Checking while satisfying requirements expressed by temporal properties. We apply our approach to a dam infrastructure, represented by a set of deployed sensors.

In this work we briefly summarize our recent contributions in the field of proof methods, theorem proving and countermodel generation for non-normal modal logics. We first recall some labelled sequent calculi for the basic system E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. Then, we present PRONOM, a theorem prover and countermodel generator for non-normal modal logics implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof in the labelled calculi, otherwise it is able to extract a model falsifying it from an open, saturated branch. © 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).

This document provides a formal definition of the modelling language HLL - High Level Language. HLL is a declarative stream-based language supporting a large variety of types and operators. It is suitable for modelling discrete-time sequential behaviors and expressing temporal properties of these behaviors. In 2018 the HLL Forum initiative started as a working group of tool providers and users of HLL. New features of HLL (compared to version 2.7) were developed jointly by the HLL Forum. This document is a prerelease (proposal) by Systerel to HLL Forum of an upcoming version 4.0.

International audience; LINGUA FRANCA (LF) is a polyglot coordination language designed for the composition of concurrent, timesensitive, and potentially distributed reactive components called reactors. The LF coordination layer facilitates the use of target languages (e.g., C, C++, Python, TypeScript) to realize the program logic, where each target language requires a separate runtime implementation that must correctly implement the reactor semantics. Verifying the correctness of runtime implementations is not a trivial task, and is currently done on the basis of regression testing. To provide a more formal verification tool for existing and future target runtimes, as well as to help verify properties of LF programs, we recruit the use of GEMOC Studio-an Eclipse-based workbench for the development, integration, and use of heterogeneous executable modeling languages. We present an operational model for LF, realized in GEMOC Studio, that is primed to interact with a rich set of analysis and verification tools. Our instrumentation provides the ability to navigate the execution of LF programs using an omniscient debugger with graphical model animation; to check assertions in particular execution runs, or exhaustively, using a model checker; and to validate or debug traces obtained from arbitrary LF runtime environments.

International audience; To respond to users’ demands, organizations’ in-formation systems are put into action consuming resources of different types. However, it happens that resources are poorly defined raising concerns about their availabilities at run-time. To ensure the correct definition of resources, this paper presents an approach to formally model and verify them using model-checking. First, properties referred to as limited, limited-but-renewable, and non-shareable are assigned to resources allowing to develop their consumption cycles. Afterwards, we model property-based resource consumption cycles as state diagrams and then, convert them into timed automata in preparation for their formal verification. After this conversion, specific CTL formulae are associated with each resource property. A case study illustrates how some cloud resources are defined as limited, shared, and even shared temporarily. These resources are modeled as timed automata and the conformity of their respective behaviors with respect to resource properties is verified.

International audience; A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of every component of the tool-chain. In order to contribute to the end-to-end verification of compilers, we implemented a verified lexer generator with usage similar to OCamllex. This software-Coqlex-reads a lexer specification and generates a lexer equipped with Coq proofs of its correctness. Although the performance of the generated lexers does not measure up to the performance of a standard lexer generator such as OCamllex, the safety guarantees it comes with make it an interesting alternative to use when implementing totally verified compilers or other language processing tools.

International audience; We introduce the W-calculus, an extension of the call-byvalue λ-calculus with synchronous semantics, designed to be flexible enough to capture different implementation forms of Digital Signal Processing algorithms, while permitting a direct embedding into the Coq proof assistant for mechanized formal verification. In particular, we are interested in the different implementations of classical DSP algorithms such as audio filters and resonators, and their associated high-level properties such as Linear Time-invariance. We describe the syntax and denotational semantics of the W-calculus, providing a Coq implementation. As a first application of the mechanized semantics, we prove that every program expressed in a restricted syntactic subset of W is linear time-invariant, by means of a characterization of the property using logical relations. This first semantics, while convenient for mechanized reasoning, is still not useful in practice as it requires re-computation of previous steps. To improve on that, we develop an imperative version of the semantics that avoids recomputation of prior stream states. We empirically evaluate the performance of the imperative semantics using a staged interpreter written in OCaml, which, for an input program in W , produces a specialized OCaml program, which is then fed to the optimizing OCaml compiler. The approach provides a convenient path from the high-level semantical description to low-level efficient code. Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.

This document provides a formal definition of the modelling language HLL - High Level Language. HLL is a declarative stream-based language supporting a large variety of types and operators. It is suitable for modelling discrete-time sequential behaviors and expressing temporalproperties of these behaviors.In 2018 the HLL Forum initiative started as a working group of tool providers and users of HLL. New features of HLL (compared to version 2.7) were developed jointly by the HLL Forum. This document is a prerelease (proposal) by Prover to HLL Forum of an upcoming version 4.0.

Software programs are used for many critical roles. A bug in those can have a devastating cost, possibly leading to the loss of human lives. Such bugs are usually found at the source level (which can be ruled out with source-level verification methods), but they can also be inserted by the compiler unknowingly. CompCert is the first commercially available optimizing compiler with a formal proof of correctness: compiled programs are proven to behave the same as their source programs. However, because of the challenges involved in proving compiler optimizations, CompCert only has a limited number of them. As such, CompCert usually generates low-performance code compared to classical compilers such as GCC. While this may not significantly impact out-of-order architectures such as x86, on in-order architectures, particularly on VLIW processors, the slowness is significant (code running half as fast as GCC -O2). On VLIW processors, the intra-level parallelism is explicit and specified in the assembly code through “bundles” of instructions: the compiler must bundlize instructions to achieve good performance.In this thesis, we identify, investigate, implement and formally verify several classical optimizations missing in CompCert. We start by introducing a formal model for VLIW bundles executing on an interlocked core and generate those bundles through a postpass (after register allocation) scheduling. Then, we introduce a prepass (before register allocation) superblock scheduling, implementing static branch prediction and tail-duplication along the way. Finally, we further increase the performance of our generated code by implementing loop unrolling, loop rotation and loop peeling – the latter being used for Loop-Invariant Code Motion. These transformations are verified by translation validation, some of them with hash-consing to achieve reasonable compilation time.We evaluate each introduced optimization on benchmarks, including Polybench and TACleBench, on the KV3 VLIW core, ARM Cortex A53, and RISC-V “Rocket” core. Thanks to this work, our version of CompCert is now only 16% slower (respectively 12% slower and 30% slower) thanGCC -O2 on the KV3 (respectively ARM and RISC-V), instead of 50% (respectively 38% and 45%).; On utilise des logiciels pour différents rôles, parfois critiques. La présence d’un bogue dans un logiciel peut avoir un coût dévastateur, pouvant aller jusqu’à la perte de vies humaines dans les cas les plus extrêmes. Les bogues viennent en général du code source (ceux-là peuvent être détectés par des méthodes de vérification formelle sur le langage source), mais ils peuvent être également générés par le compilateur. CompCert est le premier compilateur optimisant commercialisé comportant une preuve formelle de correction : il est formellement prouvé que les programmes compilés avec cet outil ont le même comportement que leurs programmes sources originels. Cependant, comme prouver les optimisations d’un compilateur relève d’un défi considérable, CompCert n’en a qu’un nombre limité. Ainsi, en général CompCert génère du code moins performant comparé à d’autres compilateurs classiques tels que GCC. Bien que cela n’impacte peu les architectures à exécution dans le désordre telles que x86, sur des architectures à exécution dans l’ordre, et en particulier sur des processeurs VLIW, le ralentissement estimportant (le code résultant est deux fois plus lent que GCC -O2). Sur un processeur VLIW , le parallélisme d’instructions est explicite et spécifié dans le code assembleur par des bundles (paquets) d’instructions : le compilateur doit paquétiser les instructions pour obtenir une bonne performance.Le but de cette thèse est d’identifier, d’enquêter, d’implémenter et de vérifier formellement plusieurs optimisations classiques manquantes dans CompCert. Tout d’abord, j’introduis un model formel d’exécution de bundles VLIW sur processeur à pipeline imbriqué. Nous générons ces bundles à partir d’un réordonnancement en postpass (après allocation de registres). Ensuite, j’introduis un réordonnancement de superblocks en prepass (avant allocation de registres). Ce travail implique aussi l’introduction d’une prédiction statique de branchements, et une duplication de queue. Enfin, pour continuer d’augmenter la performance du code généré, j’introduis du déroulage, rotation, et pelage de boucles – ce dernier étant utilisé dans du déplacement d’invariants de boucles. Ces transformations sont vérifiées par validation de translation, et certaines utilisent du partage maximal afin d’obtenir des temps de compilation raisonnables.Nous avons évalué chacune de ces optimisations sur des tests de performance, dont Polybench et TACLeBench, sur le coeur VLIW KV3, l’ARM Cortex A53, et le coeur RISC-V “Rocket”. Grâce à nos travaux, notre version de CompCert est maintenant seulement 16% plus lente (respectivement 12% et 30% plus lente) que GCC -O2 sur KV3 (respectivement ARM et RISC-V), au lieu de 50% (respectivement 38% et 45%).

International audience; Smart contracts are the artifact of the blockchain that provides immutable and verifiable specifications of physical transactions. Solidity is a domain-specific programming language with the purpose of defining smart contracts. It aims at reducing the transaction costs occasioned by the execution of contracts on the distributed ledgers such as Ethereum. However, Solidity contracts need to adhere to safety and security requirements that require formal verification and certification. This paper proposes a method to meet such requirements by translating Solidity contracts to Event-B models, supporting certification. To that purpose, we define a restrained Solidity subset and a transfer function that translates Solidity contracts to Event-B models. Besides, we have implemented a translator to improve the conversion efficiency. As a case study, we take advantage of Event-B method capabilities to simulate models at different levels of abstraction and to express the properties of a typical smart contract: Honeypot contract. Lastly, we verify the generated proof obligations of the Event-B model with the help of the Rodin platform.

Designing distributed applications involves a fundamental trade-off between safety and performance as described by CAP theorem. We focus on the cases where safety is the top requirement.For the subclass of state-based distributed systems, we propose a proof methodology for establishing that a given application maintains a given invariant. Our approach allows reasoning about individual operations separately. We demonstrate that our rules are sound, and with a mechanized proof engine, we illustrate their use with some representative examples. For conflicting operations, the developer can choose between conflict resolution or coordination. We present a novel replicated tree data structure that supports coordination-free concurrent atomic moves, and arguably maintains the tree invariant. Our analysis identifies cases where concurrent moves are inherently safe. For the remaining cases we devise a conflict resolution algorithm. The trade-off is that in some cases a move operation "loses". Given the coordination required by some application for safety, it can be implemented in many different ways. Even restricting to locks, they can use various configurations, differing by lock granularity, type, and placement. The performance of each configuration depends on workload. We study the "coordination lattice", i.e., design space of lock configurations, and define a set of metrics to systematically navigate them., La conception d'applications distribuées implique fondamentalement un compromis entre la sûreté et les performances. Nous nous concentrons sur les cas où la sûreté est la principale exigence. Dans le cadre des systèmes distribués basés sur l'état, nous proposons une méthodologie de preuve pour établir qu'une application donnée maintient un invariant donné. Notre approche permet de raisonner sur les opérations individuelles séparément. Nous démontrons que nos règles sont correctes et, à l'aide d'un moteur de preuve, nous illustrons leur utilisation par quelques exemples représentatifs. Pour les opérations conflictuelles, le développeur peut choisir entre la résolution de conflit ou la coordination. Nous présentons une nouvelle structure de données en forme d'arbre répliqué qui prend en charge les déplacements atomiques concurrents sans coordination et qui maintient l'invariant de l'arbre. Notre analyse identifie les cas où les déplacements concurrents sont intrinsèquement sûrs. Pour les autres cas, nous concevons un algorithme de résolution des conflits. La contrepartie est que dans certains cas, une opération de déplacement est "perdante". Étant donné la coordination requise par certaines applications pour la sûreté, elle peut être implémentée de nombreuses façons différentes. Même en se limitant aux verrous, ceux-ci peuvent utiliser diverses configurations qui diffèrent par: la granularité, le type et le placement. La performance de chaque configuration dépend de la charge de travail. Nous étudions le "treillis de coordination", l'espace de conception des configurations de verrouillage, et définissons un ensemble de mesures pour y naviguer systématiquement.

International audience; We investigate three particular instances of the marking coverability problem in ordinary, safe Petri nets: the Dead Places Problem, the Dead Transitions Problem, and the Concurrent Places Problem. To address these three problems, which are of practical interest, although not yet supported by mainstream Petri net tools, we propose a combination of static and dynamic algorithms. We implemented these algorithms and applied them to a large collection of 13,000+ Petri nets obtained from realistic systems-including all the safe benchmarks of the Model Checking Contest. Experimental results show that 95% of the problems can be solved in a few minutes using the proposed approaches.

The growing risk of privacy violation and espionage associated with the rapid spread of mobile communications renewed interest in the original concept of sending encrypted voice as audio signal over arbitrary voice channels. The usual methods used for encrypted data transmission over analog telephony turned out to be inadequate for modern vocal links (cellular networks, VoIP) equipped with voice compression, voice activity detection, and adaptive noise suppression algorithms. The limited available bandwidth, nonlinear channel distortion, and signal fadings motivate the investigation of a dedicated, joint approach for speech encodingand encryption adapted to modern noisy voice channels.This thesis aims to develop, analyze, and validate secure and efficient schemes for real-time speech encryption and transmission via modern voice channels. In addition to speech encryption, this study covers the security and operational aspects of the whole voice communication system, as this is relevant from an industrial perspective.The thesis introduces a joint speech encryption scheme with lossy encoding, which randomly scrambles the vocal parameters of some speech representation (loudness, pitch, timbre) and outputs an encrypted pseudo-voice signal robust against channel noise. The enciphering technique is based on random translations and random rotations using lattices and spherical codes on flat tori. Against transmission errors, the scheme decrypts the vocal parameters approximately and reconstructs a perceptually analogous speech signal with the help of a trained neural-based voice synthesizer. The experimental setup was validated by sending encrypted pseudo-voice over a real voice channel, and the decrypted speech was tested using subjective quality assessment by a group of about 40 participants.Furthermore, the thesis describes a new technique for sending data over voice channels that relies on short harmonic waveforms representing quaternary codewords. This technique achieves a variable bitrate up to 6.4 kbps and has been successfully tested over various real voice channels. Finally, the work considers a dedicated cryptographic key exchange protocol over voice channels authenticated by signatures and a vocal verification. The protocol security has been verified in a symbolic model using Tamarin Prover.The study concludes that secure voice communication over real digital voice channels is technically viable when the voice channels used for communication are stable and introduce distortion in a predictable manner.stabintroduce distortion in a predictable manner.; Les risques croissants de violation de la vie privée et d’espionnage associés à la forte croissance des communications mobiles ont ravivé l’intérêt du concept originel de chiffrement de la parole sous forme de signaux audio transmis sur des canaux vocaux non spécifiques. Les méthodes habituelles utilisées pour la transmission de données cryptées par téléphonie analogique se sont révélées inadaptées pour les communications vocales modernes (réseaux cellulaires, VoIP) avec leurs algorithmes de compression de la voix, de détection d’activité vocale et de suppression adaptative du bruit. La faible bande passante disponible, les distorsions non linéaires des canaux et les phénomènes d’évanouissements du signal motivent l’introduction d’une approche conjointe du codage et du chiffrement de la parole adaptée aux canaux vocauxbruités modernes.Dans cette thèse sont développés, analysés et validés divers schémas sûrs et efficaces pour le chiffrement et la transmission de la parole en temps réel pour les canaux vocaux modernes. En plus du chiffrement de la parole, cette étude couvre les aspects sécurité et algorithmique de l’ensemble du système de communication vocale - aspects critiques d’un point de vue industriel. La thèse détaille un système de chiffrement de la parole associé à un codage avec perte, par brouillage aléatoire des paramètres vocaux (volume, hauteur, timbre) de certaines représentations de la parole. En résulte un pseudo-signal vocal chiffré robuste aux erreurs ajoutées par les canaux de transmission modernes. La technique de chiffrement repose sur l’introduction de translations et rotations aléatoires sur des maillages de tores plats associés à des codes sphériques. Face aux erreurs de transmission, le schéma déchiffre approximativement les paramètres vocaux et reconstruit, grâce à un synthétiseur vocal utilisant un réseau de neurones par apprentissage, un signal de parole perceptuellement très proche du signal d’origine. Le dispositif expérimental a été validé par la transmission de signaux de type pseudo-voix chiffrés sur un canal vocal réel. Les signaux de parole déchiffrés ont été favorablement notés lors d’une évaluation subjective de qualité incluant environ 40 participants.La thèse décrit également une nouvelle technique de transmission de données sur canaux vocaux en utilisant un dictionnaire d’ondes harmoniques courtes représentant les mots d’un code quaternaire. La technique fournit un débit binaire variable allant jusqu’à 6.4 kbps et a été testée avec succès sur différents canaux vocaux réels. Enfin, est présenté aussi un protocole d’échange de clés cryptographiques dédié pour les canaux vocaux authentifiés par signatures et vérification vocale. La sécurité du protocole a été vérifiée sous forme d’un modèle symbolique par l’assistant de preuve formelle Tamarin.L’étude conclut qu’une communication vocale sécurisée sur des canaux vocaux numériques réels est techniquement et de fait viable lorsque les canaux vocaux utilisés pour la communication sont stables et ne présentent que des distorsions prévisibles.

International audience; Software-Defined Network (SDN) technology provides the possibility to turn the network infrastructure into a dynamic programmable fabric capable of meeting the application needs in real-time. Thanks to the independence of the control plane from the data plane, the control entity, generally called as controller, has also the flexibility to implement proprietary complex algorithms. Within such a dynamic and complex environment, this document advocates for applying formal verification methods and more precisely composition model checking to ensure the correct behavior of the overall SDN system at design phase. To illustrate this purpose, it proposes to build different comprehensive formal models of a typical SDN platform selected here as a study object. Thorough performance results related to each model are provided and discussed. Thanks to such formal verifications, it is possible to pinpoint issues such as the one regarding network isolation within a complex SDN architecture. Although dealing with formal methods, this document attempts to strike a balance between theory, experimental work and network architecture discussion.

The tree is an essential data structure in many applications. In a distributed application, such as a distributed file system, the tree is replicated.To improve performance and availability, different clients should be able to update their replicas concurrently and without coordination. Such concurrent updates converge if the effects commute, but nonetheless, concurrent moves can lead to incorrect states and even data loss. Such a severe issue cannot be ignored; ultimately, only one of the conflicting moves may be allowed to take effect. However, as it is rare, a solution should be lightweight. Previous approaches would require preventative cross-replica coordination, or totally order move operations after-the-fact, requiring roll-back and compensation operations. In this paper, we present a novel replicated tree that supports coordination-free concurrent atomic moves, and provably maintains the tree invariant. Our analysis identifies cases where concurrent moves are inherently safe, and we devise a lightweight, coordination-free, rollback-free algorithm for the remaining cases, such that a maximal safe subset of moves takes effect. We present a detailed analysis of the concurrency issues with trees, justifying our replicated tree data structure. We provide mechanized proof that the data structure is convergent and maintains the tree invariant. Finally, we compare the response time and availability of our design against the literature.; L’arbre est une structure de données essentielle. Quand l’application est distribuée, par exemple dans un système de fichiers distribué, l’arbre est répliqué. Pour améliorer les performances et la disponibilité, les différents clients doivent pouvoir mettre à jour leurs répliques simultanément et sans coordination. Celles-ci convergent si les mises à jour commutent entre elles ; néanmoins, même dans ce cas, des opérations “move” concurrentes peuvent conduire à des états incorrects, et même à la perte de données. Au bout du compte, entre deux opérations “move” en conflit, seule l’une des deux peut être autorisée à prendre effet. Cependant, comme ce cas est rare, la solution doit être légère. Les approches précédentes nécessitaient une coordination préventive des répliques, ou des retours en arrière a posteriori. Dans cet article, nous présentons un nouvel arbre répliqué, qui met en œuvre une opération “move” atomique sans coordination, et dont nous prouvons qu’il maintient l’invariant d’arbre.Notre analyse identifie les cas où les “move” concurrents sont intrinsèquement sûrs, et proposons un algorithme léger, sans coordination et sans retour-arrière, pour les autres cas, de sorte qu’un sous-ensemble maximal et sûr de “move” prenne effet. Nous présentons une analyse détaillée des problèmes de cohérence dans les arbres. Nous fournissons une preuve mécanisée que la structure des données est convergente et maintientl’invariant d’arbre. Enfin, nous comparons le temps de réponse et la disponibilité de notre concept à la littérature.

The tree is an essential data structure in many applications. In a distributed application, such as a distributed file system, the tree is replicated.To improve performance and availability, different clients should be able to update their replicas concurrently and without coordination. Such concurrent updates converge if the effects commute, but nonetheless, concurrent moves can lead to incorrect states and even data loss. Such a severe issue cannot be ignored; ultimately, only one of the conflicting moves may be allowed to take effect. However, as it is rare, a solution should be lightweight. Previous approaches would require preventative cross-replica coordination, or totally order move operations after-the-fact, requiring roll-back and compensation operations. In this paper, we present a novel replicated tree that supports coordination-free concurrent atomic moves, and provably maintains the tree invariant. Our analysis identifies cases where concurrent moves are inherently safe, and we devise a lightweight, coordination-free, rollback-free algorithm for the remaining cases, such that a maximal safe subset of moves takes effect. We present a detailed analysis of the concurrency issues with trees, justifying our replicated tree data structure. We provide mechanized proof that the data structure is convergent and maintains the tree invariant. Finally, we compare the response time and availability of our design against the literature.; L’arbre est une structure de données essentielle. Quand l’application est distribuée, par exemple dans un système de fichiers distribué, l’arbre est répliqué. Pour améliorer les performances et la disponibilité, les différents clients doivent pouvoir mettre à jour leurs répliques simultanément et sans coordination. Celles-ci convergent si les mises à jour commutent entre elles ; néanmoins, même dans ce cas, des opérations “move” concurrentes peuvent conduire à des états incorrects, et même à la perte de données. Au bout du compte, entre deux opérations “move” en conflit, seule l’une des deux peut être autorisée à prendre effet. Cependant, comme ce cas est rare, la solution doit être légère. Les approches précédentes nécessitaient une coordination préventive des répliques, ou des retours en arrière a posteriori. Dans cet article, nous présentons un nouvel arbre répliqué, qui met en œuvre une opération “move” atomique sans coordination, et dont nous prouvons qu’il maintient l’invariant d’arbre.Notre analyse identifie les cas où les “move” concurrents sont intrinsèquement sûrs, et proposons un algorithme léger, sans coordination et sans retour-arrière, pour les autres cas, de sorte qu’un sous-ensemble maximal et sûr de “move” prenne effet. Nous présentons une analyse détaillée des problèmes de cohérence dans les arbres. Nous fournissons une preuve mécanisée que la structure des données est convergente et maintientl’invariant d’arbre. Enfin, nous comparons le temps de réponse et la disponibilité de notre concept à la littérature.

Many applications, notably in the context of verification (for critical systems in transportation, energy, etc.), rely on checking the satisfiability of logic formulas. Satisfiability-modulo-theories (SMT) solvers handle large formulas in expressive languages with built-in and custom operators (e.g. arithmetic and data structure operators). These tools are built using a cooperation of a SAT (propositional satisfiability) solver to handle the Boolean structure of the formula and theory reasoners to tackle the atomic formulas (e.g. « x > y+z » for the theory of arithmetic). Currently, SMT solvers only handle first-order logic. They cannot reason about higher-order expressions, and they generally cannot perform proofs by induction. This is unfortunate, because most interactive verification tools, which use SMT solvers as back-end reasoning engines, offer higher-order languages. This thesis offers solutions to improve interactions between automatic solvers and proof assistants. In particular, we answer two important issues allowing us to improve the use of SMT solvers within proof assistants. Our first contribution consists in providing a suitable architecture to SMT solvers for higher-order logic. The second contribution aims to improve quantifier reasoning inside SMT solvers. For both approaches, we developed a practical implementation and provide a concrete evaluation on a large collection of problems mostly coming from formalization problems. The results obtained during these evaluations are encouraging and show that the developed techniques can provide good improvements for SMT solvers.Many applications, notably in the context of verification (for critical systems in transportation, energy, etc.), rely on checking the satisfiability of logic formulas. Satisfiability-modulo-theories (SMT) solvers handle large formulas in expressive languages with built-in and custom operators (e.g. arithmetic and data structure operators). These tools are built using a cooperation of a SAT (propositional satisfiability) solver to handle the Boolean structure of the formula and theory reasoners to tackle the atomic formulas (e.g. « x > y+z » for the theory of arithmetic). Currently, SMT solvers only handle first-order logic. They cannot reason about higher-order expressions, and they generally cannot perform proofs by induction. This is unfortunate, because most interactive verification tools, which use SMT solvers as back-end reasoning engines, offer higher-order languages. This thesis offers solutions to improve interactions between automatic solvers and proof assistants. In particular, we answer two important issues allowing us to improve the use of SMT solvers within proof assistants. Our first contribution consists in providing a suitable architecture to SMT solvers for higher-order logic. The second contribution aims to improve quantifier reasoning inside SMT solvers. For both approaches, we developed a practical implementation and provide a concrete evaluation on a large collection of problems mostly coming from formalization problems. The results obtained during these evaluations are encouraging and show that the developed techniques can provide good improvements for SMT solvers., La vérification formelle de programmes informatiques ou de systèmes dits critiques tels que dans le transport, l'énergie, etc, est essentielle pour garantir le bon fonctionnement de ces systèmes. Les méthodes de vérification employées s'appuient très fortement sur des procédés mathématiques et logiques permettant de raisonner de manière formelle sur le comportement de ces systèmes. Ces procédés définissent généralement les comportements sous forme de grands ensembles de contraintes logiques. L'approche par satisfaisabilité est une méthode largement utilisée pour vérifier ces contraintes et est un exemple de cas, où les solveurs SMT (satisfaisabilité modulo théories) sont fortement sollicités. Généralement, les solveurs SMT ne gèrent que la logique de premier ordre. Ils ne peuvent pas raisonner sur des expressions d'ordre supérieur, et ils ne peuvent généralement pas effectuer de preuves par induction. C'est regrettable, car la plupart des outils de vérification interactifs, qui utilisent les solveurs SMT, utilisent des langages d'ordre supérieur. L'objectif de cette thèse dans sa globalité est d'offrir des solutions pour améliorer les interactions entre solveur automatique et assistant de preuves. En particulier nous répondons à deux problématiques importantes permettant d'améliorer les usages de solveurs SMT au sein des assistants de preuves. Notre première contribution permet de réduire l'écart entre solveur et assistant de preuve en proposant une architecture adaptée pour la logique d'ordre supérieur. La seconde contribution permet d'améliorer les capacités de raisonnement des solveurs SMT pour les quantificateurs. Pour les deux approches développées nous apportons un ensemble d'évaluation sur des problèmes extraits pour la grande majorité de problèmes de formalisation. Les résultats obtenus lors de ces évaluations sont encourageants et montrent que les techniques développées dans cette thèse peuvent apporter de bonnes améliorations pour les solveurs SMT. Ce doctorat s'est effectué dans le cadre du projet ERC de J. Blanchette (Matryoshka), un ambitieux projet quinquennal qui vise à construire des prouveurs automatiques utiles pour la vérification interactive, et réduire l'écart entre les prouveurs interactifs et solveurs automatiques. L'un des objectifs concrets du projet est d'étendre les capacités de raisonnement des solveurs SMT vers l'ordre supérieur.

International audience; Model-checking intends to verify whether a property is satisfied by a model, or not. Model-checking of high-level models, e.g. SysML models, usually first requires a model transformation to a low level formal specification. The present papers proposes a new model-checker that can be applied (almost) directly to the SysML model. The paper first explains how this model-checker works. Then, we explain how it can efficiently check CTL-like properties. Finally, the paper discusses the performance of this model-checker integrated in the TTool framework.

An invaluable feature of computer algebra systems is their ability to plot the graph of functions. Unfortunately, when one is trying to design a library of mathematical functions, this feature often falls short, producing incorrect and potentially misleading plots, due to accuracy issues inherent to this use case. This paper investigates what it means for a plot to be correct and how to formally verify this property. The Coq proof assistant is then turned into a tool for plotting function graphs using reliable polynomial approximations. This feature is provided as part of the CoqInterval library., Comment: In Proceedings F-IDE 2021, arXiv:2108.02369

International audience; One of the 21st century’s hottest topics in the world of IT has been the emergence of what some predict to be the foundation stone for a new era of internet (web 3.0): Blockchain technology. Besides being the backbone of what we come to know as cryptocurrencies, Blockchain’s features make for a bottomless list of possible applications, especially thanks to the concept of smart contracts. This, however, caused Blockchain to be in the limelight of not only interested investors but also malicious users who started hunting for this technology’s vulnerabilities, which resulted in numerous attacks on different Blockchain platforms. In an attempt to mend such loopholes, researchers took an interest in the verification of smart contracts, which are at the heart of Blockchain’s applications. In this survey, we aim to present a general overview of the different axes investigated by researchers towards the verification of smart contracts, while taking a special interest in studies that focus on formal verification, the different approaches they apply and vulnerabilities they target.

International audience; The design of embedded real-time systems requires specific toolchains to guarantee time constraints and safe behavior. These tools need to be managed in a coherent way all along the design process and need to address timing constraints and execution semantic in a holistic way during the system's modeling, verification, and implementation phases. However, modeling languages used by these tools do not always share a common semantic. This can introduce a dangerous gap between what designers want to express, what is verified and the behavior of the final executable code. In order to address this problem, we propose a new toolchain, called Hippo, that integrates tools for design, verification and implementation built around a common formalism. Our formalism is based on an extension of the Fiacre specification language with runtime features, such as asynchronous function calls and synchronization with events. We formally define the behavior of these additions and describe a compiler to generate both an executable code and a verifiable model from the same highlevel specification. The execution of the resulting code is supported by a dedicated execution engine that guarantees real-time behavior and that reduces the semantic gap between high-level models and executable code. We illustrate our approach with a non trivial use case: the autonomous navigation of a Segway RMP440 robotic platform. We describe how we obtain a Hippo model from an initial specification of the system based on the robotics programming framework GenoM. We illustrate our approach by describing how the Hippo runtime is used to control this robot, but also how we can use formal verification to check critical properties on this system.

International audience; Outsourcing an increasing amount of data to a third party raises a number of security and privacy challenges, namely remote data integrity verification. Indeed, proofs for data possession checking address the verification that some previously outsourced data blocks across multiple storing nodes are correctly stored and fully available. In this paper, we propose a new set homomorphic proof of data possession, referred to as SHoPS, supporting several operations like aggregation of proofs. SHoPS is a deterministic Proof of Data Possession (PDP) scheme, based on an interactive proof protocol. Our approach has several advantages. First, it enables several proofs to be aggregated and a subset of data files' proofs to be verified, while providing an attractive communication overhead. Second, it supports public verifiability where the verification process can be delegated to another entity, thus releasing the data owner from the cumbersome task of periodical verifications. Third, SHoPS is efficient and provably secure, as it is resistant to the fraudulence of the prover and the leakage of verified data. Finally, a theoretical performances' analysis shows that SHoPS performs better in terms of functionality, communication and computation overhead compared to closely related works and experimental results point out the applicability of the proposed scheme in real world scenarios

International audience; Discrete, logic-based models are increasingly used to describe biological mechanisms. Initially introduced to study gene regulation, these models evolved to cover various molecular mechanisms, such as signaling, transcription factor cooperativity, and even metabolic processes. The abstract nature and amenability of discrete models to robust mathematical analyses make them appropriate for addressing a wide range of complex biological problems. Recent technological breakthroughs have generated a wealth of high-throughput data. Novel, literature-based representations of biological processes and emerging algorithms offer new opportunities for model construction. Here, we review up-to-date efforts to address challenging biological questions by incorporating omic data into logic-based models and discuss critical difficulties in constructing and analyzing integrative, large-scale, logicbased models of biological mechanisms.

Modern computing systems have grown in complexity, and even though system components are generally carefully designed and even verified by different groups of people, thecompositionof these components is often regarded with less attention. Inconsistencies between components’ assumptions on the rest of the system can have significant repercussions on this system, and may ultimately lead to safety or security issues. In this article, we introduce FreeSpec, a formalismbuilt upon the key idea that components can bemodeled as programs with algebraic effects to be realized by other components. FreeSpec allows for the modular modeling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition. In addition, we have implemented a framework for the Coq proof assistant based on FreeSpec.

International audience; Verifpal is a new automated modeling framework and verifier for cryptographic protocols, optimized with heuristics for common-case protocol specifications, that aims to work better for real-world practitioners, students and engineers without sacrificing comprehensive formal verification features. In order to achieve this, Verifpal introduces a new, intuitive language for modeling protocols that is easier to write and understand than the languages employed by existing tools. Its formal verification paradigm is also designed explicitly to provide protocol modeling that avoids user error. Verifpal is able to model protocols under an active attacker with unbounded sessions and fresh values, and supports queries for advanced security properties such as forward secrecy or key compromise impersonation. Furthermore, Verifpal's semantics have been formalized within the Coq theorem prover, and Verifpal models can be automatically translated into Coq as well as into ProVerif models for further verification. Verifpal has already been used to verify security properties for Signal, Scuttlebutt, TLS 1.3 as well as the first formal model for the DP-3T pandemic-tracing protocol, which we present in this work. Through Verifpal, we show that advanced verification with formalized semantics and sound logic can exist without any expense towards the convenience of real-world practitioners.

International audience; UML interactions, aka sequence diagrams, are frequently used by engineers to describe expected scenarios of good or bad behaviors of systems under design, as they provide allegedly a simple enough syntax to express a quite large variety of behaviors. This paper uses them to express formal safety requirements for safety critical systems in an incremental way, where the scenarios are progressively refined after checking the consistency of the requirements. As before, the semantics of these scenarios are expressed by transforming them into an intermediate semantic model amenable to formal verification. We rely on the Clock Constraint Specification Language (CCSL) as the intermediate semantic language. An SMT-based analysis tool called MyCCSL is used to check consistency of the sequence diagrams. We compare these requirements against actual execution traces to prove the validity of our transformation. In some sense, sequence diagrams and CCSL constraints both express a family of acceptable infinite traces that must include the behaviors given by the finite set of finite execution traces against which we validate. Finally, the whole process is illustrated on partial requirements for a railway transit system.

The increasing complexity of embedded systems renders them more vulnerable to software bugs, design errors and security flaws. Therefore, there is a growing need for verification and validation activities. To execute and analyze models of these systems, transformations are usually required to obtain (i) the executable code that can be deployed on embedded targets as well as (ii) analysismodels used to apply formal verification techniques (e.g., model-checking). However, these typically unproven transformations are responsible for semantic gaps and require to establish an equivalence relation between executable code and analysis models to ensure that what is executed is what has been verified. To unify analysis activities and embedded execution of these models, the EMI approach (= embedded model interpreter approach) relies on a controllable model interpreter that uses a unique pair (model + semantics) for all software development activities. To evaluate this approach, a UML model interpreter has been designed and applied on different case studies of embedded systems to perform multiple analysis activities (e.g., simulation, animation, debugging, model-checking, monitoring).; La complexité croissante des systèmes embarqués les expose à davantage de bogues logiciels, d’erreurs de conception et de failles de sécurité. Les besoins en vérification et en validation sont donc de plus en plus importants. Pour exécuter et analyser des modèles de ces systèmes, des transformations sont généralement nécessaires pour obtenir (i) le code exécutable pouvant être déployé sur une cible embarquée et (ii) des modèles d’analyse permettant d’appliquer des techniques de vérification formelle (p. ex. de model-checking). Cependant, ces transformations typiquement non-prouvées sont à l’origine de fossés sémantiques et nécessitent d’établir une relation d’équivalence entre le code exécutable et les modèles d’analyse afin de garantir que ce qui est exécuté est bien ce qui a été vérifié. Pour unifier les activités d’analyse et l’exécution embarquée de modèles, l’approche EMI (= embedded model interpreter) repose sur un interpréteur de modèles pilotable permettant d’utiliser un unique couple (modèle + sémantique) pour toutes les activités de développement logiciel. Pour évaluer cette approche, un interpréteur de modèles UML a été conçu et appliqué à différents cas d’études de systèmes embarqués afin de mettre en oeuvre diverses activités d’analyse (p. ex. simulation, animation, débogage, model-checking, monitoring).

Part 5: Short Contributions; International audience; Deriving tests with guaranteed fault coverage by FSM-based test methods is rather complex for systems with a large number of states. At the same time, formal verification methods allow to effectively process large transition systems; in particular, SMT solvers are widely used to solve analysis problems for finite transition systems. In this paper, we describe the known necessary and sufficient conditions of completeness of test suites derived by FSM-based test methods via the first-order logic formulas and use an SMT solver in order to check them. In addition, we suggest a new sufficient condition for test suite completeness and check the corresponding first-order logic formula via the SMT solver. The results of computer experiments with randomly generated finite state machines confirm the correctness and efficiency of a proposed approach.

International audience; In this article, we focus on the usage of MQTT (Message Queuing Telemetry Transport) within Connected Vehicles (CVs). Indeed, in the original version of MQTT protocol, the broker is responsible “only” for sending received data to subscribers; abstracting then the underlying mechanism of data exchange. However, within CVs context, subscribers (i.e., the processing infrastructure) may be overloaded with irrelevant data, in particular when the requirement is real or near real-time processing. To overcome this issue, we propose MQTT-CV; a new variant of MQTT protocol, in which the broker is able to perform local processing in order to reduce the workload at the infrastructure; i.e., filtering data before sending them. In this article, we first validate formally the correctness of MQTT-CV protocol (i.e., the three components of the proposed protocol are correctly interacting), through the use of Promela language and its system verification tool; the model checker SPIN. Secondly, using real-world data provided by our car manufacturer partner, we have conducted real implementation and experiments. The obtained results show the effectiveness of our approach in term of data workload reduction at the processing infrastructure. The mean improvement, besides the fact that it is dependent of the target application, was in general about 10 times less in comparison to native MQTT protocol.

International audience; When interactive systems allow users to interact with critical systems, they are qualified as Critical Interactive Systems, CIS for short. Their design requires the support of different activities and tasks to achieve user goals. Examples of such systems are cockpits, nuclear plant control panels, medical devices, etc. Such critical systems are very difficult to model due to the complexity of the offered interaction capabilities. %humans in the loop.%This paper presents a formal framework, F3FLUID (Formal Framework For FLUID), for designing safety-critical interactive systems. It relies on FLUID as core modelling language. FLUID enables the modelling and use of interactive systems domain concepts and supports an incremental design of such systems. Formal verification, validation and animation of the designed models are supported through different transformations of FLUID models into target formal verification techniques: %to analyse consistency by transformation for FLUID models. Event-B for formal verification, ProB model checker for animation and Interactive Cooperative Objects for user validation. The Event-B models are generated from FLUID while ICO and ProB models are produced from Event-B. We exemplify the real-life case study TCAS (Traffic alert and Collision Avoidance System) to demonstrate our framework.

To improve the design, Verification and Validation phases of Power Supply Equipment of the Electric Lines control systems at French Railway Company (SNCF for Societe nationale des chemins de fer francais), this paper proposes an integrated methodology, for automatic generation, formal verification and implementation of safe Programmable Logic Control (PLC) programs. The main objective is to save time and to improve the “overloaded” workflow of systems engineers. This methodology is compliant with the traditional engineering workflow. The first phase of the methodology focuses on the automatic generation of PLC programs, wiring diagrams, and test-based recipe books, based on reusing and adapting similar models of existing projects to the new specifications (corresponding to functional and safety requirements). The second phase is related to the application of formal verification and control synthesis techniques to guarantee the safety of the control installation. The first phase of the methodology has been successfully deployed at SNCF. The second phase is currently being evaluated.