Publications de Clément Pit-Claudel

Publications associées (9)

Foundational Integration Verification of a Cryptographic Server

We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve crypto ...

2024

Specification and Verification of Strong Timing Isolation of Hardware Enclaves

Clément Pit-Claudel, Thomas Emile Bourgeat

The process isolation enforceable by commodity hardware and operating systems is too weak to protect secrets from malicious code running on the same machine: attacks exploit timing side channels derived from contention on shared microarchitectural resource ...

Association for Computing Machinery, Inc2024

Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types

Mathias Josef Payer, Clément Pit-Claudel

Modern software needs fine-grained compartmentalization, i.e., intra-process isolation. A particularly important reason for it are supply-chain attacks, the need for which is aggravated by modern applications depending on hundreds or even thousands of libr ...

ASSOC COMPUTING MACHINERY2024

A Conjecture Regarding SMT Instability

George Candea, Clément Pit-Claudel, Can Cebeci

Automated verifiers rely on SMT solvers as a backend for proof automation. This simplifies verification in the common case, but also creates usability challenges due to instability. Previous work proposes mitigation strategies motivated by the assumption t ...

CEUR-WS2025

Linear Matching of JavaScript Regular Expressions

Clément Pit-Claudel, Aurèle Aimé Aubin Barrière

Modern regex languages have strayed far from well-understood traditional regular expressions: They include features that fundamentally transform the matching problem. In exchange for these features, modern regex engines at times suffer from exponential com ...

2024

Practical Verification of System-Software Components Written in Standard C

Yonghao Zou, George Candea, Clément Pit-Claudel, Diyu Zhou, Can Cebeci

Systems code is challenging to verify, because it uses constructs (like raw pointers, pointer arithmetic, and bit twiddling) that are hard for tools to reason about. Existing approaches either sacrifice programmer friendliness, by demanding significant man ...

Association for Computing Machinery, Inc2024

Lessons learned from the first edition of a large second-year course in software construction

Clément Pit-Claudel, Shardul Aniruddha Chiplunkar

This paper lays out a case study of Software Construction, a new course in the undergraduate computer and communication sciences curriculum at EPFL. We hope to share some generalizable lessons we learned from running its first edition in Fall 2023. The cou ...

EPFL2024

A Coq Mechanization of JavaScript Regular Expression Semantics

Noé Eric De Santo, Clément Pit-Claudel, Aurèle Aimé Aubin Barrière

We present an executable, proven-safe, faithful, and future-proof Coq mechanization of JavaScript regular expression (regex) matching, as specified by the latest published edition of ECMA-262 section 22.2. This is, to our knowledge, the first time that an ...

2024

Diagrammatic notations for interactive theorem proving

Clément Pit-Claudel, Shardul Aniruddha Chiplunkar

Diagrams are ubiquitous in the development and presentation of proofs, yet surprisingly uncommon in computerized mathematics. Instead, authors and developers rely almost exclusively on line-oriented notations (textual abbreviations and symbols). How might ...

EPFL2023