Dans ce mémoire, je présente une technique pour combiner du code de bas niveau à un langage purement fonctionnel avec types dépendants. Par code de bas niveau, je veux dire n’importe quel programme écrit dans un langage qui permet le contrôle direct des ressources de la machine. En particulier, ce texte s’intéresse à la gestion de la mémoire. Plus concrètement, un programmeur C contrôle l’endroit et le moment où un bloc de mémoire est alloué, ainsi que la façon dont l’objet est initialisé. Par exemple, on peut allouer de l’espace sur la pile pour immédiatement l’initialiser avec un memcpy. Alternativement, on peut allouer un bloc sur le tas et l’initialiser champ par champ plus tard. Pour certaines applications où la mémoire est limitée ou la performance importante, ce choix est important. Un tel niveau de contrôle n’est pas disponible dans les langages de haut niveau, sauf pour quelques exceptions. Les langages fonctionnels comme OCaml ou Haskell découragent ou même interdisent de modifier les champs d’un objet. C’est encore plus vrai pour les langages à types dépendants où la mutation est l’éléphant dans le magasin de porcelaine de la cohérence. C’est un choix de design intentionnel. Un programme pur est plus facile à comprendre et analyser, mais comment séparer l’initialisation de l’allocation quand un objet ne peut pas changer ? Ce mémoire essaie de démontrer que ce n’est pas parce que c’est impossible, mais parce que ces langages ne sont pas habituellement utilisés dans un contexte où c’est nécessaire. Par contre, ce n’est pas facile non plus. Pour garantir la sécurité et la cohérence, il faut modéliser l’état d’un objet partiellement initialisé au niveau des types, ce que la plupart des langages ont de la peine à faire. La combinaison du manque de nécessité et de la lourdeur syntaxique et conceptuelle est la raison pour laquelle cette fonctionnalité est souvent absente. Pour y parvenir, nous prenons un langage à types dépendants, Typer, et nous y ajoutons le nécessaire pour récupérer une partie du contrôle abandonné dans le design original. Nous permettons au programmeur d’allouer des blocs de mémoire et de les initialiser graduellement plus tard, sans compromettre les propriétés de sécurité du programme. Concrètement, nous utilisons les monades, un concept de la théorie des catégories déjà utilisé pour la modélisation d’effets de bord, pour limiter les mutations aux endroits sécuritaires. / In this thesis, I will demonstrate how to combine low-level code with dependent types. By low-level code, I mean any program authored in a language that allows direct control of computer resources. In particular, this text will focus on memory management. Specifically, a C programmer has control over the location and time when a block of memory is allocated, as well as how it is initialized. For instance, it is possible to allocate stack space to immediately initialize it with an invocation of memcpy. Alternatively, one can allocate heap spate and initialize it field by field later. For some applications where memory is constrained or performance is important, this choice can matter. This level of control is not available in high-level languages, barring a few exceptions. Functional languages such as OCaml or Haskell discourage or simply forbid the mutation of objects. This is especially the case in dependently typed languages where mutation is the bull in the china shop of consistency. This is a deliberate choice as a pure program is easier to understand and reason about. However, having allocation and initialization done in two distinct steps seems impossible in this situation. This thesis shows that this is not impossible, it is simply done this way because these kinds of languages are seldom used in a context where such control is necessary. This does not mean though that adding this feature is easy. If we are to guarantee both safety and consistency, we need to keep track of the initialization state at the type level. Most languages struggle to do this. Language designers simply forgo this feature because it is not useful to them in addition to being difficult to use. To achieve it, we start with a dependently typed language, Typer, and add back the mechanisms necessary to recover the control relinquished in the original design. We let the programmer allocate blocks of memory to initialize later, without compromising the safety properties of the program. Specifically, we use monads, a concept from category theory, a know technique to model side effects, to limit mutation to situations where it is safe.

La sécurité des applications sur le web est totalement dépendante de leur design et de la robustesse de l'implémentation des algorithmes et protocoles cryptographiques sur lesquels elles s'appuient. Cette thèse présente une nouvelle approche, applicable à de larges projets, pour vérifier l'état de l'art des algorithmes de calculs sur les grands nombres, tel que rencontrés dans les implémentations de référence. Le code et les preuves sont réalisés en F*, un langage orienté preuve et qui offre un système de types riche et expressif. L'implémentation et la vérification dans un langage d'ordre supérieur permet de maximiser le partage de code mais nuit aux performances. Nous proposons donc un nouveau langage, Low*, qui encapsule un sous ensemble de C en F* et qui compile vers C de façon sûre. Low* conserve toute l'expressivité de F* pour les spécifications et les preuves et nous l'utilisons pour implémenter de la cryptographie, en y intégrant les optimisations des implémentations de référence. Nous vérifions ce code en termes de sûreté mémoire, de correction fonctionnelle et d'indépendance des traces d'exécution vis à vis des données sensibles. Ainsi, nous présentons HACL*, une bibliothèque cryptographique autonome et entièrement vérifiée, dont les performances sont comparables sinon meilleures que celles du code C de référence. Plusieurs algorithmes de HACL* font maintenant partie de la bibliothèque NSS de Mozilla, utilisée notamment dans Firefox et dans RedHat. Nous appliquons les mêmes concepts sur miTLS, une implémentation de TLS vérifiée et montrons comment étendre cette méthodologie à des preuves cryptographiques, du parsing de message et une machine à état. / The security of Internet applications relies crucially on the secure design and robust implementations of cryptographic algorithms and protocols. This thesis presents a new, scalable and extensible approach for verifying state-of-the-art bignum algorithms, found in popular cryptographic implementations. Our code and proofs are written in F∗, a proof-oriented language which offers a very rich and expressive type system. The natural way of writing and verifying higher-order functional code in F∗ prioritizes code sharing and proof composition, but this results in low performance for cryptographic code. We propose a new language, Low∗, a fragment of F∗ which can be seen as a shallow embedding of C in F∗ and safely compiled to C code. Nonetheless, Low∗ retains the full expressiveness and verification power of the F∗ system, at the specification and proof level. We use Low∗ to implement cryptographic code, incorporating state-of-the-art optimizations from existing C libraries. We use F∗ to verify this code for functional correctness, memory safety and secret in- dependence. We present HACL∗, a full-fledged and fully verified cryptographic library which boasts performance on par, if not better, with the reference C code. Several algorithms from HACL∗ are now part of NSS, Mozilla’s cryptographic library, notably used in the Firefox web browser and the Red Hat operating system. Eventually, we apply our techniques to miTLS, a verified implementation of the Transport Layer Security protocol. We show how they extend to cryptographic proofs, state-machine implementations and message parsing verification.

