Charon: An Analysis Framework for Rust

TL;DR

Charon is a comprehensive analysis framework for Rust that simplifies access to a stable AST, enabling diverse analysis tools and demonstrating its utility through multiple case studies including verification, compilation, and security analysis.

Contribution

It introduces Charon, a unified framework that provides a stable AST for Rust, easing the development of analysis tools and reducing redundant effort across the ecosystem.

Findings

Charon enables diverse Rust analyses with a stable AST.

Re-implementation of Rudra analysis demonstrates Charon's versatility.

Case studies show Charon's effectiveness in verification, compilation, and security.

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