
@phdthesis{boespflug_outils_pour_lanalyse_2023_tel-04192194,
	title = {Outils pour l'analyse de code et de contre-mesures pour l'injection de fautes multiples},
	abstract = {Les attaquants actifs sont capables d'intervenir sur le comportement du programme pendant son exécution. En particulier, les attaques par injection de fautes, qui ont émergées à l'origine en tant que méthode de test contre les fautes matérielles accidentelles, sont un vecteur d'attaque puissant dans lequel l'attaquant peut injecter des fautes pendant l'exécution à l'aide de techniques physiques telles que les faisceaux lasers ou des glitches de tension ou de fréquence. Plus récemment, des méthodes d'injection de fautes logicielles sont apparues.Cette thèse s'intéresse à l'analyse de programmes dans le contexte des attaques en fautes, et plus particulièrement en fautes multiples, qui implique que l'attaquant est capable d'effectuer des attaques combinant plusieurs fautes.Ces attaques combinées complexifient la tâche des outils d'évaluation automatique de robustesse en raison de l'explosion combinatoire des chemins d'exécution due aux fautes.Ce manuscrit présente les différentes contributions de cette thèse.En premier lieu, l'outil d'analyse de robustesse Lazart a été repris et développé au cours de cette thèse et vise à aider la recherche d'attaques dans un programme dans le contexte de fautes multiples.L'évaluation des protections contre ce type d'attaques a aussi été un sujet important de cette thèse et des contributions sont présentées pour aider au placement de contre-mesures logicielles.Enfin, les outils de placement utilisés dans la littérature se basent souvent sur une approche essais / erreurs qui n'est pas adaptée au contexte d'attaques multiples et s'intéressent rarement à montrer que les protections sont effectivement utiles. Une méthodologie d'optimisation de programmes protégés a été développée, visant à déterminer quelles portions des protections peuvent être retirées, tout en maintenant le même niveau de sécurité.},
	author = {Boespflug, E.},
	year = {2023},
	eprinttype={HAL}, eprint = {tel-04192194},
	HAL_version = {v1},
}

@phdthesis{ducousso_moving_code_analysis_2023_tel-04662172,
	title = {Moving code analysis from safety to security : attacker model},
	abstract = {Major works have delved into program analysis over the last decades, leveraging techniques such as symbolic execution, static analysis, abstract interpretation or bounded model checking, to hunt for software vulnerabilities and bugs in programs, or to prove their absence, leading to industrial adoption in some leading companies. As bugs are an attack entry point, removing them is a first step towards better software security. Yet, they are based on the standard concept of reachability and represent an attacker able to craft smart, legitimate input, through legitimate input sources of the program, exploiting corner cases in the code itself, a rather weak threat model, typically a file formatted to trigger a buffer overflow in data processing. Tools only looking for bugs and software vulnerabilities may deem a program secure while the bar remains quite low for an advanced attacker, able for example to take advantage of attack vectors such as (physical) hardware fault injections, micro-architectural attacks, software-based hardware attacks like Rowhammer, or any combination of vectors.In this thesis, our goal is to devise a technique to automatically and efficiently reason about the impact of an advanced attacker onto a program security properties.We propose adversarial reachability, a formalism extending standard reachability to reason about a program execution in the presence of an advanced attacker. As equipping the attacker with new capacities significantly increases the state space of the program under analysis, we build a new algorithm based on symbolic techniques, named adversarial symbolic execution, to address the adversarial reachability problem from the bug-finding point of view (bounded verification). Our algorithm prevents path explosion thanks to a new forkless encoding of attacker capabilities, modeled as faults. We show it correct and k-complete with respect to adversarial reachability. To improve the performance further, we design two new optimizations to reduce the number of injected faults while keeping the same attacker power: Early Detection of faultSaturation and Injection On Demand.We propose an implementation of our techniques for binary-level analysis, on top of the BINSEC framework. We systematically evaluate its performances against prior work, using a standard fault injection benchmark from physical fault attacks and smart cards. Experiments show a very significant performance gain against prior approaches, for example up to x10 and x200 times on average for 1 and 2 faults respectively - with a similar reduction in the number of adversarial paths. At most, we are x200 times faster for 1 fault and x6000 for 2. Moreover, our approach scales up to 10 faults whereas the state-of-the-art starts to timeout for 3 faults. We also show the use of our method in a number of different security scenarios such as reproducing a BellCoRe attack with one reset fault on CRT-RSA or looking for attacks on a program protected by the SecSwift countermeasure. In addition, we perform a security analysis of the well-tested WooKey bootloader and demonstrate the ability of our analysis to find attacks and evaluate countermeasures in real-life security scenarios. We were especially able to find an attack not mentioned before on a recently proposed patch, and proposed a new patch to the developers.},
	author = {Ducousso, S.},
	year = {2023},
	eprinttype={HAL}, eprint = {tel-04662172},
	HAL_version = {v1},
}

@phdthesis{gourdin_formal_validation_of_2023_tel-04648091,
	title = {Formal Validation of Intra-Procedural Transformations by Defensive Symbolic Simulation},
	abstract = {Compilers are highly complex software systems and may, therefore, contain bugs. These bugs can result in errors during the compilation process, or, much more annoyingly, in the generation of incorrect code. Bugs that subtly alter the semantics of generated programs are often very insidious and challenging to trace. In certain applications, particularly in embedded, safety-critical systems subject to stringent regulations and requirements (e.g., avionics, trains, etc.), eliminating these bugs is of paramount importance.Although most of these bugs are typically found in optimization passes, disabling optimizations is not a viable option in many applications. In fact, simply turning off optimizations is insufficient to guarantee bug-free code. Regulatory standards often necessitate the use of simple, predictable processors, heavily reliant on the compiler for performance.An alternative solution is to employ a certified compiler, mechanically proven correct in a proof assistant. Such a compiler ensures that the generated assembly code faithfully preserves the source code's semantics. CompCert belongs to this category, and stands as the first formally verified C compiler widely used in the industry. However, proving the correctness of intricate optimizations remains a challenge. This is why certified compilers, including CompCert, produce code that is significantly less performant compared to mainstream compilers like GCC or LLVM.Translation validation offers a technique where only the result of an optimization is verified, rather than proving the correctness of its implementation. The optimization algorithm, referred to as an oracle, remains untrusted. Nevertheless, its results are always subjected to validation by a proven validator designed to reject any errors.In this thesis, we delve into the concept of guided, defensive translation validation. The principle is to allow oracles to guide the validator by providing hints that reduce the search space, thereby minimizing the complexity of the validation process. Specifically, we propose a formally verified symbolic interpreter capable of validating an entire class of transformations. Our tool requests program invariants from oracles as hints to drive the symbolic simulation of both the original and optimized code. The proven simulation test defensively validates the applied optimizations, ensuring consistency with the unoptimized code.We have successfully validated several new transformations using this approach, including some that had never been formally verified before, thanks to the communication between oracles and their validator. Notably, we verify a strength-reduction optimization targeting 64-bit RISC-V architectures, which show promise in the context of safety-critical embedded systems. In addition to strength-reduction, our symbolic simulation framework also supports partial redundancy elimination, dead code elimination, code motion, scheduling, and weak software pipelining with renaming.We have integrated our validation mechanism into a fork of CompCert through the development of a new intermediate language called Block Transfer Language, BTL. Translations to and from BTL are also defensively validated, accomplished with a separate, formally verified checker capable of validating code duplication and factorization as control-flow graph morphisms. To rigorously assess the impact of our optimizations and the overhead introduced by their validation, we conducted multiple experimental measurements of both compilation time and runtime performance. Platform specific optimizations were tested on both AArch64 and RISC-V architectures. Results show a significant improvement of the runtime performance while maintaining a reasonable compilation time.In the future, this same method could potentially be applied to validate other transformations, such as the automatic insertion of security countermeasures. Our designs appear to be applicable beyond CompCert.},
	author = {Gourdin, L.},
	year = {2023},
	eprinttype={HAL}, eprint = {tel-04648091},
	HAL_version = {v1},
}

@phdthesis{mambakam_parametric_timed_formalisms_2023_tel-04395793,
	title = {Parametric timed formalisms for specification and monitoring},
	abstract = {Cyber-physical systems (CPS) consist of computer systems which control physical processes. Examples of this include medical devices, autonomous cars, and robots. Due to the complexity and heterogeneity of their components, it is not always possible to derive mathematical models for such systems and data-driven design approaches are thus a crucial alternative. This thesis is built upon extensions of two specification formalisms, Signal Temporal Logic (STL) and Timed Regular Expressions (TRE), which are expressive to describe temporal aspects of CPS behaviours and additionally suitable for monitoring and validation purposes.STL is a temporal logic that is adapted to specify properties of real-valued signals. We extend the logic with operators for counting events. These operators, for example, can be used to count Electrocardiogram (ECG) pulses. Parametric specifications (like parametric STL) over signals when assigned parameters can be viewed as producing predictors that indicate where a temporal pattern occurs. We term as Increasing Parametric Pattern Predictors (IPPP) specifications that become easy to satisfy as the parameter values increase. Given data labelled by experts, we propose a method to learn predictors by finding parameters of IPPP to match the labelled data as accurately as possible. We introduce a measure called epsilon-count to quantify prediction accuracy. For IPPP, decreasing both false positives and false negatives involves optimising opposing targets. We devise an algorithm that identifies parameters while respecting these opposing constraints. Pareto domination and binary search are the two main ideas behind efficient implementation of this algorithm.TRE extend regular expressions with timing constraints defined over duration. Monitoring using TRE specifications is termed as Timed Pattern Matching (TPM). This involves finding in the input behaviour, all time intervals where the specification is matched. Parametric Timed Pattern Matching (PTPM) can be defined over parametric versions of TRE (PTRE) in which we compute along with time intervals also the parameter values that allow the match. The semantics of PTRE slightly differ for real-valued signals and sequences of time-stamped events. We show that for these two types of semantics we get two kinds of polytopes which we term parametric zones and parametric intervals. Operations over parametric zones can be optimised by exploiting their separation in time similar to the plane-sweep algorithms used for TPM. Operations over parametric intervals can also benefit greatly from sorting and subsequent binary-search procedures. We also show how parametric identification can be performed on top of PTPM to compute all parameter values that makes the specification matches patterns labelled by experts.For both parametric temporal formulae and expressions, along with synthetic examples for reader’s understanding, we also apply our methods to analysis of ECGs and marine traffic data.},
	author = {Mambakam, A.},
	year = {2023},
	eprinttype={HAL}, eprint = {tel-04395793},
	HAL_version = {v1},
}

@phdthesis{morice_a_high_level_2022_tel-04076218,
	title = {A High Level Model Based on Hardware Dependencies for The Development of Embedded Software on Microcontrollers},
	abstract = {This thesis focuses on the development of embedded software on microcontrollers. The increasing complexity of these circuits makes the development more challenging. Many tasks must now be driven by the software, such as the management of clocks and power supply of different parts of the circuit. Microcontrollers are highly configurable, which allows fine-tuning of power consumption. In addition, microcontrollers include numerous and varied blocks dedicated to a specific task, and therefore very efficient for this task. The use of these blocks allows optimizing the power consumption and the execution speed. The development of a correct, fast, power-efficient software that makes the most out of the features offered by the chip is therefore difficult.We choose as a case study a mini weather station composed of an STM32 microcontroller, sensors and actuators, and a first version of the embedded software. The analysis of the system and the addition of new features shows that the existing tools, although essential, do not allow to easily produce an efficient version of the software. We first propose to focus on power consumption. The first approach relies on the use of a so-called transactional model of the system, augmented with monitors that observe the behavior of the software executed in simulation. A monitor is dedicated to the detection of a given power-consuming behavior for which an efficient version can be implemented with the same hardware.This first approach, as well as the in-depth study of some microcontroller features, show that the dependencies between hardware elements are key information for the software development. These dependencies, as, for example, the value of a register and the state (on or off) of the clock of a block, are difficult to see with existing tools such or documentation.This thesis presents a new framework for modeling microcontrollers called Bubble Dump. It is meant to make the dependencies between hardware elements explicit, in order to assist the development of embedded software. The framework is formalized and implemented in a tool that allows the construction of models, the execution of embedded software in simulation. It also proposes a user interface to explore the dependencies.},
	author = {Morice, V.},
	year = {2022},
	eprinttype={HAL}, eprint = {tel-04076218},
	HAL_version = {v1},
}

@phdthesis{rosenberger_institutionbased_semantics_and_2022_tel-04360323,
	title = {Institution-based Semantics and Tool Support for the UML},
	abstract = {Model-based techniques, in particular the Unified Modeling Language (UML), have found wideadoption in the software industry. Formal methods can produce software which is guaranteed topossess desired properties, this being of particular interest where safety or security are concerned.Formal methods have been used very successfully in certain fields like the railway domain (e.g.,the verification of the fully automatic lines of the Paris metro system). However, in the widersoftware industry the adoption of formal methods has been limited. This thesis is part of an effortto ease the uptake of formal methods by enabling a fully formal use of the UML. In pursuing thisgoal, we want to follow software engineering best practices such as the don’t-repeat-yourselfprinciple and modularity.To achieve this, we use Institution Theory and the Heterogeneous Toolset (HeTS). InstitutionTheory is a principled way to relate different formalisms in a modular way. The HeterogeneousToolset is based on Institution Theory and implements tool reuse across different formalisms. Thisis the context into which we wish to integrate the UML, by providing institutional semantics andHeTS implementations for the different UML sublanguages. Translations between these UMLinstitutions then give joint semantics. Translations to other established languages implementedin HeTS allow us to borrow their tool-support.The contributions of this thesis to the effort outlined above consist in the development oflanguages for UML State Machines and Composite Structures and translations to the existinglanguage Casl. We give an account of our languages and translations in terms of InstitutionTheory, as well as a prototypical implementation in HeTS. Further, we verify properties based onspecifications in our languages to demonstrate the feasibility of our approach. The experiencesfrom our work on institutionalisation, implementation and verification moreover point to severalopportunities for future work.},
	author = {Rosenberger, T.},
	year = {2022},
	eprinttype={HAL}, eprint = {tel-04360323},
	HAL_version = {v1},
}

@phdthesis{schuh_implantation_sure_dapplications_2022_tel-03827333,
	title = {Implantation sûre d'applications temps-réel critiques sur plateforme pluri-coeur},
	abstract = {Les systèmes temps-réel critiques sont conçus pour garantir non seulement les fonctionnalités mais aussi des contraintes temporelles. Parmi ces systèmes, nous pouvons citer le domaine des transports (avionique, automobile, ferroviaire) mais aussi le domaine médical ou celui de l'énergie. Cette dernière décennie, ces systèmes ont été mis en œuvre sur des plateformes complexes telles que des plateformes multi/pluri-cœurs. La prédictibilité de ces systèmes est garantie par le calcul de temps d'exécution pire-cas pour une application et une plateforme données; auxquels s'ajoutent, dans le cas de plateformes multi-cœurs, les coûts des interférences dues aux accès aux ressources partagées.L'utilisation de plateformes multi/pluri-cœurs pour les systèmes temps-réel critiques est de plus en plus répandue dans l'industrie, et elle est un sujet d'étude bien représenté dans le monde de la recherche. Cette thèse fournit des solutions et études comparatives concernant plusieurs points clés. Notre flot de conception se concentre sur le choix de modèles d'exécution, sur le placement des tâches sur les cœurs et en mémoire ainsi que leur ordonnancement, et sur une modélisation de la plateforme cible et des interférences qu'elle induit. Ainsi, le flot proposé permet d'obtenir une implémentation sûre des applications critiques, avec des bornes garanties sur leurs temps de réponse.Les applications temps-réel critique que nous étudions sont celles qui peuvent être représentées sous forme de graphe dirigé acyclique (Directed Acyclic Graph, DAG), où les nœuds correspondent au code fonctionnel (tâches), et les arrêtes représentent des contraintes de précédence et/ou des communications de données. Ce type de représentation est typique de ce que produisent les environnements de développement de haut-niveau utilisés dans l'industrie. Dans cette thèse, nous étudions majoritairement des applications générées par l'outil SCADE, dont des études de cas directement extraites, ou largement inspirées d'applications industrielles.Dans le cadre de cette thèse, la plateforme cible est le processeur Kalray MPPA qui offre des caractéristiques intéressantes vis-à-vis de la prédictibilité. Cette architecture est pluri-cœurs, c'est-à-dire qu'elle offre deux niveaux de parallélisme : un ensemble de cœurs de calculs parallèles forme un multi-cœur (cluster), et l'ensemble des clusters parallèles forme la plateforme complète. Dans cette thèse, nous étudions différents modèles d'exécution qui permettent d'obtenir plus de prédictibilité sur des plateformes pluri/multi-cœurs. Une méthode d'implémentation de ces différents modèles sur Kalray MPPA2 et MPPA3 est proposée, qui permet de les comparer en terme de type de modèle (exécution phasée) et d'implémentation en isolation complète ou partielle (avec prise en compte des délais d'interférence). Ces travaux ont montré qu'il était, dans notre contexte, plus intéressant de ne pas utiliser une isolation complète mais de modéliser de façon précise les interférences et leurs effets. Pour les phases de placement sur les cœurs et la mémoire ainsi que l'ordonnancement, nous avons mis l'accent sur l'utilisation mémoire et les coûts de communication. Un algorithme préliminaire nous permet de montrer que ces deux facteurs sont primordiaux et devraient être centraux pour les travaux futurs.L'utilisation d'une nouvelle plateforme (Kalray MPPA3) a nécessité une modélisation fine des temps d'accès aux ressources partagées, ainsi que le développement d'une méthode de calcul des délais dûs aux interférences. Un modèle des communications (intra et inter-clusters) a été développé et couplé à un outil d'analyse de temps de réponse. Pour tous ces travaux, des extensions d'outils académiques et industriels ont été réalisées: modèle du MPPA3 pour l'analyse temporelle (Multi-Core Interference Analysis, MIA) et le développement d'applications (SHIM),génération du code de communication et d'orchestration pour les applications produite par SCADE.},
	author = {Schuh, M.},
	year = {2022},
	eprinttype={HAL}, eprint = {tel-03827333},
	HAL_version = {v1},
}

@phdthesis{werner_optimizing_identification_and_2022_tel-03719660,
	title = {Optimizing identification and exploitation of fault injection vulnerabilities on microcontrollers.},
	abstract = {Fault injection - for example by focused light, electromagnetic pulse, or power glitch - is an extremely powerful technique for compromising an embedded system. By physically disturbing the environment of the microcontroller, it is possible to modify its behavior to extract secret information, or to bypass security mechanisms. Although fault injection vulnerabilities are a potential threat to the security of many embedded systems, in practice, it is often difficult to identify and exploit them, because fault effects, which depend a lot on the target microcontroller and the fault injection equipment used, are not known in advance. In order to analyze fault injection vulnerabilities, fault effects can be simulated using fault models. However, depending on the model fidelity, some of the vulnerabilities identified may not be exploitable in practice because the modelized effect is not realistic.Accordingly, the main objective of this thesis is to propose new methods, techniques and tools to reduce the gap between simulation and experimentation, in order to optimize the identification and exploitation of these vulnerabilities. For this, we propose an end-to-end methodology, combining results obtained experimentally and by simulation, in order to infer the most probable fault models to improve the realism of the simulated faults. This first approach will lead us to take an interest in test programs designed to maximize the fault propagation. Thus, we propose original metrics to evaluate these tests, in order to design more efficient ones, and improve our understanding of fault effects. Finally, we propose to use, for the first time in fault injection, two recent optimization techniques to optimize the identification of the best equipment parameters, in order to speed up the exploitation of fault injection vulnerabilities.},
	author = {Werner, V.},
	year = {2022},
	eprinttype={HAL}, eprint = {tel-03719660},
	HAL_version = {v1},
}

@phdthesis{bégay_developing_and_certifying_2021_tel-03643235,
	title = {Developing and certifying in Coq/MathComp of Datalog optimizations for network verification},
	abstract = {Over the last decades, the world has gone more and more digital. This trend was not refuted in 2020 or 2021, as professional and personal services are increasingly provided and accessed through computers, tablets and mobile devices. This intense digital shift means that network failures are more costly and prejudicial than ever, let alone critical in many instances. We emphasize that the failures we mention and are interested in do not result from external attacks – which do occur on a weekly, if not daily basis and in industrial proportions –, but are to be seen as bugs.These bugs stem, first and foremost, from the extremely high complexity of network design, which in turn comes from the intrinsically distributed nature of networks. Moreover, networking has run for a long time on a duct tape culture, in the sense that it lacked formal foundations, and the possibilities that the existence and study of such foundations unlock.Over the last ten to fifteen years, researchers with a background in programming language theory have started to take an interest in networking, and how they could apply their theoretical tools and approaches to this field. Combined with the critically increased need for safety (and security), this situation led to the introduction of formal methods for networks. This trend is also fostered by the latest advances in formal methods, both in terms of modeling techniques and computational efficiency (e.g. the existence of fast solvers such as Z3).One such tool that was introduced is Network Optimized Datalog (NoD), a Datalog engine developed at Microsoft and tailored to handle programs that describe, in the form of horn clauses, the behavior of a particular network. Although an interesting step in the desired direction, using this engine requires engineers to manually write encodings of each analyzed network, which in itself is a complex and error-prone process.Moreover, NoD does not scale with naive translations of real-size networks. In practice, the authors work with programs that contain many inlined values, using manual, convoluted, undocumented and unjustified Datalog-level program transformations. This gap in an otherwise remarkable tool led us to work on the design and automatization of such program transformations, this time with a full formalization.However, having a formalization of non-trivial operations is not enough to trust them. The aim of our work has then been the formal verification of these transformations in the Coq proof assistant, using (and slightly extending) an existing Coq implementation of Datalog.Although inspired by network verification, our work is not circumscribed to it. Concretely, the analyses and rewritings we provide can be used – and relevant – in other contexts. Moreover, we believe that this works brings a new insight into the semantics and formal study of Datalog programs, which may serve as the basis of future works in other contexts.},
	author = {Bégay, P.-L.},
	year = {2021},
	eprinttype={HAL}, eprint = {tel-03643235},
	HAL_version = {v1},
}

@phdthesis{khoussi_rigorous_modeling_and_2021_tel-03728262,
	title = {Rigorous modeling and performance evaluation of networking systems},
	abstract = {The demand for faster performance, increased accessibility, mobility and securecommunications has driven significant advancements in Internet architectures, protocols and applications. Whether Internet usage relates to businesses or entertainment, its performance and security are two of the highest orders. Recent advances in modern technology and network innovations have driven the desire to move away from manual error-prone methods of testing network components and evolve from the ad-hoc tools and simulation based testing which are, traditionally, used in assessing the performance of networking components but fail to achieve high accuracy results and obtain trustworthy analysis.Despite the criticism that formal verification (FV) methods have been receivingand lack of appreciation, they have achieved undeniable results and made great contributions in this field and other mature fields. For this reason, we investigate a FV methodology for analyzing the performance aspect of networking systems. We rely on a model-based approach that is based on building a rich faithful stochastic model of a system, then apply statistical model checking to assess its performance against a specified requirement. We explain that the stochastic behavior of the model is captured by introducing probabilistic variables which are updated via probability distributions. The latter are, typically, obtained by collecting and analyzing measurements from the system’s execution using traditional statistical tests to select the best fit distribution (i.e., process of distribution fitting). Unfortunately, distribution fitting requires a good statistical background and familiarity with several distributions which is beyond the expertise of some analysts.As such, we developed a tool called DeepFit that combines traditional statisticaltests and deep learning to automate the distribution fitting task. DeepFit is thenintegrated into the workflow of our FV methodology for rigorous modeling andperformance assessment of networking systems.},
	author = {Khoussi, S.},
	year = {2021},
	eprinttype={HAL}, eprint = {tel-03728262},
	HAL_version = {v1},
}

@phdthesis{recoules_verification_automatique_de_2021_tel-03719227,
	title = {Vérification automatique de code bas-niveau : C, assembleur et binaire},
	abstract = {Les méthodes formelles pour le développement logiciel ont fait de grands progrès au cours des deux dernières décennies, au point que leur application dans les logiciels embarqués critiques pour la sûreté est un succès indéniable. Leur application aux logiciels non critiques est cependant l’un des défis majeurs à venir. Par exemple, les programmeurs C utilisent régulièrement l’assembleur embarqué (inline assembly)GNU pour réaliser des optimisations de bas niveau ou accéder aux primitives du système. Cela a généralement pour conséquence de rendre inopérants les analyseurs formels de pointe développés pour C. Ceci est doublement problématique puisque l’assembleur embarqué est notoirement difficile à écrire correctement : non seulement le morceau d’assembleur peut contenir des erreurs, mais il y a également un risque d’incompatibilité à l’interface entre C et assembleur, ce qui peut entraîner des bugs subtils et difficiles à trouver. Nous proposons d’attaquer le problème de la vérification de programmes C contenant de l’assembleur embarqué. Nous avons donc conçu deux techniques, nommées RUSTInA et TInA, basées sur une formalisation originale de l’assembleur embarqué, ainsi que de nouveaux algorithmes dédiés. RUSTInA est la première technique automatisée pour la vérification formelle de la conformité de l’interface de l’assembleur embarqué (c’est-à-dire l’absence d’incompatibilité entre le code et l’interface), avec la capacité supplémentaire de proposer des correctifs (prouvés) et des raffinements de code (optimisation). TInA est la première technique de traduction automatique, générique, adaptée aux outils de vérification formelle et digne de confiance qui transforme l’assembleur embarqué en code C sémantiquement équivalent, afin de tirer parti des analyseurs C existants. Des expériences intensives sur du code réel (tous les morceaux d’assembleur embarqué trouvés dans les paquets de Debian Jessie) ont permis de remonter 986 problèmes significatifs dans 54 paquets,dont 156 problèmes de 7 paquets qui ont été signalés avec succès et traités par les développeurs grâce à notre génération automatique de correctifs. Ces expériences montrent également la faisabilité de notre traduction « orientée pour la vérification »et ces avantages pour les analyseurs C de l’état de l’art.},
	author = {Recoules, F.},
	year = {2021},
	eprinttype={HAL}, eprint = {tel-03719227},
	HAL_version = {v1},
}

@phdthesis{six_optimized_and_formallyverified_2021_tel-03326923,
	title = {Optimized and formally-verified compilation for a VLIW processor},
	abstract = {Software programs are used for many critical roles. A bug in those can have a devastatingcost, possibly leading to the loss of human lives. Such bugs are usually found at a source level(which can be ruled out with source-level verification methods), but they can also be inserted bythe compiler unknowingly. CompCert is the first compiler with a formal proof of correctness:compiled programs are proven to behave the same as their source programs. However, because ofthe challenges involved in proving compiler optimizations, CompCert only has a limited numberof them. As such, CompCert usually generates low-performance code compared to classicalcompilers such as GCC. While this may not significantly impact out-of-order architectures suchas 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 isexplicit and specified in the assembly code through “bundles” of instructions: the compiler mustbundlize instructions to achieve good performance.In this thesis, we identify, investigate, implement and formally verify several classical optimiza-tions missing in CompCert. We start by introducing a formal model for VLIW bundles executionon 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 furtherincrease the performance of our generated code by implementing loop unrolling, loop rotationand loop peeling – the latter being used for Loop-Invariant Code Motion. These transformationsare verified by translation validation, some of them with hash-consing to achieve reasonablecompilation time.We evaluate each introduced optimization on benchmarks, including Polybench and TACleBench,on the KV3 VLIW core, ARM Cortex A53, and RiscV “Rocket” core. Thanks to this work, ourversion of CompCert is now only 16\% slower (respectively 12\% slower and 30\% slower) than GCC -O2 on the KV3 (respectively ARM and RiscV), instead of 50\% (respectively 38\% and45\%).},
	author = {Six, C.},
	year = {2021},
	eprinttype={HAL}, eprint = {tel-03326923},
	HAL_version = {v2},
}

@phdthesis{boutonnet_modular_analysis_of_2020_tel-02554125,
	title = {Modular analysis of numerical properties by abstract interpretation},
	abstract = {Any software bug or device malfunction in safety-critical systems can have catastrophicconsequences. The validation and analysis of programs in critical systems is of paramountimportance to guarantee that the software satisfies its specification and that it is devoidedof runtime errors.Static program analysis by abstract interpretation computes a sound approximationof the set of reachable states of a program. It discovers invariant properties of programswhich are represented by elements of an abstract domain. Most industrial static analysistools do not use expressive relational numerical abstract domains like convex polyhedradue to their computational cost.We propose a new modular analysis for the automatic discovery of numerical propertiesbased on the computation of disjunctive relational summaries of procedures. Proceduresummaries are computed once and for all, and used to compute the effect of procedurecalls, in a bottom-up fashion. Our approach is especially applied to improve the scalabilityof Linear Relation Analysis, or abstract interpretation with convex polyhedra, althoughit is based on a more general framework usable with any relational abstract domain.Disjunctive relational summaries are finite sets of abstract input-output relations represented by elements of a relational abstract domain. They are computed based on apartitioning of procedure preconditions. We give heuristics to compute an abstract partition of a procedure precondition. We also give ways to improve the precision of summarycomputation, notably through a careful treatment of preconditions during analysis. Ourapproach also applies to recursive procedures where summaries are computed recursivelyin terms of themselves.We implemented our approach in a new static analysis platform for C programs calledmars. We conducted experiments on programs from the Mälardalen benchmark showingthat our approach can significantly reduce the analysis time for Linear Relation Analysiscompared to a full context-sensitive analysis where procedures are analyzed completelyin each call context. Analysis precision is not significantly damaged and can even beimproved due to the use of disjunction.In a second part, we present an approach for the modular analysis of reactive systems for numerical properties. We propose a flexible representation of the behavior ofreactive components called Relational Mode Automata (RMA), which allows the analysisof reactive systems behavior at various levels of abstraction. RMA can be constructedautomatically from disjunctive summaries of the procedures implementing componentreactions. The analysis results of individual components using RMA can be reused toanalyze larger reactive systems with multiple component instantiations in a modular way.We give an application of this approach to the analysis of a simplified automated subwaycontrol system.},
	author = {Boutonnet, R.},
	year = {2020},
	eprinttype={HAL}, eprint = {tel-02554125},
	HAL_version = {v2},
}

@phdthesis{farinier_decision_procedures_for_2020_tel-02988031,
	title = {Decision procedures for vulnerability analysis},
	abstract = {Formal methods have repeatedly demonstrated their relevance in search and analysis of bugs. If current methods are well suited to critical code analysis where mistakes are not a possible option, they are less interested on non-critical programs. Indeed, on such programs bugs are too numerous and only the most serious are corrected, a practice that does not fit well with today's tools.The aim of this thesis is therefore to allow such a gradation in the context of formal methods, which involves developing new decision procedures tailored to vulnerability analysis.},
	author = {Farinier, B.},
	year = {2020},
	eprinttype={HAL}, eprint = {tel-02988031},
	HAL_version = {v1},
}

@phdthesis{salwan_l’usage_de_l’execution_2020_tel-02966552,
	title = {L’usage de l’exécution symbolique pour la déobfuscation binaire en milieu industriel},
	abstract = {Cette thèse a été faite dans un cadre industriel où les activités principales sont la rétro-ingénierie pour la recherche de vulnérabilités et la vérification de certaines propriétés de sécurité sur des programmes déjà compilés. La première partie de cette thèse porte sur la collecte et le partage des problématiques industrielles lors de l’analyse de programmes binaires. Basé sur ces problématiques, un cadre de travail d’analyse dynamique binaire a été développé et formalisé. Des exemples réels d’utilisation y sont ensuite présentés tels que la détection de prédicats opaques dans les conditions de branchement. Enfin, une nouvelle approche automatique permettant la dévirtualisation de code binaire y est présentée en combinant les fonctionnalités du cadre de travail ainsi que celles d’autres outils.},
	author = {Salwan, J.},
	year = {2020},
	eprinttype={HAL}, eprint = {tel-02966552},
	HAL_version = {v1},
}

@phdthesis{xu_generalisation_of_alternating_2020_tel-02964621,
	title = {Generalisation of Alternating Automata over Infinite Alphabets},
	abstract = {The language inclusion problem is recognised as being central to verification in different domains, such as hardware, communication protocols, software systems, etc. There we might face two challenges: non-determinism and infinite alphabets.We propose two models of alternating automata over infinite alphabets: (i) alternating data automata (ADA) and (ii) first-order alternating data automata (FOADA). They both recognise the data words over infinite alphabets. In ADA model, the control states are Booleans and the transition rules are specified by a set of formulae in a combined first-order theory of states (Booleans) and data that relate past values of variables with current values of variables. But a restriction of the ADA model is that, there is not hidden variable, hence all the data values taken by the variables are visible in the input. But in FOADA model, the arguments of a predicate atom track the values of the internal variables associated with the state, and these values are invisible in the input sequence, which overcomes the restriction of the ADA model.With these two alternating models, Boolean operations of union, intersection and comple- ment can be done in linear time, thus matching the complexity of performing these opera- tions in the finite-alphabet case. However, the price to be paid here is that the emptiness checking becomes undecidable. For this reason, we provide two efficient semi-algorithms for emptiness checking: (i) lazy predicate abstraction and (ii) IMPACT method. These semi-algorithms are proven to terminate by returning a word from the language of the given au- tomaton if one exists; but if the language of the given automaton is empty, then the termination is not guaranteed.The main application of our models is checking inclusions between various classes of au- tomata extended with variables ranging over infinite domains that recognise languages over infinite alphabets. The most widely known classes of this kind are timed automata and finite- memory (register) automata. Another application is checking safety (mutual exclusion, absence of deadlocks, etc.) and liveness (termination, lack of starvation, etc.) properties of parameterised concurrent programs.Besides the theoretical parts, we also have developed a tool - FOADA Checker, mainly used for checking inclusion between two automata or checking emptiness of an automaton. FOADA Checker is written in Java, via Java-SMT interface and using Z3 SMT solver for spuriousness, coverage queries and interpolant generation. The IMPACT semi-algorithm has been implemented in the tool to check the emptiness of an automaton.},
	author = {Xu, X.},
	year = {2020},
	eprinttype={HAL}, eprint = {tel-02964621},
	HAL_version = {v1},
}

@phdthesis{el_ballouli_modeling_selfconfiguration_in_2019_tel-02175324,
	title = {Modeling self-configuration in Architecture-based self-adaptive systems},
	abstract = {Modern systems are pressured to adapt in response to their constantly changing environment to remain useful. Traditionally, this adaptation has been handled at down times of the system. there is an increased demand to automate this process and achieve it whilst the system is running. Self-adaptive systems were introduced as a realization of continuously adapting systems. Self-adaptive systems are able to modify at runtime their behavior and/or structure in response to their perception of the environment, the system itself, and their requirements. The focus of this work is on realizing self-configuration, a key and essential property of self-adaptive systems. Self-configuration is the capability of reconfiguring automatically and dynamically in response to changes. This may include installing, integrating, removing and composing/decomposing system elements.This thesis introduces the Dr-BIP framework, an extension of the BIP framework for modeling self-configuring systems that relies on a model-based and component & connector approach to prescribe systems. The combination of both of these approaches exploits the benefits of each, making their combination an ideal methodology to realize complex self-configuring systems.A Dr-BIP system model is a runtime model which captures the running system at three different levels of abstraction namely behavior, configuration, and configuration variants. The system's configuration is captured by component and connectors. In a component and connector system, self-configuration can have three different levels of granularity which includes the ability to add or remove connectors, add or remove components, and add or remove subsystems. Dr-BIP supports explicit addition and removal of both components and subsystems, but implicit addition and removal of connectors. The main advantage of relying on an implicit addition and removal of connectors is the ability to guarantee by construction specific configuration topologies.To capture the three levels of abstraction, we introduce motifs as primary structures to prescribe a self-configuring Dr-BIP system. A motif defines a set of components that evolve according to interaction and reconfiguration rules. A system is composed of multiple motifs that possibly share components and evolve together. Interaction rules dictate how components composing the system can interact and reconfiguration rules dictate how the system configuration can evolve over time. Finally, we show that the proposed framework is both minimal and expressive by modeling four different self-configuring systems. Last but not least, we propose a modeling language to codify the framework concepts and provision an interpreter implementation.},
	author = {El ballouli, R.},
	year = {2019},
	eprinttype={HAL}, eprint = {tel-02175324},
	HAL_version = {v1},
}

@phdthesis{kahil_schedulability_in_mixedcriticality_2019_tel-02462740,
	title = {Schedulability in Mixed-criticality Systems},
	abstract = {Real-time safety-critical systems must complete their tasks within a given time limit. Failure to successfully perform their operations, or missing a deadline, can have severe consequences such as destruction of property and/or loss of life. Examples of such systems include automotive systems, drones and avionics among others. Safety guarantees must be provided before these systems can be deemed usable. This is usually done through certification performed by a certification authority.Safety evaluation and certification are complicated and costly even for smaller systems.One answer to these difficulties is the isolation of the critical functionality. Executing tasks of different criticalities on separate platforms prevents non-critical tasks from interfering with critical ones, provides a higher guaranty of safety and simplifies the certification process limiting it to only the critical functions. But this separation, in turn, introduces undesirable results portrayed by an inefficient resource utilization, an increase in the cost, weight, size and energy consumption which can put a system in a competitive disadvantage.To overcome the drawbacks of isolation, Mixed Criticality (MC) systems can be used. These systems allow functionalities with different criticalities to execute on the same platform. In 2007, Vestal proposed a model to represent MC-systems where tasks have multiple Worst Case Execution Times (WCETs), one for each criticality level. In addition, correctness conditions for scheduling policies were formally defined, allowing lower criticality jobs to miss deadlines or be even dropped in cases of failure or emergency situations.The introduction of multiple WCETs and different conditions for correctness increased the difficulty of the scheduling problem for MC-systems. Conventional scheduling policies and schedulability tests proved inadequate and the need for new algorithms arose. Since then, a lot of work has been done in this field.In this thesis, we contribute to the study of schedulability in MC-systems. The workload of a system is represented as a set of jobs that can describe the execution over the hyper-period of tasks or over a duration in time. This model allows us to study the viability of simulation-based correctness tests in MC-systems. We show that simulation tests can still be used in mixed-criticality systems, but in this case, the schedulability of the worst case scenario is no longer sufficient to guarantee the schedulability of the system even for the fixed priority scheduling case. We show that scheduling policies are not predictable in general, and define the concept of weak-predictability for MC-systems. We prove that a specific class of fixed priority policies are weakly predictable and propose two simulation-based correctness tests that work for weakly-predictable policies.We also demonstrate that contrary to what was believed, testing for correctness can not be done only through a linear number of preemptions.The majority of the related work focuses on systems of two criticality levels due to the difficulty of the problem. But for automotive and airborne systems, industrial standards define four or five criticality levels, which motivated us to propose a scheduling algorithm that schedules mixed-criticality systems with theoretically any number of criticality levels. We show experimentally that it has higher success rates compared to the state of the art.We illustrate how our scheduling algorithm, or any algorithm that generates a single time-triggered table for each criticality mode, can be used as a recovery strategy to ensure the safety of the system in case of certain failures.Finally, we propose a high level concurrency language and a model for designing an MC-system with coarse grained multi-core interference.},
	author = {Kahil, R.},
	year = {2019},
	eprinttype={HAL}, eprint = {tel-02462740},
	HAL_version = {v1},
}

@phdthesis{lo_application_des_architectures_2019_tel-02180636,
	title = {Application des architectures many core dans les systèmes embarqués temps réel},
	abstract = {Les processeurs mono-coeurs traditionnels ne sont plus suffisants pour répondre aux besoins croissants en performance des fonctions avioniques. Les processeurs multi/many-coeurs ont emergé ces dernières années afin de pouvoir intégrer plusieurs fonctions et de bénéficier de la puissance par Watt disponible grâce aux partages de ressources. En revanche, tous les processeurs multi/many-coeurs ne répondent pas forcément aux besoins des fonctions avioniques. Nous préférons avoir plus de déterminisme que de puissance de calcul car la certification de ces processeurs passe par la maîtrise du déterminisme. L’objectif de cette thèse est d’évaluer le processeur many-coeur (MPPA-256) de Kalray dans un contexte industriel aéronautique. Nous avons choisi la fonction de maintenance HMS (Health Monitoring System) qui a un besoin important en bande passante et un besoin de temps de réponse borné.Par ailleurs, cette fonction est également dotée de propriétés de parallélisme car elle traite des données de vibration venant de capteurs qui sont fonctionnellement indépendants, et par conséquent leur traitement peut être parallélisé sur plusieurs coeurs. La particularité de cette étude est qu’elle s’intéresse au déploiement d’une fonction existante séquentielle sur une architecture many-coeurs en partant de l’acquisition des données jusqu’aux calculs des indicateurs de santé avec un fort accent sur le fluxd’entrées/sorties des données. Nos travaux de recherche ont conduit à 5 contributions:• Transformation des algorithmes existants en algorithmes incrémentaux capables de traiter les données au fur et mesure qu’elles arrivent des capteurs.• Gestion du flux d’entrées des échantillons de vibrations jusqu’aux calculs des indicateurs de santé,la disponibilité des données dans le cluster interne, le moment où elles sont consommées et enfinl’estimation de la charge de calcul.• Mesures de temps pas très intrusives directement sur le MPPA-256 en ajoutant des timestamps dans le flow de données.• Architecture logicielle qui respecte les contraintes temps-réel même dans les pires cas. Elle estbasée sur une pipeline à 3 étages.• Illustration des limites de la fonction existante: nos expériences ont montré que les paramètres contextuels de l’hélicoptère tels que la vitesse du rotor doivent être corrélés aux indicateurs de santé pour réduire les fausses alertes.},
	author = {Lo, M.},
	year = {2019},
	eprinttype={HAL}, eprint = {tel-02180636},
	HAL_version = {v1},
}

@phdthesis{mediouni_modeling_and_analysis_2019_tel-02305867,
	title = {Modeling and Analysis of Stochastic Real-Time Systems},
	abstract = {In this thesis, we address the problem of modeling and verification of complex systems exhibiting both probabilistic and timed behaviors. Designing such systems has become increasingly complex due to the heterogeneity of the involved components, the uncertainty resulting from open environment and the real-time constraints inherent to their application domains. Handling both software and (abstraction of) hardware in a unified view while also including performanceinformation (e.g. computation and communication times, energy consumption, etc.) becomes a must. Building and analyzing performance models is of paramount importance in order to give guarantees on the functional and extra-functional system requirements and to make well-founded design decisions based on quantitative measures at early design stages.This thesis brings several new contributions. First, we introduce a new modeling formalism called Stochastic Real-Time BIP (SRT-BIP) for the modeling, the simulation and the code generation of component-based systems. This formalism inherits from the BIP framework its component-based and real-time modeling capabilities and, extends it by providing comprehensive primitives to express complex stochastic behaviors.Second, we investigate machine learning techniques to ease the construction of performance models. We propose to enhance and adapt a state-of-the-art learning procedure to infer stochastic real-time models from concrete system execution and to represent them in the SRT-BIP formalism.Third, given performance models in SRT-BIP, we explore the use of statistical Model Checking (SMC) for the anaysis of system’s functional and performance requirements. To do so, we provide a full framework, called SBIP, as a support tool for the modeling, simulation and analysis of SRT-BIP systems. SBIP is an Integrated Development Environment (IDE) that implements SMC algorithms for quantitative, qualitative and rare events analyses together with an automated exploring procedure for parameterized requirements. We validate our proposalson real-life case studies ranging from communication protocols and concurrent systems to embedded systems.Finally, we further investigate the interest of SMC when included in elaborated system analysis workflows. We illustrate this by proposing two risk assessment approaches. In the first approach, we introduce a spiral methodology to build resilient systems with FDIR components that we validate on the safety assessment of a planetary rover locomotion system. The second approach is concerned with the security assessment of organization’s defenses following an offensive security approach. The goal is to synthesize impactful defense configurations against optimized attack strategies (that minimize attack cost and maximize success probability). These attack strategies are obtained by combining model learning with meta heuristics, and where SMC is used to score and prioritize potential candidate strategies.},
	author = {Mediouni, B. L.},
	year = {2019},
	eprinttype={HAL}, eprint = {tel-02305867},
	HAL_version = {v1},
}

@phdthesis{touzeau_static_analysis_of_2019_tel-02510350,
	title = {Static analysis of least recently used caches : complexity, optimal analysis, and applications to worst-case execution time and security},
	abstract = {The certification of real-time safety critical programs requires bounding their execution time.Due to the high impact of cache memories on memory access latency, modern Worst-Case Execution Time estimation tools include a cache analysis.The aim of this analysis is to statically predict if memory accesses result in a cache hit or a cache miss.This problem is undecidable in general, thus usual cache analyses perform some abstractions that lead to precision loss.One common assumption made to remove the source of undecidability is that all execution paths in the program are feasible.Making this hypothesis is reasonable because the safety of the analysis is preserved when adding spurious paths to the program model.However, classifying memory accesses as cache hits or misses is still hard in practice under this assumption, and efficient cache analysis usually involve additional approximations, again leading to precision loss.This thesis investigates the possibility of performing an optimally precise cache analysis under the common assumption that all execution paths in the program are feasible.We formally define the problems of classifying accesses as hits and misses, and prove that they are NP-hard or PSPACE-hard for common replacement policies (LRU, FIFO, NRU and PLRU).However, if these theoretical complexity results legitimate the use of additional abstraction, they do not preclude the existence of algorithms efficient in practice on industrial workloads.Because of the abstractions performed for efficiency reasons, cache analyses can usually classify accesses as Unknown in addition to Always-Hit (Must analysis) or Always-Miss (May analysis).Accesses classified as Unknown can lead to both a hit or a miss, depending on the program execution path followed.However, it can also be that they belong to one of the Always-Hit or Always-Miss category and that the cache analysis failed to classify them correctly because of a coarse approximation.We thus designed a new analysis for LRU instruction that is able to soundly classify some accesses into a new category, called Definitely Unknown, that represents accesses that can lead to both a hit or a miss.For those accesses, one knows for sure that their classification does not result from a coarse approximation but is a consequence of the program structure and cache configuration.By doing so, we also reduce the set of accesses that are candidate for a refined classification using more powerful and more costly analyses.Our main contribution is an analysis that can perform an optimally precise analysis of LRU instruction caches.We use a method called block focusing that allows an analysis to scale by only analyzing one cache block at a time.We thus take advantage of the low number of candidates for refinement left by our Definitely Unknown analysis.This analysis produces an optimal classification of memory accesses at a reasonable cost (a few times the cost of the usual May and Must analyses).We evaluate the impact of our precise cache analysis on the pipeline analysis.Indeed, when the cache analysis is not able to classify an access as Always-Hit or Always-Miss, the pipeline analysis must consider both cases.By providing a more precise memory access classification, we thus reduce the state space explored by the pipeline analysis and hence the WCET analysis time.Aside from this application of precise cache analysis to WCET estimation, we investigate the possibility of using the Definitely Unknown analysis in the domain of security.Indeed, caches can be used as side-channel to extract some sensitive data from a program execution, and we propose a variation of our Definitely Unknown analysis to help a developer finding the source of some information leakage.},
	author = {Touzeau, V.},
	year = {2019},
	eprinttype={HAL}, eprint = {tel-02510350},
	HAL_version = {v1},
}

@phdthesis{yu_towards_an_efficient_2019_tel-02964528,
	title = {Towards an Efficient Parallel Parametric Linear Programming Solver},
	abstract = {VPL (Verified Polyhedra Library) is an abstract polyhedra domain using constraint-only description. All main operators boiled down to polyhedral projection, which can be computed using Fourier-Motzkin elimination. This method generates many redundant constraints which must be eliminated at a high cost. A novel algorithm was implemented in VPL for computing the polyhedral projection using parametric linear programming (PLP), which can replace Fourier-Motzkin elimination. This PLP solver can also be used for computing the join operator (convex hull). Our work focuses on improving the efficiency of the algorithm of PLP solver.In prior work, PLP was done in arbitrary precision rational arithmetic. In this work, we present an approach where most of the computations are performed in floating-point arithmetic, and then exact rational results are reconstructed. The result obtained from our approach is guaranteed to be sound. We also propose a workaround for a difficulty called degeneracy, which plagued previous attempts at using PLP for computations on polyhedra: in general the (parametric) linear programming problems are degenerated, resulting in redundant computations and duplicates in geometric descriptions.The algorithm of the PLP solver is intrinsically parallelable, however it was developed in VPL with OCaml, which does not well support parallelism programming. In our approach, which is implemented with C++, we proposed a task-based scheme for parallelizing it. Two parallel implementations have been realized using two different parallel mechanisms: Intel’s Thread Building Blocks (TBB) and OpenMP tasks.},
	author = {Yu, H.},
	year = {2019},
	eprinttype={HAL}, eprint = {tel-02964528},
	HAL_version = {v1},
}
