Optimization of source code for safety-critical systems
Optimisation du code source pour les systèmes critiques de sécurité
Résumé
A computer system is safety-critical when it can cause serious damages to property, the environment, human life, or to the societyas a whole. Real-world safety-critical systems are also necessarily complex, because, in order to take into account the interactionsbetween software, hardware, the physical environment, and sometimes their distributed nature (systems of systems), they need to implementa variety of safety measures, in software, in hardware, in the system design, at development time, at compile time, and at run-time. Those safety measureswhich vary from one safety-critical system to another very often lead to decrease of performance, for increase of execution time of software.This research work is situated in the context of one such system, the communication-based train control (CBTC) system ofSiemens Mobility France which operates a number of driverless subway systems around the World, including the Paris lines 1, 4, and 14. That system is certified according to the industrial norm EN-50128and up to the highest Safety Integrity Level 4, required for safety-critical systems with potentially catastrophic consequences.In this context, the thesis looks for an answer to the question of how to automatically optimize execution time performance of such systems withoutloosing the previously obtained safety guarantees.The answer provided by this thesis is provably correct optimization of source code. A first contribution is a source-to-source compilerfor VCP Ada (a subset of Ada) programs, that optimizes source code while preserving the formal semantics of the programs. The compiler has been provencorrect in the Coq proof assistant and guarantees the equivalence of execution between the original and the optimized program. Thecompiler copes with the complexities of the platform, due to hardware safety measures, which is important, since real-worldsafety-critical system are often susceptible to have such measures, potentially conflicting with existing formally proven optimizingcompilers. Moreover, choosing the approach of a source-to-source compilation shows to have methodological advantages over an approachto proven optimizations having a number of intermediate languages, allowing to simplify and diminish the needed proof effort.A second contribution is to the problem of provably correct lexical analysis of compilers, which has previously not received a lot ofresearch attention, a weak link in any compilation chain using a proven or qualified compiler. We develop CoqLex, the firstCoq-formalized lexer generator, based on a modification of an existing Coq implementation of regular expression matching viaBrzozowski derivatives.The developed theory and tools have been applied to optimize real-world VCP Ada programs of CBTC systems, consisting of thousandsof source files, with promising results.
Un système informatique est dit critique de sécurité lorsqu'il peut causer de graves dommages matériels, environnementaux ou humains.Ce type de système est nécessairement complexe, car les interactions entre logiciel, matériel et environnement,nécessitent l'implémentation de mesures de sécurité aussi bien au niveau logiciel que matérielpendant leur conception, leur développement, leur compilation et leur exécution. Ces mesures de sécurité qui varient un système à un autreconduisent très souvent à des dégradations de performances, en particulier l'augmentation du temps d'exécution.Ce travail de recherche se situe dans le contexte du système CBTC (Communication-Based Train Control) deSiemens Mobility France, un système de contrôle de train certifié EN-50128 et SIL-4 (le plus haut niveau de sûreté) dans le développement de nombreux systèmes de pilote automatiqueà travers le monde, en particulier sur les lignes 1, 4 et 14 du métro parisien.Dans ce contexte, le but de cette thèse est de trouver des solutions pour réduire le temps d'exécution de ces systèmes tout en conservantles garanties de sécurité déjà acquises.La réponse apportée par cette thèse est une optimisation formellement vérifiée du code source. Une première contribution est un compilateur VCP Ada (un sous-ensemble d'Ada)vers VCP Ada, qui optimise le code source tout en préservant la sémantique des programmes. Ce compilateur a été implémenté avecl'assistant de preuve Coq et fourni des preuves en Coq qui garantissent l'équivalence entre le programme original et le programme optimisé.Ce compilateur tient aussi compte des complexités liées aux mesures de sécurité matérielle qui sont potentiellement incompatibles avec l'utilisation des compilateursformellement vérifiés existants. Par ailleurs, le choix de l'application des optimisations sur le code source présente des avantages méthodologiques parrapport aux optimisations utilisant de nombreux langages intermédiaires, car ils permettent de simplifier et de réduire l'effort de preuve nécessaire.Une deuxième contribution concerne la vérification formelle des analyseurs lexicaux des compilateurs, qui n'a jusqu'à présent, pas reçu beaucoup l'attention de la part deschercheurs, créant donc un maillon faible dans la chaîne de compilation. Nous avons développé CoqLex, le premier générateur d'analyseur lexical formellement vérifié en Coq, basé sur unemodification d'une implémentation existante en Coq des expressions régulières via les dérivés de Brzozowski.La théorie et les outils développés ont été utilisés pour optimiser les programmes VCP Ada des systèmes CBTC, composés de milliers de fichiers sources, avec desrésultats prometteurs.
Origine : Version validée par le jury (STAR)