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.

Modular Information Flow Through Ownership / Crichton, Will; Patrignani, Marco; Agrawala, Maneesh; Hanrahan, Pat. - (2022), pp. 1-14. (Intervento presentato al convegno PLDI tenutosi a San Diego nel 13 - 17 June 2022) [10.1145/3519939.3523445].

Modular Information Flow Through Ownership

Patrignani, Marco;
2022-01-01

Abstract

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.
2022
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
San Diego, CA
ACM
978-1-4503-9265-5
Crichton, Will; Patrignani, Marco; Agrawala, Maneesh; Hanrahan, Pat
Modular Information Flow Through Ownership / Crichton, Will; Patrignani, Marco; Agrawala, Maneesh; Hanrahan, Pat. - (2022), pp. 1-14. (Intervento presentato al convegno PLDI tenutosi a San Diego nel 13 - 17 June 2022) [10.1145/3519939.3523445].
File in questo prodotto:
File Dimensione Formato  
PLDI_2022___Modular_Information_Flow_through_Ownership.pdf

Solo gestori archivio

Descrizione: first online
Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 1.32 MB
Formato Adobe PDF
1.32 MB Adobe PDF   Visualizza/Apri
3519939.3523445.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 552.38 kB
Formato Adobe PDF
552.38 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/341573
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact