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 90% 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.
翻译:对信息流或数据如何影响程序内的其他数据进行统计分析是一项艰巨的任务。分析指针和突变需要访问程序的完整源头。 但是,程序通常使用事先整合的相互依存关系,只有类型签名。 我们证明所有制类型可以用于正确和精确地分析通过仅给予其类型签名的功能电话进行的信息流动。 从这个洞察力,我们建立了花流,这是用所有制语言Rust来分析信息流动的系统。我们证明,该系统的健全性是一种不干预形式,使用Oxide正式的Rust模式。 然后,我们用经验来评估花流的精确性,表明在大型 Rust 代码库中抽取的90%的案例中,模块流与全程序流是相同的。 我们通过在它上面执行一个程序切片和一个IFC检查器来说明花流的可适用性。