research-article

Open access

From fine- to coarse-grained dynamic information flow control and back

Authors:

Alejandro Russo,

Deian StefanAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue POPL

Article No.: 76, Pages 1 - 31

https://doi.org/10.1145/3290389

Published: 02 January 2019 Publication History

Abstract

We show that fine-grained and coarse-grained dynamic information-flow control (IFC) systems are equally expressive. To this end, we mechanize two mostly standard languages, one with a fine-grained dynamic IFC system and the other with a coarse-grained dynamic IFC system, and prove a semantics-preserving translation from each language to the other. In addition, we derive the standard security property of non-interference of each language from that of the other, via our verified translation. This result addresses a longstanding open problem in IFC: whether coarse-grained dynamic IFC techniques are less expressive than fine-grained dynamic IFC techniques (they are not!). The translations also stand to have important implications on the usability of IFC approaches. The coarse- to fine-grained direction can be used to remove the label annotation burden that fine-grained systems impose on developers, while the fine- to coarse-grained translation shows that coarse-grained systems---which are easier to design and implement---can track information as precisely as fine-grained systems and provides an algorithm for automatically retrofitting legacy applications to run on existing coarse-grained systems.

Supplementary Material

WEBM File (a76-vassena.webm)

Download
88.81 MB

References

[1]

Thomas H. Austin and Cormac Flanagan. 2009. Efficient Purely-Dynamic Information Flow Analysis. In Proc. of the 9th ACM Workshop on Programming Languages and Analysis for Security (PLAS ’09).

Digital Library

[2]

Thomas H. Austin and Cormac Flanagan. 2010. Permissive Dynamic Information Flow Analysis. In Proc. of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS ’10).

Digital Library

[3]

Gilles Barthe, Tamara Rezk, and Amitabh Basu. 2007. Security Types Preserving Compilation. Computer Languages, Systems & Structures 33, 2 (2007), 35–59.

Digital Library

[4]

Lujo Bauer, Shaoying Cai, Limin Jia, Timothy Passaro, Michael Stroucken, and Yuan Tian. 2015. Run-time Monitoring and Formal Analysis of Information Flows in Chromium. In Proc. of the 22nd Annual Network & Distributed System Security Symposium. Internet Society.

[5]

Abhishek Bichhawat, Vineet Rajani, Deepak Garg, and Christian Hammer. 2014. Information Flow Control in WebKit’s JavaScript Bytecode. In International Conference on Principles of Security and Trust (POST). 159–178.

[6]

Niklas Broberg, Bart van Delft, and David Sands. 2013. Paragon for Practical Programming with Information-Flow Control. In Proc. of the 11th Asian Symposium on Programming Languages and Systems (APLAS ’13). 217–232.

Digital Library

[7]

Pablo Buiras, Deian Stefan, and Alejandro Russo. 2014. On Dynamic Flow-Sensitive Floating-Label Systems. In Proc. of the 2014 IEEE 27th Computer Security Foundations Symposium (CSF ’14). IEEE Computer Society, Washington, DC, USA, 65–79.

Digital Library

[8]

Pablo Buiras, Dimitrios Vytiniotis, and Alejandro Russo. 2015. HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell. In ACM SIGPLAN Notices, Vol. 50. ACM, 280–288.

Digital Library

[9]

Petros Efstathopoulos, Maxwell Krohn, Steve VanDeBogart, Cliff Frey, David Ziegler, Eddie Kohler, David Mazières, Frans Kaashoek, and Robert Morris. 2005. Labels and Event Processes in the Asbestos Operating System. In Proc. of the 20th ACM symp. on Operating systems principles (SOSP ’05).

Digital Library

[10]

Matthias Felleisen. 1991. On the Expressive Power of Programming Languages. Sci. Comput. Program. 17, 1-3 (Dec. 1991), 35–75.

Digital Library

[11]

Earlence Fernandes, Justin Paupore, Amir Rahmati, Daniel Simionato, Mauro Conti, and Atul Prakash. 2016. FlowFence: Practical Data Protection for Emerging IoT Application Frameworks. In USENIX Security Symposium. 531–548.

Digital Library

[12]

Daniel B. Giffin, Amit Levy, Deian Stefan, David Terei, David Mazières, John C. Mitchell, and Alejandro Russo. 2012. Hails: Protecting Data Privacy in Untrusted Web Applications. In 10th USENIX Symposium on Operating Systems Design and Implementation, OSDI ’12.

