More Web Proxy on the site http://driver.im/

research-article

Modular information flow through ownership

Authors:

Marco Patrignani,

Maneesh Agrawala,

Pat HanrahanAuthors Info & Claims

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 1 - 14

https://doi.org/10.1145/3519939.3523445

Published: 09 June 2022 Publication History

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.

Supplementary Material

Auxiliary Archive (pldi22main-p150-p-archive.zip)

This is the appendix for the paper "Modular Information Flow through Ownership" (Crichton et al.) at PLDI 2022. It contains additional rules and proofs for theorems in the paper, and details about the evaluation.

Download
3.42 MB

References

[1]

Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. 1999. A Core Calculus of Dependency. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’99). Association for Computing Machinery, New York, NY, USA. 147–160. isbn:1581130953 https://doi.org/10.1145/292540.292555

Digital Library

[2]

Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, and Alexander J. Summers. 2020. How Do Programmers Use Unsafe Rust? Proc. ACM Program. Lang., 4, OOPSLA (2020), Article 136, nov, 27 pages. https://doi.org/10.1145/3428204

Digital Library

[3]

Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers. 2019. Leveraging Rust Types for Modular Specification and Verification. Proc. ACM Program. Lang., 3, OOPSLA (2019), Article 147, oct, 30 pages. https://doi.org/10.1145/3360573

Digital Library

[4]

Thomas H. Austin and Cormac Flanagan. 2009. Efficient Purely-Dynamic Information Flow Analysis. In Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security (PLAS ’09). Association for Computing Machinery, New York, NY, USA. 113–124. isbn:9781605586458 https://doi.org/10.1145/1554339.1554353

Digital Library

[5]

Abhiram Balasubramanian, Marek S. Baranowski, Anton Burtsev, Aurojit Panda, Zvonimir Rakamarić, and Leonid Ryzhyk. 2017. System Programming in Rust: Beyond Safety. In Proceedings of the 16th Workshop on Hot Topics in Operating Systems (HotOS ’17). Association for Computing Machinery, New York, NY, USA. 156–161. isbn:9781450350686 https://doi.org/10.1145/3102980.3103006

Digital Library

[6]

Pablo Buiras, Dimitrios Vytiniotis, and Alejandro Russo. 2015. HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015). Association for Computing Machinery, New York, NY, USA. 289–301. isbn:9781450336697 https://doi.org/10.1145/2784731.2784758

Digital Library

[7]

Marek Chalupa. 2016. Slicing of LLVM bitcode. Master’s thesis. Masaryk University.

[8]

David G. Clarke, John M. Potter, and James Noble. 1998. Ownership Types for Flexible Alias Protection. In Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA ’98). Association for Computing Machinery, New York, NY, USA. 48–64. isbn:1581130058 https://doi.org/10.1145/286936.286947

Digital Library

[9]

Keith D Cooper, Timothy J Harvey, and Ken Kennedy. 2001. A simple, fast dominance algorithm. Software Practice & Experience, 4, 1-10 (2001), 1–8.

[10]

Patrick Cousot and Radhia Cousot. 2002. Modular Static Program Analysis. In Proceedings of the 11th International Conference on Compiler Construction (CC ’02). Springer-Verlag, Berlin, Heidelberg. 159–178. isbn:3540433694

[11]

R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. 1989. An Efficient Method of Computing Static Single Assignment Form. In Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’89). Association for Computing Machinery, New York, NY, USA. 25–35. isbn:0897912942 https://doi.org/10.1145/75277.75280

Digital Library

[12]

Al Danial. 2021. cloc: Count Lines of Code. https://github.com/AlDanial/cloc

[13]

Isil Dillig, Thomas Dillig, Alex Aiken, and Mooly Sagiv. 2011. Precise and Compact Modular Procedure Summaries for Heap Manipulating Programs. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’11). Association for Computing Machinery, New York, NY, USA. 567–577. isbn:9781450306638 https://doi.org/10.1145/1993498.1993565

Digital Library

[14]

Ana Nora Evans, Bradford Campbell, and Mary Lou Soffa. 2020. Is Rust Used Safely by Software Developers? In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE ’20). Association for Computing Machinery, New York, NY, USA. 246–257. isbn:9781450371216 https://doi.org/10.1145/3377811.3380413

Digital Library

[15]

Jeanne Ferrante, Karl J. Ottenstein, and Joe D. Warren. 1987. The Program Dependence Graph and Its Use in Optimization. ACM Trans. Program. Lang. Syst., 9, 3 (1987), jul, 319–349. issn:0164-0925 https://doi.org/10.1145/24039.24041

Digital Library

[16]

Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science, 50, 1 (1987), 1–101. https://doi.org/10.1016/0304-3975(87)90045-4

Digital Library

[17]

J. A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. In 1982 IEEE Symposium on Security and Privacy. IEEE. https://doi.org/10.1109/sp.1982.10014

[18]

Dan Grossman, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. 2002. Region-Based Memory Management in Cyclone. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI ’02). Association for Computing Machinery, New York, NY, USA. 282–293. isbn:1581134630 https://doi.org/10.1145/512529.512563

Digital Library

[19]

Andrew Head, Elena L. Glassman, Björn Hartmann, and Marti A. Hearst. 2018. Interactive Extraction of Examples from Existing Code. In Proceedings of the 2018 CHI Conference on Human Factors in Computing Systems. Association for Computing Machinery, New York, NY, USA. 1–12. isbn:9781450356206 https://doi.org/10.1145/3173574.3173659

Digital Library

[20]

Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer. 2019. Stacked Borrows: An Aliasing Model for Rust. Proc. ACM Program. Lang., 4, POPL (2019), Article 41, dec, 32 pages. https://doi.org/10.1145/3371109

Digital Library

[21]

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the Foundations of the Rust Programming Language. Proc. ACM Program. Lang., 2, POPL (2017), Article 66, dec, 34 pages. https://doi.org/10.1145/3158154

Digital Library

[22]

Amy J. Ko and Brad A. Myers. 2004. Designing the Whyline: A Debugging Interface for Asking Questions about Program Behavior. In Proceedings of the SIGCHI Conference on Human Factors in Computing Systems (CHI ’04). Association for Computing Machinery, New York, NY, USA. 151–158. isbn:1581137028 https://doi.org/10.1145/985692.985712

Digital Library

[23]

Peng Li and S. Zdancewic. 2006. Encoding information flow in Haskell. In 19th IEEE Computer Security Foundations Workshop (CSFW’06). 12 pp.–16. https://doi.org/10.1109/CSFW.2006.13

Digital Library

[24]

Niko Matsakis. 2017. Non-lexical lifetimes. https://rust-lang.github.io/rfcs/2094-nll.html

[25]

Andrew C. Myers. 1999. JFlow: Practical Mostly-Static Information Flow Control. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’99). Association for Computing Machinery, New York, NY, USA. 228–241. isbn:1581130953 https://doi.org/10.1145/292540.292561

Digital Library

[26]

Emil Jørgensen Njor and Hilmar Gústafsson. 2021. Static Taint Analysis in Rust. Master’s thesis. Aalborg University.

[27]

François Pottier and Vincent Simonet. 2003. Information Flow Inference for ML. ACM Trans. Program. Lang. Syst., 25, 1 (2003), jan, 117–158. issn:0164-0925 https://doi.org/10.1145/596980.596983

Digital Library

[28]

Zvonimir Rakamaric and Michael Emmi. 2014. SMACK: Decoupling Source Language Details from Verifier Implementations. In Proceedings of the 26th International Conference on Computer Aided Verification (CAV), Armin Biere and Roderick Bloem (Eds.) (Lecture Notes in Computer Science, Vol. 8559). Springer, 106–113. https://doi.org/10.1007/978-3-319-08867-9_7

Digital Library

[29]

Atanas Rountev, Barbara G. Ryder, and William Landi. 1999. Data-Flow Analysis of Program Fragments. In Proceedings of the 7th European Software Engineering Conference Held Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE-7). Springer-Verlag, Berlin, Heidelberg. 235–252. isbn:3540665382

Digital Library

[30]

Alejandro Russo, Koen Claessen, and John Hughes. 2008. A Library for Light-Weight Information-Flow Security in Haskell. In Proceedings of the First ACM SIGPLAN Symposium on Haskell (Haskell ’08). Association for Computing Machinery, New York, NY, USA. 13–24. isbn:9781605580647 https://doi.org/10.1145/1411286.1411289

Digital Library

[31]

A. Sabelfeld and A.C. Myers. 2003. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21, 1 (2003), 5–19. https://doi.org/10.1109/JSAC.2002.806121

Digital Library

[32]

Marc Shapiro and Susan Horwitz. 1997. The Effects of the Precision of Pointer Analysis. In Proceedings of the 4th International Symposium on Static Analysis (SAS ’97). Springer-Verlag, Berlin, Heidelberg. 16–34. isbn:3540634681

Digital Library

[33]

Yannis Smaragdakis and George Balatsouras. 2015. Pointer analysis. Foundations and Trends in Programming Languages, 2, 1 (2015), 1–69.

Digital Library

[34]

Deian Stefan, Alejandro Russo, John C. Mitchell, and David Mazières. 2011. Flexible Dynamic Information Flow Control in Haskell. In Proceedings of the 4th ACM Symposium on Haskell (Haskell ’11). Association for Computing Machinery, New York, NY, USA. 95–106. isbn:9781450308601 https://doi.org/10.1145/2034675.2034688

