Thibault Dardinier
PhD student, Programming Methodology Group, ETH Zurichthibault.dardinier[at]inf.ethz.ch
About Publications Education Experience Awards Teaching Supervision Other
About
I am a PhD student in the Programming Methodology Group at ETH Zurich, supervised by Prof. Peter Müller. My goal is to develop formal foundations (using the Isabelle proof assistant) for automatic deductive verifiers based on separation logic, with a particular focus on intermediate verification languages (such as Viper).
Before this, I graduated from ETH Zurich (as part of the Direct Doctorate program) and from École Polytechnique in France. During my studies, I completed internships at SRI International, Siemens, and the Ministry of Defense (France).
Publications
Preprints
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
Marco Eilers, Thibault Dardinier, Peter MüllerAbstract arXiv
Information flow security ensures that the secret data manipulated by a program does not influence its observable output. Proving information flow security is especially challenging for concurrent programs, where operations on secret data may influence the execution time of a thread and, thereby, the interleaving between different threads. Such internal timing channels may affect the observable outcome of a program even if an attacker does not observe execution times. Existing verification techniques for information flow security in concurrent programs attempt to prove that secret data does not influence the relative timing of threads. However, these techniques are often restrictive (for instance because they disallow branching on secret data) and make strong assumptions about the execution platform (ignoring caching, processor instructions with data-dependent runtime, and other common features that affect execution time). In this paper, we present a novel verification technique for secure information flow in concurrent programs that lifts these restrictions and does not make any assumptions about timing behavior. The key idea is to prove that all mutating operations performed on shared data commute, such that different thread interleavings do not influence its final value. Crucially, commutativity is required only for an abstraction of the shared data that contains the information that will be leaked to a public output. Abstract commutativity is satisfied by many more operations than standard commutativity, which makes our technique widely applicable. We formalize our technique in CommCSL, a relational concurrent separation logic with support for commutativity-based reasoning, and prove its soundness in Isabelle/HOL. We implemented CommCSL in HyperViper, an automated verifier based on the Viper verification infrastructure, and demonstrate its ability to verify challenging examples.
Verification-Preserving Inlining in Automatic Separation Logic Verifiers
Thibault Dardinier, Gaurav Parthasarathy, Peter MüllerAbstract arXiv
Bounded verification has proved useful to detect bugs and to increase confidence in the correctness of a program. In contrast to unbounded verification, reasoning about calls via (bounded) inlining and about loops via (bounded) unrolling does not require method specifications and loop invariants and, therefore, reduces the annotation overhead to the bare minimum, namely specifications of the properties to be verified. For verifiers based on traditional program logics, verification via inlining (and unrolling) is verification-preserving: successful unbounded verification of a program w.r.t. some annotation implies successful verification of the inlined program. That is, any error detected in the inlined program reveals a true error in the original program. However, this essential property might not hold for automatic separation logic verifiers such as Caper, GRASShopper, RefinedC, Steel, VeriFast, and verifiers based on Viper. In this setting, inlining generally changes the resources owned by method executions, which may affect automatic proof search algorithms and introduce spurious errors. In this paper, we present the first technique for verification-preserving inlining in automatic separation logic verifiers. We identify a semantic condition on programs and prove in Isabelle/HOL that it ensures verification-preserving inlining for state-of-the-art automatic separation logic verifiers. We also prove a dual result: successful verification of the inlined program ensures that there are method and loop annotations that enable the verification of the original program for bounded executions. To check our semantic condition automatically, we present two approximations that can be checked syntactically and with a program verifier, respectively. We implemented these checks in Viper and demonstrate that they are effective for non-trivial examples from different verifiers.
Conference
OOPSLA
Fractional Resources in Unbounded Separation Logic
Thibault Dardinier, Peter Müller, Alexander J. SummersObject-Oriented Programming Systems, Languages, and Applications (OOPSLA), Proc. ACM Program. Lang.
Abstract Link PDF Isabelle formalization
Many separation logics support fractional permissions to distinguish between read and write access to a heap location, for instance, to allow concurrent reads while enforcing exclusive writes. Fractional permissions extend to composite assertions such as (co)inductive predicates and magic wands by allowing those to be multiplied by a fraction. Typical separation logic proofs require that this multiplication has three key properties: it needs to distribute over assertions, it should permit fractions to be factored out from assertions, and two fractions of the same assertion should be combinable into one larger fraction. Existing formal semantics incorporating fractional assertions into a separation logic define multiplication semantically (via models), resulting in a semantics in which distributivity and combinability do not hold for key resource assertions such as magic wands, and fractions cannot be factored out from a separating conjunction. By contrast, existing automatic separation logic verifiers define multiplication syntactically, resulting in a different semantics for which it is unknown whether distributivity and combinability hold for all assertions. In this paper, we present a novel semantics for separation logic assertions that allows states to hold more than a full permission to a heap location during the evaluation of an assertion. By reimposing upper bounds on the permissions held per location at statement boundaries, we retain key properties of separation logic, in particular, the frame rule. Our assertion semantics unifies semantic and syntactic multiplication and thereby reconciles the discrepancy between separation logic theory and tools and enjoys distributivity, factorisability, and combinability. We have formalised our semantics and proved its properties in Isabelle/HOL.
ICTAC
VeriMon: A Formally Verified Monitoring Tool (invited)
David Basin, Thibault Dardinier, Nico Hauser, Lukas Heimes, Jonathan Julián Huerta y Munive, Nicolas Kaletsch, Srđan Krstić, Emanuele Marsicano, Martin Raszyk, Joshua Schneider, Dawit Legesse Tirore, Dmitriy Traytel, Sheila ZinggInternational Colloquium on Theoretical Aspects of Computing (ICTAC)
Abstract Link
A runtime monitor observes a running system and checks whether the sequence of events the system generates satisfies a given specification. We describe the evolution of VeriMon: an expressive and efficient monitor that has been formally verified using the Isabelle proof assistant.
CAV
Sound Automation of Magic Wands
Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller, Alexander J. SummersComputer Aided Verification (CAV)
Abstract Link Extended version Slides Isabelle formalization (part 1) (part 2) Artifact
The magic wand −∗ (also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A footprint of a magic wand formula is a state that, combined with any state in which A holds, yields a state in which B holds. The key challenge of proving a magic wand (also called packaging a wand) is to find such a footprint. Existing package algorithms either have a high annotation overhead or, as we show in this paper, are unsound. We present a formal framework that precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics. We prove in Isabelle/HOL that our formal framework is sound and complete, and use it to develop a novel package algorithm that offers competitive automation and is sound. Moreover, we present a novel, restricted definition of wands and prove in Isabelle/HOL that it is possible to soundly combine fractions of such wands, which is not the case for arbitrary wands. We have implemented our techniques for the Viper language, and demonstrate that they are effective in practice.
IJCAR
A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic
David Basin, Thibault Dardinier, Lukas Heimes, Srđan Krstić, Martin Raszyk, Joshua Schneider, Dmitriy TraytelInternational Joint Conference on Automated Reasoning (IJCAR)
Abstract Link Isabelle formalization
Runtime monitors for rich specification languages are sophisticated algorithms, especially when they are heavily optimized. To gain trust in them and safely explore the space of possible optimizations, it is important to verify the monitors themselves. We describe the development and correctness proof in Isabelle/HOL of a monitor for metric first-order dynamic logic. This monitor significantly extends previous work on formally verified monitors by supporting aggregations, regular expressions (the dynamic part), and optimizations including multi-way joins adopted from databases and a new sliding window algorithm.
GECCO
A new analysis method for evolutionary optimization of dynamic and noisy objective functions
Raphaël Dang-Nhu, Thibault Dardinier, Benjamin Doerr, Gautier Izacard, Dorian NognengGenetic and Evolutionary Computation Conference (GECCO)
Abstract Link
Evolutionary algorithms, being problem-independent and randomized heuristics, are generally believed to be robust to dynamic changes and noisy access to the problem instance. We propose a new method to obtain rigorous runtime results for such settings. In contrast to many previous works, our new approach mostly relies on general parameters of the dynamics or the noise models, such as the expected change of the dynamic optimum or the probability to have a dynamic change in one iteration. Consequently, we obtain bounds which are valid for large varieties of such models. Despite this generality, for almost all particular models regarded in the past our bounds are stronger than those given in previous works. As one particular result, we prove that the (1 + λ) EA can optimize the OneMax benchmark function efficiently despite a constant rate of 1-bit flip noise. For this, a logarithmic size offspring population suffices (the previous-best result required a super-linear value of λ). Our results suggest that the typical way to find the optimum in such adverse settings is not via a steady approach of the optimum, but rather via an exceptionally fast approach after waiting for a rare phase of low dynamic changes or noise.
Master's Thesis
Beyond the Frame Rule: Static Inlining in Separation Logic
Thibault DardinierMaster's Thesis. ETH Zurich, Switzerland.
Abstract Link
Various formal verification techniques can be used to automatically verify the absence of errors in programs. This provides an advantage over testing approaches, namely the guarantee that a program is correct for any possible execution. However, such approaches often require a user to provide additional specifications to guide the verification, in the form of loop invariants and method preconditions and postconditions, which places a burden on the user. When no specifications are provided, verifiers usually report potential errors which are not actual errors, hence lowering confidence in error reporting. Users might want to learn quickly (without providing too many specifications) and with high confidence whether a program is incorrect. This would speed up the development and verification process by only having to provide specifications when one is fairly certain that the program is correct. Static inlining, that is inlining of method calls and unrolling of loop iterations, is an interesting approach to tackle this issue. Using approaches based on static inlining, verifiers could inform a user of the existence of fundamental errors, errors for which no annotation can make the program verify. The existence of fundamental errors indicates an error in the program itself, informing the user this program cannot be verified, without the user needing to waste time and energy in the search of the right annotation. One would expect that errors reported in an inlined program always correspond to fundamental errors in the original program, since annotations only serve as approximations of method calls and loops. Surprisingly, this is not always the case. Indeed, Viper, a verification infrastructure for permissionbased reasoning, partly based on separation logic and implicit dynamic frames with fractional permissions, has special features (such as permission introspection) which give rise to examples where this is not the case. These examples have all in common that they do not satisfy the frame rule. In this thesis, we find (and prove correct) a soundness condition which characterizes the set of Viper programs for which static inlining is sound, that is errors in the inlined program correspond to fundamental errors in the original program. We define a parametric language which generalizes Viper, where program states are elements of a separation algebra, define the soundness condition in terms of this language, and prove the soundness property of inlining under this soundness condition, using the proof assistant Isabelle/HOL. We then show how one can instantiate this parametric language to transfer the results to Viper. We also explore a completeness property of static inlining, and consider extensions to different loop semantics and different ways of inlining.
Education
PhD Student, ETH Zurich
Zurich, Switzerland Part of the Direct Doctorate program.Master of Computer Science with distinction, ETH Zurich, 5.8/6
Zurich, SwitzerlandDiplôme d'Ingénieur (MSc), École Polytechnique, 3.96/4 (top 5%)
Palaiseau, FranceClasses Préparatoires (MPSI-MP), Lycée du Parc
Lyon, FranceExperience
Static Inlining in Separation Logic, ETH Zurich (Programming Methodology Group)
Master's Thesis Supervision: Gaurav Parthasarathy, Prof. Peter Müller- Exploration of static inlining in non-monotonic separation logic to detect program errors early (without annotations), applied to the intermediate verification language Viper.
- Received the ETH Medal.
- See the thesis.
Formalizing Multiway-Join Algorithms in Isabelle/HOL, ETH Zurich (Information Security Group)
Direct doctorate research project Supervision: Dr. Dmitriy Traytel, Martin RaszykResearch Fellow, SRI International (CSL)
Menlo Park, California, USASupervision: Dr. Susmit Jha
Theoretical Analysis of Evolutionary Algorithms, École Polytechnique (LIX)
Supervision: Prof. Benjamin DoerrR&D Intern, Siemens (Corporate Technology)
Munich, GermanyResearch Intern, Ministry of Defense (France)
Paris, FranceAwards
Best Overall Team, VerifyThis (Program Verification Competition)
with Jonás Fiala- VerifyThis is a program verification competition, whose 2022 edition took place at ETAPS 2022 in Munich.
- It offers several challenges presented in natural language and pseudo code. Participants have to formalize the requirements, implement a solution, and formally verify the implementation for adherence to the specification.
- Our team won the "Best Overall Team" prize using Viper.
ETH Medal, ETH Zurich
Awarded by ETH Zürich for my Master's thesis on inlining in separation logic, along with a financial sum. The ETH Medal is awarded to less than 2.5% of all Master's graduates of an ETH department.Research Internship Prize, École Polytechnique
Awarded by École Polytechnique for my work on Gaussian Processes at SRI International.National Defense Medal (France)
Awarded for my internship at the Ministry of Defense.3rd Place, Prologin (National Programming Contest)
Prologin is a contest for French speaking students under 21, with qualifiers. The best 100 candidates meet and discover a multiplayer game created for the contest. They have 36 hours in a row to create an AI for the game. A ranking is established with the results of a contest between all AIs. Ranked 3rd.2nd Place, Prologin (National Programming Contest)
Ranked 2nd.Teaching
Teaching Assistant, ETH Zurich
Zurich, Switzerland- Concepts of Object-Oriented Programming (2020, 2021, 2022)
- Formal Methods and Functional Programming (head teaching assistant, 2021, 2022)
Oral Examiner in Mathematics, Lycée Blaise Pascal
Orsay, FranceTwo hours weekly for undergraduates preparing competitive entrance exams to France’s top-ranking scientific schools.
Supervision
- Ellen Arlt, MSc thesis (co-supervised with Gaurav Parthasarathy)
A Formally Verified Automatic Verifier for Concurrent Programs - Anqi Li, MSc practical work project
Improving User-Defined Permission Models in Viper - Todor Hristov, MSc practical work project
Improving the Support for Magic Wands in Viper - Dina Weiersmüller, BSc thesis (co-supervised with Linard Arquint)
Advanced Logical Proofs in a Verifier - Matthias Schenk, BSc thesis
Practical Inlining in Viper
- Nicola Widmer, BSc thesis (co-supervised with Malte Schwerhoff)
Sound Automation of Magic Wands in a Symbolic-Execution Verifier - Matthias Roshardt, MSc thesis
Extending the Viper Verification Language with User-Defined Permission Models - Noé Weeks, BSc internship (co-supervised with Gaurav Parthasarathy)
Making Magic Wands Combinable - Benjamin Bonneau, MSc internship (co-supervised with Gaurav Parthasarathy)
A Formal Foundation for the Dafny Verifier - Yanick Bachmann, BSc thesis
An Abstract Representation for Wildcard Permissions in Viper
Other Activities
Development of an Online Video Platform for the Video Association (JTX)
Development of an Optimization Algorithm (Bin Packing) for Industrial Purposes
Volunteer, Mission Potosi
Potosi, BoliviaMission Potosi is an organisation with about 50 students from 4 schools (business, medical and engineering), which collaborates with local ONGs (Cepromin, Pasocap) and a german ONG (Kindernothilfe) in Potosi (Bolivia) to provide childcare for mining families.
Military Training as an Officer
Coëtquidan, FranceThis military training, part of the cursus at École polytechnique, teaches us a lot on various subjects such as strategy, communication, leadership, etc.