Digital Library

[13]

J.A. Goguen and J. Meseguer. 1982. Security Policies and Security Models. In Proc. of IEEE Symposium on Security and Privacy. IEEE Computer Society.

[14]

D. Hedin, A. Birgisson, L. Bello, and A. Sabelfeld. 2014. JSFlow: Tracking Information Flow in JavaScript and its APIs. In Proc. of the ACM Symposium on Applied Computing (SAC ’14).

Digital Library

[15]

Stefan Heule, Deian Stefan, Edward Z. Yang, John C. Mitchell, and Alejandro Russo. 2015. IFC Inside: Retrofitting Languages with Dynamic Information Flow Control. In Proc. of the Conference on Principles of Security and Trust (POST ’15). Springer.

Digital Library

[16]

Catalin Hritcu, Michael Greenberg, Ben Karel, Benjamin C. Pierce, and Greg Morrisett. 2013. All Your IFCException Are Belong to Us. In Proc. of the 2013 IEEE Symposium on Security and Privacy (SP ’13). IEEE Computer Society, Washington, DC, USA, 3–17.

Digital Library

[17]

M. Jaskelioff and A. Russo. 2011. Secure Multi-execution in Haskell. In Proc. Andrei Ershov International Conference on Perspectives of System Informatics (LNCS). Springer-Verlag.

Digital Library

[18]

Limin Jia, Jassim Aljuraidan, Elli Fragkaki, Lujo Bauer, Michael Stroucken, Kazuhide Fukushima, Shinsaku Kiyomoto, and Yutaka Miyake. 2013. Run-Time Enforcement of Information-Flow Properties on Android. In Proc. of the 18th European Symposium on Research in Computer Security (ESORICS ’13). Springer.

[19]

Maxwell Krohn, Alexander Yip, Micah Brodsky, Natan Cliffer, M. Frans Kaashoek, Eddie Kohler, and Robert Morris. 2007. Information Flow Control for Standard OS Abstractions. (October 2007).

[20]

Andrew C. Myers, Lantian Zheng, Steve Zdancewic, Stephen Chong, and Nathaniel Nystrom. 2006. Jif 3.0: Java information flow. (July 2006). http://www.cs.cornell.edu/jif

[21]

Adwait Nadkarni, Benjamin Andow, William Enck, and Somesh Jha. 2016. Practical DIFC Enforcement on Android. In USENIX Security Symposium. 1119–1136.

Digital Library

[22]

François Pottier and Vincent Simonet. 2003. Information Flow Inference for ML. ACM Trans. Program. Lang. Syst. 25, 1 (Jan. 2003), 117–158.

Digital Library

[23]

Vineet Rajani, Iulia Bastys, Willard Rafnsson, and Deepak Garg. 2017. Type Systems for Information Flow Control: The Question of Granularity. ACM SIGLOG News 4, 1 (Feb. 2017), 6–21.

Digital Library

[24]

Vineet Rajani and Deepak Garg. 2018. Types for Information Flow Control: Labeling Granularity and Semantic Models. In Proc. of the IEEE Computer Security Foundations Symp. (CSF ’18). IEEE Computer Society.

[25]

Indrajit Roy, Donald E. Porter, Michael D. Bond, Kathryn S. McKinley, and Emmett Witchel. 2009. Laminar: Practical Finegrained Decentralized Information Flow Control. In Proc. of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’09). ACM, New York, NY, USA, 63–74.

Digital Library

[26]

Alejandro Russo. 2015. Functional Pearl: Two Can Keep a Secret, if One of Them Uses Haskell. In Proc. of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015). ACM.

Digital Library

[27]

Alejandro Russo, Koen Claessen, and John Hughes. 2009. A library for light-weight Information-Flow Security in Haskell. ACM SIGPLAN Notices (HASKELL ’08) 44 (01 2009), 13.

Digital Library

[28]

Alejandro Russo and Andrei Sabelfeld. 2010. Dynamic vs. Static Flow-Sensitive Security Analysis. In Proc. of the 2010 23rd IEEE Computer Security Foundations Symp. (CSF ’10). IEEE Computer Society, 186–199.

Digital Library

[29]

Andrei Sabelfeld and Andrew C. Myers. 2006. Language-based Information-flow Security. IEEE J.Sel. A. Commun. 21, 1 (Sept. 2006), 5–19.

Digital Library

[30]

Thomas Schmitz, Maximilian Algehed, Cormac Flanagan, and Alejandro Russo. 2018. Faceted Secure Multi Execution. In Proc. of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS ’18). ACM, New York, NY, USA, 1617–1634.

Digital Library

[31]

Deian Stefan, Alejandro Russo, Pablo Buiras, Amit Levy, John C. Mitchell, and David Mazières. 2012. Addressing Covert Termination and Timing Channels in Concurrent Information Flow Systems. In International Conference on Functional Programming (ICFP). ACM SIGPLAN.

Digital Library

[32]

Deian Stefan, Alejandro Russo, David Mazières, and John C. Mitchell. 2017. Flexible Dynamic Information Flow Control in the Presence of Exceptions. Journal of Functional Programming 27 (2017).

[33]

Deian Stefan, Alejandro Russo, John C. Mitchell, and David Mazières. 2011. Flexible Dynamic Information Flow Control in Haskell. In Proc. of the 4th ACM Symposium on Haskell (Haskell ’11). ACM, New York, NY, USA, 95–106.

Digital Library

[34]

Deian Stefan, Edward Z. Yang, Petr Marchenko, Alejandro Russo, Dave Herman, Brad Karp, and David Mazières. 2014. Protecting Users by Confining JavaScript with COWL. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI’14). USENIX Association, Berkeley, CA, USA, 131–146. http://dl.acm.org/citation.cfm? id=2685048.2685060

Digital Library

[35]

Ta-Chung Tsai, Alejandro Russo, and John Hughes. 2007. A Library for Secure Multi-threaded Information Flow in Haskell. In Proc. of the 20th IEEE Computer Security Foundations Symposium (CSF’07). 187–202.

Digital Library

[36]

Marco Vassena and Alejandro Russo. 2016. On Formalizing Information-Flow Control Libraries. In Proc. of the 2016 ACM Workshop on Programming Languages and Analysis for Security (PLAS ’16). ACM, New York, NY, USA, 15–28.

Digital Library

[37]

Marco Vassena, Alejandro Russo, Pablo Buiras, and Lucas Waye. 2017. MAC A Verified Static Information-Flow Control Library. Journal of Logical and Algebraic Methods in Programming (2017).

[38]

Dennis Volpano and Geoffrey Smith. 1997. Eliminating Covert Flows with Minimum Typings. In Proc. of the 10th IEEE workshop on Computer Security Foundations (CSFW ’97). IEEE Computer Society.

Digital Library

[39]

Jean Yang, Kuat Yessenov, and Armando Solar-Lezama. 2012. A Language for Automatically Enforcing Privacy Policies. In Proc. of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’12). ACM, New York, NY, USA, 85–96.

Digital Library

[40]

Alexander Yip, Neha Narula, Maxwell Krohn, and Robert Morris. 2009. Privacy-preserving Browser-side Scripting with BFlow. In Proc. of the 4th ACM European Conference on Computer Systems (EuroSys ’09). ACM.

Digital Library

[41]

Stephan Arthur Zdancewic. 2002. Programming Languages for Information Security. Ph.D. Dissertation. Ithaca, NY, USA. AAI3063751.

Digital Library

[42]

Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazières. 2006. Making Information Flow Explicit in HiStar. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation - Volume 7 (OSDI ’06). USENIX Association, Berkeley, CA, USA, 19–19. http://dl.acm.org/citation.cfm?id=1267308.1267327

Digital Library

[43]

Nickolai Zeldovich, Silas Boyd-Wickizer, and David Mazières. 2008. Securing Distributed Systems with Information Flow Control. In Proceedings of the 5th USENIX Symposium on Networked Systems Design and Implementation (NSDI’08). USENIX Association, Berkeley, CA, USA, 293–308. http://dl.acm.org/citation.cfm?id=1387589.1387610

Digital Library

Cited By

Tarkhani ZMadhavapeddy A(2023)Information Flow Tracking for Heterogeneous Compartmentalized SoftwareProceedings of the 26th International Symposium on Research in Attacks, Intrusions and Defenses10.1145/3607199.3607235(564-579)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3607199.3607235
Runge TServetto MPotanin ASchaefer I(2022)Immutability and Encapsulation for Sound OO Information Flow ControlACM Transactions on Programming Languages and Systems10.1145/357327045:1(1-35)Online publication date: 2-Dec-2022
https://dl.acm.org/doi/10.1145/3573270
Gregersen SBay JTimany ABirkedal L(2021)Mechanized logical relations for termination-insensitive noninterferenceProceedings of the ACM on Programming Languages10.1145/34342915:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434291
Show More Cited By

