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 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.
Keywords: Formal verification, Translation validation, Symbolic execution, Compiler optimizations, RISC-V, the Coq proof assistant, the CompCert compiler.
Les compilateurs sont des systèmes logiciels très complexes et peuvent donc contenir des bogues. Ces bogues peuvent se traduire par des erreurs au cours du processus de compilation ou, plus ennuyeusement encore, par la génération d’un code incorrect. Les bogues qui altèrent subtilement la sémantique des programmes générés sont souvent très insidieux et difficiles à retracer. Dans certaines applications, en particulier dans les systèmes embarqués critiques pour la sécurité et sujets à des exigences et régulations strictes (par exemple, avionique, trains, etc.), l’élimination de ces bogues est d’une importance capitale.
Bien que la plupart de ces bogues soient typiquement situés dans les passes d’optimisation, la désactivation des optimisations n’est pas une solution viable dans de nombreuses applications. En fait, la simple désactivation des optimisations ne suffit pas à garantir un code exempt de bogues. Les normes réglementaires imposent en général l’utilisation de processeurs simples et prédictibles, dont la performance dépend largement du compilateur.
Une solution alternative est d’employer un compilateur certifié, mécaniquement prouvé correct dans un assistant de preuve. Un tel compilateur assure que le code assembleur généré préserve fidèlement la sémantique du code source. CompCert appartient à cette catégorie, et est le premier compilateur C formellement vérifié et largement utilisé dans l’industrie. Cependant, prouver la correction d’optimisations complexes reste un défi. C’est pourquoi les compilateurs certifiés, y compris CompCert, produisent un code significativement moins performant que les compilateurs classiques tels que GCC ou LLVM.
La validation de traduction est une technique où seul le résultat d’une optimisation est vérifié, plutôt que de prouver la correction de son implémentation. L’algorithme d’optimisation, appelé oracle, reste considéré comme non fiable. Néanmoins, ses résultats sont toujours soumis à la validation par un validateur prouvé et conçu pour rejeter toute erreur.
Dans cette thèse, nous approfondissons le concept de validation de traduction guidée. Le principe est de permettre aux oracles de guider le validateur en lui fournissant des indices qui réduisent l’espace de recherche, minimisant ainsi la complexité du processus de validation. Plus précisément, nous proposons un interpréteur symbolique formellement vérifié capable de valider toute une classe de transformations. Notre outil demande aux oracles des invariants de programme en tant qu’indices pour guider la simulation symbolique du code original et du code optimisé. Le test de simulation prouvé valide défensivement les optimisations appliquées, en garantissant leur cohérence vis-à-vis du code non optimisé.
Nous avons validé avec succès plusieurs nouvelles transformations en utilisant cette approche, dont certaines n’avaient jamais été formellement vérifiées jusqu’alors, grâce à la communication entre les oracles et leur validateur. Notamment, nous avons vérifié une optimisation de ”strength-reduction” (littéralement, ”réduction de force”) ciblant les architectures RISC-V 64 bits, qui sont prometteuses dans le contexte des systèmes embarqués critiques pour la sécurité. En plus de la ”strength-reduction”, notre outil de simulation symbolique supporte l’élimination de redondances partielles, l’élimination du code mort, le déplacement de code, l’ordonnancement, et une forme faible de pipeline logiciel avec renommage.
Nous avons intégré notre mécanisme de validation dans notre version de développement (fork) de CompCert, en développant une nouvelle représentation intermédiaire nommée ”Block Transfer Language”, BTL (littéralement “Langage de Transfert en Blocs”). Les traductions de et vers BTL sont également validées de manière défensive, à l’aide d’un vérificateur dédié, formellement vérifié, et capable de valider de la duplication et factorisation de code en tant que morphismes des graphes de flux de contrôle. Pour évaluer rigoureusement l’impact de nos optimisations et le temps de compilation supplémentaire induit par leur validation, nous avons effectué de multiples mesures expérimentales du temps de compilation et des performances à l’exécution. Les optimisations spécifiques à une architecture cible ont été testées sur des plateformes AArch64 et RISC-V. Les résultats montrent une amélioration significative des performances à l’exécution tout en maintenant un temps de compilation raisonnable.
À l’avenir, cette même méthode pourrait potentiellement être appliquée pour valider d’autres transformations, comme l’insertion automatique de contre-mesures de sécurité. Nos conceptions semblent être applicables au-delà de CompCert.
Mots clefs : Vérification formelle, Validation de traduction, Exécution symbolique, Optimisations de compilateur, RISC-V, L’assistant de preuve Coq, Le compilateur certifié CompCert.