This thesis aims to provide recommendations for interfacing two memory-safe programming languages, Rust and SPARK. The comparison of Rust and C/C++, as well as SPARK and C/C++, has been thoroughly researched. However, this level of investigation hasn’t been as extensive between memory-safe languages. SPARK is a subset of Ada, a programming language with a long track record in safety-critical applications. Rust is a multi-paradigm language that has gained popularity since its emergence roughly a decade ago. Both languages implement ownership systems and type safety, which are instrumental in developing safe and reliable software. Memory-safety bugs in code written in C/C++ account for about 70 % of major vulnerabilities in the industry, as reported by organizations such as Microsoft, Apple, and Google. While tools to avoid memory errors exist, code cannot be made safe retroactively, which creates a need for languages designed with safety in mind, such as Rust and SPARK. Combining those two languages is a very promising path for low-level and systems programming and safety-critical applications (automotive, avionics, medical etc.). This thesis identifies best practices for safe bindings between Rust and SPARK, focusing on ensuring memory safety, type safety, and ownership, and then analyzes how to maintain or transfer those properties. The thesis provides clear recommendations based on control study programs and a real-world example using BBQueue, a circular buffer library suitable for embedded systems implemented in both languages. The identified best practices can be used for safe bindings and automated tools/code generation. This thesis fills a gap in existing research, primarily focusing on combining safe and unsafe languages. It provides a valuable contribution to software security and safety-critical systems. / Denna avhandling syftar till att ge rekommendationer för att koppla samman två minnessäkra programmeringsspråk, Rust och SPARK. Sådana kombinationer har redan studerats utförligt mellan Rust/SPARK och de osäkra språken C/C++, men det finns relativt lite information och forskning angående minnessäkra språk. SPARK är en delmängd av Ada, ett språk som har använts i decenier i säkerhetskritiska applikationer. Rust är ett multiparadigmatiskt språk som har blivit populärt sedan dess skapande för ungefär ett decennium sedan. Båda språken implementerar ägarskapssystem och typsäkerhet, vilka är avgörande för att utveckla säkra och tillförlitliga programvaror. Minnesfel i C/C++ står för cirka 70 procent av de stora sårbarheterna i branschen, som rapporterats av organisationer såsom Microsoft, Apple och Google. Även om det finns verktyg för att undvika minnesfel kan koden inte göras säker retroaktivt, vilket skapar ett behov av språk som är designade med säkerhet i åtanke. Att kombinera Rust och SPARK är en mycket lovande väg för systemprogrammering, låg nivå och säkerhetskritiska applikationer (bilindustri, flygavionik, medicinskt etc). Denna avhandling identifierar bästa praxis för säkra bindningar mellan Rust och SPARK, med fokus på att säkerställa minnessäkerhet, typsäkerhet och ägarskap, och analyserar sedan hur man kan behålla eller överföra dessa egenskaper. Avhandlingen ger klara rekommendationer baserade på kontrollstudieprogram och ett exempel med hjälp av BBQueue, ett cirkulärt buffertbibliotek som används i inbyggda system. Dessa resulat kan användas för att skapa säkra bindningar, manuelt eller med ett automatiserat verktyg. Denna avhandling fyller en lucka i befintlig forskning, som främst fokuserar på att kombinera säkra och osäkra språk. Den bidrar värdefullt till programvarusäkerhet och säkerhetskritiska system.

Cílem této práce je vývoj dvoukanálového kontroléru krokových motorů. V rámci práce je popsán jak vývoj elektroniky, tak vývoj příslušného software. Elektronika kontrolŕu je založena na mikrokontroléru STM32F405 a driverů krokových motorů vyráběných firmou Trinamic. Pro komunikaci s nadřazenými systémy je implementován protokol CANOpen a sběrnice I\textsuperscript{2}C a USB. Elektronika byla navržena v software KiCAD and využívá čtyřvrstvého plošného spoje a moderních výrobních technologií. Co se týká software, byl vyvinut jak firmware pro mikrokontrolér, tak software pro ovládání kontroléru. Obě části software využívají programovacího jazyka Rust, který se zaměřuje na bezpečnost práce s pamětí, rychlost a zero-cost abstrakce. Sekundárním cílem této práce je ukázat, jak lze tento programovací jazyk s výhodou použít pro programování nízkoúrovňového embedded software. Firmware kontroléru implementuje nezávislé řízení pohybu obou os kontroléru a to jak v rychlostním, tak v pozičním režimu a zároveň implementuje bezpečnostní funkce pro případy selhání komunikace. Výsledný kontrolér by měl být použit v rámcí výzkumné skupiny Robotiky a Umělé Inteligence a studenty na Ústavu Automatizace FEKT VUT.