Index Terms

From fine- to coarse-grained dynamic information flow control and back
1. Security and privacy
  1. Formal methods and theory of security
    1. Formal security models

Recommendations

From Fine- to Coarse-Grained Dynamic Information Flow Control and Back

This tutorial provides a complete and homogeneous account of the latest advances in fine- and coarse-grained dynamic information-flow control (IFC) security. Since the 1970s, the programming language and the operating system communities proposed different ...
Fine-grained role graph model
A fine-grained, controllable, user-to-user delegation method in RBAC
SACMAT '05: Proceedings of the tenth ACM symposium on Access control models and technologies

This paper addresses the issues surrounding user-to-user delegation in RBAC. We show how delegations can be incorporated into the RBAC model in a simple and straightforward manner. A special feature of the model is that it allows fine-grained control ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue POPL

January 2019

2275 pages

EISSN:2475-1421

DOI:10.1145/3302515

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution-ShareAlike International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 January 2019

Published in PACMPL Volume 3, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

11
Total Citations
View Citations
1,192
Total Downloads

Downloads (Last 12 months)141
Downloads (Last 6 weeks)21

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tarkhani ZMadhavapeddy A(2023)Information Flow Tracking for Heterogeneous Compartmentalized SoftwareProceedings of the 26th International Symposium on Research in Attacks, Intrusions and Defenses10.1145/3607199.3607235(564-579)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3607199.3607235
Runge TServetto MPotanin ASchaefer I(2022)Immutability and Encapsulation for Sound OO Information Flow ControlACM Transactions on Programming Languages and Systems10.1145/357327045:1(1-35)Online publication date: 2-Dec-2022
https://dl.acm.org/doi/10.1145/3573270
Gregersen SBay JTimany ABirkedal L(2021)Mechanized logical relations for termination-insensitive noninterferenceProceedings of the ACM on Programming Languages10.1145/34342915:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434291
Xiang JChong S(2021)Co-Inflow: Coarse-grained Information Flow Control for Java-like Languages2021 IEEE Symposium on Security and Privacy (SP)10.1109/SP40001.2021.00002(18-35)Online publication date: May-2021
https://doi.org/10.1109/SP40001.2021.00002
Ahmadpanah MAskarov ASabelfeld A(2021)Nontransitive Policies Transpiled2021 IEEE European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP51992.2021.00043(543-561)Online publication date: Sep-2021
https://doi.org/10.1109/EuroSP51992.2021.00043
Zhong WZhao JHu H(2021)A Multilevel Non-interference Vulnerability Analysis Method for Information Leakage Problem2021 IEEE Sixth International Conference on Data Science in Cyberspace (DSC)10.1109/DSC53577.2021.00058(367-374)Online publication date: Oct-2021
https://doi.org/10.1109/DSC53577.2021.00058
Bichhawat AMcCall MJia L(2021)Gradual Security Types and Gradual Guarantees2021 IEEE 34th Computer Security Foundations Symposium (CSF)10.1109/CSF51468.2021.00015(1-16)Online publication date: Jun-2021
https://doi.org/10.1109/CSF51468.2021.00015
Lu YZhang C(2020)Nontransitive Security Types for Coarse-grained Information Flow Control2020 IEEE 33rd Computer Security Foundations Symposium (CSF)10.1109/CSF49147.2020.00022(199-213)Online publication date: Jun-2020
https://doi.org/10.1109/CSF49147.2020.00022
Sun HYang WChen RKang X(2020)A coarse-grained water model for mesoscale simulation of clay-water interactionJournal of Molecular Liquids10.1016/j.molliq.2020.114085(114085)Online publication date: Aug-2020
https://doi.org/10.1016/j.molliq.2020.114085
Kang XSun HYang WChen R(2020)Wettability of Clay Aggregates— A Coarse-Grained Molecular Dynamic StudyApplied Surface Science10.1016/j.apsusc.2020.147423(147423)Online publication date: Aug-2020
https://doi.org/10.1016/j.apsusc.2020.147423
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents