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 implementing both a program slicer and an IFC checker on top of it.
Wed 15 JunDisplayed time zone: Pacific Time (US & Canada) change
10:40 - 12:00 | |||
10:40 20mTalk | P4BID: Information Flow Control in P4 PLDI DOI | ||
11:00 20mTalk | ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification PLDI Sankha Narayan Guria University of Maryland, College Park, Niki Vazou IMDEA Software Institute, Marco Guarnieri IMDEA Software Institute, James Parker Galois, Inc. DOI Pre-print | ||
11:20 20mTalk | Hardening Attack Surfaces with Formally Proven Binary Format Parsers PLDI Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Irina Spiridonova Microsoft Research, Haobin Ni Cornell University, Dmitry Malloy Microsoft, Juan Vazquez Microsoft, Michael Tang Microsoft, Omar Cardona Microsoft, Arti Gupta Microsoft DOI | ||
11:40 20mTalk | Modular Information Flow Through Ownership PLDI Will Crichton Stanford University, Marco Patrignani University of Trento, Maneesh Agrawala Stanford University, Pat Hanrahan Stanford University, USA DOI Pre-print | ||
22:40 - 00:00 | |||
22:40 20mTalk | P4BID: Information Flow Control in P4 PLDI DOI | ||
23:00 20mTalk | ANOSY: Approximated Knowledge Synthesis with Refinement Types for Declassification PLDI Sankha Narayan Guria University of Maryland, College Park, Niki Vazou IMDEA Software Institute, Marco Guarnieri IMDEA Software Institute, James Parker Galois, Inc. DOI Pre-print | ||
23:20 20mTalk | Hardening Attack Surfaces with Formally Proven Binary Format Parsers PLDI Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Irina Spiridonova Microsoft Research, Haobin Ni Cornell University, Dmitry Malloy Microsoft, Juan Vazquez Microsoft, Michael Tang Microsoft, Omar Cardona Microsoft, Arti Gupta Microsoft DOI | ||
23:40 20mTalk | Modular Information Flow Through Ownership PLDI Will Crichton Stanford University, Marco Patrignani University of Trento, Maneesh Agrawala Stanford University, Pat Hanrahan Stanford University, USA DOI Pre-print | ||