Charon: An Analysis Framework for Rust

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 mac...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-10
Main Authors: Ho, Son, Boisseau, Guillaume, Lucas Franceschino, Prak, Yoann, Fromherz, Aymeric, Protzenko, Jonathan
Format: Article
Language:English
Subjects:
Charon
Compilers
Programming languages
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422