-
Charon: An Analysis Framework for Rust
Authors:
Son Ho,
Guillaume Boisseau,
Lucas Franceschino,
Yoann Prak,
Aymeric Fromherz,
Jonathan Protzenko
Abstract:
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 ecosystem remains relatively young, meaning that every one of these tools has had to re-implement difficult, time-consuming machinery to interface with the Rust compiler and its cargo build system, to hook into the Rust compile…
▽ More
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 ecosystem remains relatively young, meaning that every one of these tools has had to re-implement difficult, time-consuming machinery to interface with the Rust compiler and its cargo build system, to hook into the Rust compiler's internal representation, and to expose an abstract syntax tree (AST) that is suitable for analysis rather than optimized for efficiency. We address this missing building block of the Rust ecosystem, and propose Charon, an analysis framework for Rust. Charon acts as a swiss-army knife for analyzing Rust programs, and deals with all of the tedium above, providing clients with a clean, stable AST that can serve as the foundation of many analyses. We demonstrate the usefulness of Charon through a series of case studies, ranging from a Rust verification framework (Aeneas), a compiler from Rust to C (Eurydice), and a novel taint-checker for cryptographic code. To drive the point home, we also re-implement a popular existing analysis (Rudra), and show that it can be replicated by leveraging the Charon framework.
△ Less
Submitted 30 May, 2025; v1 submitted 23 October, 2024;
originally announced October 2024.
-
Verified Functional Programming of an Abstract Interpreter
Authors:
Lucas Franceschino,
David Pichardie,
Jean-Pierre Talpin
Abstract:
Abstract interpreters are complex pieces of software: even if the abstract interpretation theory and companion algorithms are well understood, their implementations are subject to bugs, that might question the soundness of their computations.
While some formally verified abstract interpreters have been written in the past, writing and understanding them requires expertise in the use of proof ass…
▽ More
Abstract interpreters are complex pieces of software: even if the abstract interpretation theory and companion algorithms are well understood, their implementations are subject to bugs, that might question the soundness of their computations.
While some formally verified abstract interpreters have been written in the past, writing and understanding them requires expertise in the use of proof assistants, and requires a non-trivial amount of interactive proofs.
This paper presents a formally verified abstract interpreter fully programmed and proved correct in the F* verified programming environment. Thanks to F* refinement types and SMT prover capabilities we demonstrate a substantial saving in proof effort compared to previous works based on interactive proof assistants.
Almost all the code of our implementation, proofs included, written in a functional style, are presented directly in the paper.
△ Less
Submitted 17 October, 2021; v1 submitted 20 July, 2021;
originally announced July 2021.
-
LIO*: Low Level Information Flow Control in F*
Authors:
Jean-Joseph Marty,
Lucas Franceschino,
Jean-Pierre Talpin,
Niki Vazou
Abstract:
We present Labeled Input Output in F* (LIO*), a verified framework that enforces information flow control (IFC) policies developed in F* and automatically extracted to C. Inspired by LIO, we encapsulated IFC policies into effects, but using F* we derived efficient, low level, and provably correct code. Concretely, runtime checks are lifted to static proof obligations, the developed code is automat…
▽ More
We present Labeled Input Output in F* (LIO*), a verified framework that enforces information flow control (IFC) policies developed in F* and automatically extracted to C. Inspired by LIO, we encapsulated IFC policies into effects, but using F* we derived efficient, low level, and provably correct code. Concretely, runtime checks are lifted to static proof obligations, the developed code is automatically extracted to C and proved non-interferent using metaprogramming. We benchmarked our framework on three clients and observed up to 54% speedup when IFC runtime checks are proved statically. Our framework is designed to aid development of embedded devices where both enforcement of security policies and low level efficient code is critical.
△ Less
Submitted 27 April, 2020;
originally announced April 2020.
