2021/11/30 by Will Crichton, Marco Patrignani, Maneesh Agrawala +1
Computer Science · Mathematics · #Advanced Malware Detection Techniques #Computer science #Control flow #Data flow diagram #Database #Distributed systems and fault tolerance #Flow (mathematics) #Function (biology) #Information flow #Mathematics #Modular design #Programming language #Rust (programming language) #Security and Verification in Computing #Signature (topology) #Soundness #Task (project management) #Theoretical computer science #cs.PL
paper · pdf · doi:10.1145/3519939.3523445
Published at PLDI 2022
arxiv created 2022/03/15 · arxiv updated 2022/03/17 · openalex publication_date 2022/06/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
Statically analyzing information flow, or how data influences other data within a program, is a challenging task in imperative languages. Analyzing pointers and mutations requires access to a program's complete source. However, programs often use pre-compiled dependencies where only type signatures are available. We demonstrate that ownership types can be used to soundly and precisely analyze information flow through function calls given only their type signature. From this insight, we built Flowistry, a system for analyzing information flow in Rust, an ownership-based language. We prove the system's soundness as a form of noninterference using the Oxide formal model of Rust. Then we empirically evaluate the precision of Flowistry, showing that modular flows are identical to whole-program flows in 94% of cases drawn from large Rust codebases. We illustrate the applicability of Flowistry by using it to implement prototypes of a program slicer and an information flow control system.