112 citations · 279 across the 12 of their papers we have counts for
16 papers
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
Son Ho, Cédric Fournet, Jonathan Protzenko +7
We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification conven…
Scylla: Translating an Applicative Subset of C to Safe Rust
Aymeric Fromherz, Jonathan Protzenko
The popularity of the Rust language continues to explode; yet, many critical codebases remain authored in C. Automatically translating C to Rust is thus an appealing course of acti…
Charon: An Analysis Framework for Rust
Son Ho, Guillaume Boisseau, Lucas Franceschino +3
With the explosion in popularity of the Rust programming language, a wealth of tools have recently been developed to analyze, verify, and test Rust programs. Alas, the Rust ecosyst…
Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version)
Son Ho, Aymeric Fromherz, Jonathan Protzenko
The Rust programming language continues to rise in popularity, and as such, warrants the close attention of the programming languages community. In this work, we present a new foun…
StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko
In this work, we present StarMalloc, a verified, security-oriented, concurrent memory allocator that can be used as a drop-in replacement in real-world projects. Using the Steel se…
Aeneas: Rust Verification by Functional Translation
Son Ho, Jonathan Protzenko
We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust's rich region-based type system to eliminate memor…
Catala: A Programming Language for the Law
Denis Merigoux, Nicolas Chataing, Jonathan Protzenko
Law at large underpins modern society, codifying and governing many aspects of citizens' daily lives. Oftentimes, law is subject to interpretation, debate and challenges throughout…
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
Son Ho, Aymeric Fromherz, Jonathan Protzenko
For all the successes in verifying low-level, efficient, security-critical code, little has been said or studied about the structure, architecture and engineering of such large-sca…
A Modern Compiler for the French Tax Code
Denis Merigoux, Raphaël Monat, Jonathan Protzenko
In France, income tax is computed from taxpayers' individual returns, using an algorithm that is authored, designed and maintained by the French Public Finances Directorate (DGFiP)…
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Guido Martínez, Danel Ahman, Victor Dumitrescu +10
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to dischar…
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm, Kenji Maillard, Cédric Fournet +7
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diver…
Verified Low-Level Programming Embedded in F*
Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi +8
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a sm…
Dijkstra Monads for Free
Danel Ahman, Catalin Hritcu, Kenji Maillard +5
Dijkstra monads enable a dependent type theory to be enhanced with support for specifying and verifying effectful code via weakest preconditions. Together with their closely relate…
The ins and outs of iteration in Mezzo
Armaël Guéneau, François Pottier, Jonathan Protzenko
This is a talk proposal for HOPE 2013. Using iteration over a collection as a case study, we wish to illustrate the strengths and weaknesses of the prototype programming language M…
Programming with Permissions in Mezzo
Jonathan Protzenko, François Pottier
We present Mezzo, a typed programming language of ML lineage. Mezzo is equipped with a novel static discipline of duplicable and affine permissions, which controls aliasing and own…
Illustrating the Mezzo programming language
Jonathan Protzenko
When programmers want to prove strong program invariants, they are usually faced with a choice between using theorem provers and using traditional programming languages. The former…