Seminars related to Épicure’s research themes:
- Épicure Seminar – internal only
- 68NQRT – http://68nqrt.irisa.fr/
- Sosysec – http://seminaire-dga.gforge.inria.fr/
Past sessions of the Épicure Seminar:
- 2024/06/20 Sérgio Medeiros “Parsing Expression Grammars: A Tour”abstractParsing Expression Grammars (PEGs), similarly to Context-Free Grammars (CFGs), is a formalism to describe languages and their associated parsers. As PEGs can not describe ambiguity, PEG-based parsers are always deterministic. In this talk, we will present an overview of PEGs, showing its distinctive features. We will also discuss some associated research questions, such as the compilation of a PEG to a program of a virtual parsing machine and how to control the backtracking of a PEG-based parser.
- 2024/05/30 Alan Schmitt “Effects in Skel: From Exceptions to Delimited Computation”abstractSkeletal Semantics is a meta-language to describe the semantics of
programming languages. We present it through several examples,
highlighting how complex features can be captured in a readable way
using monads. These features range from simple effects like exceptions
to more complex ones like generators. - 2024/05/28 Jean-Loup Hatchikian-Houdot “Faster Constant Time Secure Programs with Hardware/Software Codesign” (shared with the PACAP seminar)abstractConstant-time programming is the standard for protecting a program against attacks by auxiliary timing channels:
To prevent a potential attacker from reconstructing the software’s secrets from hardware side effects, the program is designed so that no branching or memory access depends on a secret.
In practice, this way of writing a program is intuitive and can cause significant performance degradation compared to the unprotected alternative version of the program.
We propose a slightly modified hardware and software design by allowing the software to lock specific cache-set lines to relax the constraints of constant-time programming without compromising the security it provides.
This solution is specifically intended for small embedded processors, with the goal of having hardware and software costs as low as possible (as few modifications as possible to the hardware while minimizing the performance degradation of constant-time programming).
We propose a concrete application with:
– An extension of the RISC-V ISA with new instructions to manage locks.
– A compilation chain based on CompCert to compile C programs to an ELF file in RISC-V with the lock extension.
– A simulator capable of executing these ELF files while producing an execution trace that reveals all the information potential attackers could obtain in the worst case.
– Several examples of programs protected with these locks:
– Cryptographic programs (AES, Blowfish, DES, RC4)
– Classic data manipulation programs (Table permutation, binary search, Dijkstra)
– A new constant-time sorting method that minimizes performance degradation depending on the available cache size.
Formal proofs guaranteeing the security of this mechanism will likely not be addressed during this presentation (unless there are specific questions on this topic).
- 2024/05/21 Florian Brandner “Walking on Lava : Modeling DDR Memory Controllers in Coq and Cava” abstractDDR memory is the prevalent memory technology in current computer systems, providing high performance at little cost. However, its use in critical real-time systems is challenging due to potential interference among tasks. In recent years real-time memory controllers thus have been heavily researched. The main challenges for these memory controllers are (i) managing the internal state of the memory device, (ii) respecting the many timing constraints imposed by the JEDEC standard, and (iii) predictably providing high performance. Most importantly though, theses controllers should be correct. In this talk I will summarize our recent work on modeling the DDR standard in Coq and designing a framework [1] for the development of DDR memory controllers that are correct by construction. The objective of the framework is to provide a testbed to design, prove, and evaluate generic command scheduling algorithms that form the heart of memory controllers. Since the framework aims at generic algorithm design (and not hardware design), these algorithms necessarily use features that cannot be directly implemented in hardware. We thus also explore ways to obtain actual hardware implementations that can be run in an FPGA. For this we use Cava, a domain specific language, which was heavily inspired by Lava [2], and allows to describe hardware circuits within Coq. The general idea is to prove Cava implementations equivalent to the generic Coq algorithm, considering specific constraints that reflect the limitations of hardware designs [3]. This allowed us to obtain actual synthesizeable hardware circuits that we validated against an actual memory device using the ModelSim simulator. While this approach was, in principle, successful, the use of Cava turned out to be rather painful … like walking on Lava.
- 2024/04/19 Armaël Guéneau “Melocoton: A Program Logic for Verified Interoperability Between OCaml and C” abstractIn recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI). In this talk, I will present our first steps towards the goal of eveloping program logics for multi-language verification. Specifically, I will present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of program components written in OCaml and C. Melocoton is fully mechanized in Coq on top of the Iris separation logic
framework. - 2024/04/04 Frédéric Besson “T-diagrams in Coq”
- 2024/03/29 Pierre Lermusiaux “Detection of Uncaught Exceptions in Functional Programs by Abstract Interpretation”
- 2024/03/14 Antonin Reitz “StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator” abstractDespite the rise of newer, memory-safe languages, C and C++ remain the languages of choice for the development of many safety-critical applications. While these languages allow developers to achieve high performance, they are also particularly vulnerable to memory corruption exploits; recent studies estimate that memory-related errors, e.g., buffer overflows or dangling pointers, are the root cause of 70% of the security vulnerabilities in real-world software. To mitigate these exploits, modern memory allocators often adopt a security-oriented design, which provides substantial hardening against heap corruption vulnerabilities. In this talk, we present StarMalloc, a concurrent and security-oriented allocator verified using the F* proof assistant and the separation logic-based Steel framework. After an overview of its architecture, inspired by GrapheneOS’ memory allocator, hardened_malloc, we show how to specify and verify the well-formedness of our allocator, StarMalloc, and the correctness of its security mitigations using separation logic. We finally present experimental results comparing the performance of StarMalloc to other state-of-the art allocators, using a variety of benchmarks, including several real-world applications such as the Redis key-value store and the Firefox browser.
- 2024/02/23 Raphaël Monat “Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law” abstractLegal expert systems routinely rely on date computations to determine the eligibility of a citizen to social benefits or whether an application has been filed on time. Unfortunately, date arithmetic exhibits many corner cases, which are handled differently from one library to the other, making faithfully transcribing the law into code error-prone, and possibly leading to heavy financial and legal consequences for users. In this work, we aim to provide a solid foundation for date arithmetic working on days, months and years. We first present a novel, formal semantics for date computations, and formally establish several semantic properties through a mechanization in the F⋆ proof assistant. Building upon this semantics, we then propose a static analysis by abstract interpretation to automatically detect ambiguities in date computations. We finally integrate our approach in the Catala language, a recent domain-specific language for formalizing computational law, and use it to analyze the Catala implementation of the French housing benefits, leading to the discovery of several date-related ambiguities.
- 2024/01/26 Alan Schmitt “Skeletal semantics of a fragment of Python” abstractWe present PySkel, a formalization of the semantics of a fragment of Python in Skel, a simple semantics description language. We describe a subset of the Python programming language including assignments, function calls, object oriented features, and exceptions. This subset is large enough to include challenges in the formalization of Python such as the handling of scopes. This formalization is used to generate an OCaml interpreter that can be used to run Python programs.
- 2024/01/09 Clément Chavanon “PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams” abstractWe present PfComp, a verified compiler for stateless firewall policies. The policy is first compiled into an intermediate representation taking the form of a binary decision diagram that is optimised in terms of decision nodes. The decision diagram is then compiled into a Clight program. The compiler is proved correct using the Coq proof assistant and extracted into OCaml code. Our preliminary experiments show promising results. The compiler generates code for relatively large firewall policies and the generated code out-performs a sequential evaluation of the policy rules.
- 2023/12/13 Anshuman Mohan (Cornell University) “Formal Abstractions for Packet Scheduling” abstractIn software-defined networking, PIFO trees are a promising mechanism for realizing programmable packet scheduling in hardware. We formalize the syntax and semantics of PIFO trees in an operational model that decouples the scheduling policy running on a tree from the topology of the tree. We develop compilation algorithms that allow the behavior of a tree to be realized using another tree having a different topology. This is exciting because it enables real hardware adoption: switch manufacturers can provision their devices with a single tree, and yet allow network administrators to program their schedulers against a range of tree topologies. This work was presented at OOPSLA’23, where it won a Distinguished Paper Award.
- 2023/12/12 Lesly-Ann Daniel (KU Leuven) “Beyond constant-time programming: Hardware-software co-designs for microarchitectural security” abstractMicroarchitectural optimizations, such as caches, or speculative out-of-order execution, play a crucial role for enhancing system performance. However, these optimizations also enable attacks that undermine software-enforced security policies. The conventional approach of constant-time programming, while widely adopted for safeguarding cryptographic implementations against microarchitectural attacks, has its limitations. From a security perspective, it relies on certain assumptions about the underlying hardware and, for instance, does not suffice to protect against Spectre attacks. In terms of performance, it imposes an additional overhead due to, among other things, control-flow linearization.
In this presentation, we introduce two novel hardware-software co-design solutions to address some of the shortcomings of constant-time programming. First, we present ProSpeCT, a generic formal processor model that guarantees that constant-time programs (under a non-speculative semantics) are free from Spectre attacks, while still enabling speculative out-of-order execution. Second, Architectural Mimicry, a novel ISA extension that provides dedicated hardware support for efficient control-flow balancing and linearization of secret-dependent branches. Both defenses have been implemented and evaluated on top of Proteus, an extensible RISC-V processor. To conclude, we will discuss some of the remaining challenges that still need to be addressed to achieve provable end-to-end security guarantees. - 2023/11/21 Tony Law “Synthèse de haut-niveau formellement vérifiée de circuits élastiques” abstractTraditionnellement, le développement pour FPGA se réalise avec des outils propres au développement matériel, souvent distincts de ceux du développement logiciel. La synthèse de haut-niveau (HLS) fait le lien entre ces deux mondes, et consiste à compiler une spécification haut niveau vers un langage de description de matériel (HDL) pour accélérer la conception de circuits.Nous souhaitons ajouter un nouveau backend au compilateur vérifié CompCert. Celui-ci générera des circuits élastiques, un HDL utilisé par le compilateur HLS Dynamatic. En plus d’être prouvé correct en Coq, il devra aussi produire des circuits capables d’exploiter le parallélisme inhérent au matériel.Cet exposé sera une présentation haut-niveau du projet, de son état actuel, et expliquera les problématiques identifiées ainsi que les méthodes et représentations intermédiaires envisagées pour y répondre.
- 2023/11/07 Frédéric Besson “Compilation et sécurité” abstractTalk targeted to a general audience, that was given last year at FIC l’an dernier