Digital Library

[35]

Hao Tang, Xiaoyin Wang, Lingming Zhang, Bing Xie, Lu Zhang, and Hong Mei. 2015. Summary-Based Context-Sensitive Data-Dependence Analysis in Presence of Callbacks. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). Association for Computing Machinery, New York, NY, USA. 83–95. isbn:9781450333009 https://doi.org/10.1145/2676726.2676997

Digital Library

[36]

Yan Mei Tang and Pierre Jouvelot. 1994. Separate abstract interpretation for control-flow analysis. In Lecture Notes in Computer Science. Springer Berlin Heidelberg, 224–243. https://doi.org/10.1007/3-540-57887-0_98

[37]

Mark Weiser. 1981. Program Slicing. In Proceedings of the 5th International Conference on Software Engineering (ICSE ’81). IEEE Press, 439–449. isbn:0897911466

Digital Library

[38]

Aaron Weiss, Olek Gierczak, Daniel Patterson, and Amal Ahmed. 2019. Oxide: The Essence of Rust. arxiv:arXiv:1903.00982v3.

[39]

Ming Wen, Junjie Chen, Rongxin Wu, Dan Hao, and Shing-Chi Cheung. 2018. Context-Aware Patch Generation for Better Automated Program Repair. In Proceedings of the 40th International Conference on Software Engineering (ICSE ’18). Association for Computing Machinery, New York, NY, USA. 1–11. isbn:9781450356381 https://doi.org/10.1145/3180155.3180233

Digital Library

[40]

Greta Yorsh, Eran Yahav, and Satish Chandra. 2008. Generating Precise and Concise Procedure Summaries. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’08). Association for Computing Machinery, New York, NY, USA. 221–234. isbn:9781595936899 https://doi.org/10.1145/1328438.1328467

Digital Library

Cited By

Lamba ATaylor MBeardsley VBambeck JBond MLin Z(2024)Cocoon: Static Information Flow Control in RustProceedings of the ACM on Programming Languages10.1145/36498178:OOPSLA1(166-193)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649817
Surbatovich MSpargo NJia LLucia B(2023)A Type System for Safe Intermittent ComputingProceedings of the ACM on Programming Languages10.1145/35912507:PLDI(736-760)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591250
Almeida MCole GDu KLuo GPan SPan YQiu KReddy VZhang HZhu YOmar C(2022)RustViz: Interactively Visualizing Ownership and Borrowing2022 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC)10.1109/VL/HCC53370.2022.9833121(1-10)Online publication date: 12-Sep-2022
https://doi.org/10.1109/VL/HCC53370.2022.9833121

Index Terms

Modular information flow through ownership
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Automated static analysis

Recommendations

Composing polymorphic information flow systems with reference immutability
FTfJP '13: Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs

Information flow type systems, such as EnerJ (a type system for energy efficiency), and integrity and confidentiality, are unsound if subtyping for references is allowed because of the presence of mutable references. The standard approach is to disallow ...
Hypercollecting semantics and its application to static analysis of information flow
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

We show how static analysis for secure information flow can be expressed and proved correct entirely within the framework of abstract interpretation. The key idea is to define a Galois connection that directly approximates the hyperproperty of interest. ...
Hypercollecting semantics and its application to static analysis of information flow
POPL '17

We show how static analysis for secure information flow can be expressed and proved correct entirely within the framework of abstract interpretation. The key idea is to define a Galois connection that directly approximates the hyperproperty of interest. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2022

1038 pages

ISBN:9781450392655

DOI:10.1145/3519939

General Chair:
Ranjit Jhala
University of California at San Diego, USA
,
Program Chair:
Işil Dillig
University of Texas at Austin, USA

Copyright © 2022 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 June 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

PLDI '22

Sponsor:

SIGPLAN

PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 13 - 17, 2022

CA, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
569
Total Downloads

Downloads (Last 12 months)203
Downloads (Last 6 weeks)29

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lamba ATaylor MBeardsley VBambeck JBond MLin Z(2024)Cocoon: Static Information Flow Control in RustProceedings of the ACM on Programming Languages10.1145/36498178:OOPSLA1(166-193)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649817
Surbatovich MSpargo NJia LLucia B(2023)A Type System for Safe Intermittent ComputingProceedings of the ACM on Programming Languages10.1145/35912507:PLDI(736-760)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591250
Almeida MCole GDu KLuo GPan SPan YQiu KReddy VZhang HZhu YOmar C(2022)RustViz: Interactively Visualizing Ownership and Borrowing2022 IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC)10.1109/VL/HCC53370.2022.9833121(1-10)Online publication date: 12-Sep-2022
https://doi.org/10.1109/VL/HCC53370.2022.9833121

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents