Document Open Access Logo

Semantics for Noninterference with Interaction Trees

Authors Lucas Silver, Paul He , Ethan Cecchetti , Andrew K. Hirsch , Steve Zdancewic

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.29.pdf
  • Filesize: 1.09 MB
  • 29 pages

Document Identifiers

Author Details

Lucas Silver
  • University of Pennsylvania, Philadelphia, PA, USA
Paul He
  • University of Pennsylvania, Philadelphia, PA, USA
Ethan Cecchetti
  • University of Maryland, College Park, MD, USA
  • University of Wisconsin - Madison, WI, USA
Andrew K. Hirsch
  • State University of New York at Buffalo, NY, USA
Steve Zdancewic
  • University of Pennsylvania, Philadelphia, PA, USA

Funding

This work was funded in part by the NSF under the award 1521539 (Weirich, Zdancewic, Pierce).

Cite As Get BibTex

Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. Semantics for Noninterference with Interaction Trees. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 29:1-29:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.ECOOP.2023.29

Abstract

Noninterference is the strong information-security property that a program does not leak secrets through publicly-visible behavior. In the presence of effects such as nontermination, state, and exceptions, reasoning about noninterference quickly becomes subtle. We advocate using interaction trees (ITrees) to provide compositional mechanized proofs of noninterference for multi-language, effectful, nonterminating programs, while retaining executability of the semantics. We develop important foundations for security analysis with ITrees: two indistinguishability relations, leading to two standard notions of noninterference with adversaries of different strength, along with metatheory libraries for reasoning about each. We demonstrate the utility of our results using a simple imperative language with embedded assembly, along with a compiler into that assembly language.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Security and privacy → Logic and verification
  • Security and privacy → Information flow control
Keywords
  • verification
  • information-flow
  • denotational semantics
  • monads

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon Riecke. A core calculus of dependency. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 1999. URL: https://doi.org/10.1145/292540.292555.
  2. Carmine Abate, Roberto Blanco, Deepak Garg, Cătălin Hriţcu, Marco Patrignani, and Jérémy Thibault. Journey beyond full abstraction: Exploring robust property preservation for secure compilation. In IEEE Computer Security Foundations Symposium (CSF), 2019. URL: https://doi.org/10.1109/CSF.2019.00025.
  3. Maximilian Algehed and Jean-Philippe Bernardy. Simple noninterference from parametricity. Proc. ACM Program. Lang., 3(ICFP), July 2019. URL: https://doi.org/10.1145/3341693.
  4. Maximilian Algehed and Alejandro Russo. Encoding dcc in haskell. In Workshop on Programming Languages and Analysis for Security (PLAS), 2017. URL: https://doi.org/10.1145/3139337.3139338.
  5. Owen Arden, Jed Liu, and Andrew C. Myers. Flow-limited authorization. In IEEE Computer Security Foundations Symposium (CSF), July 2015. URL: https://doi.org/10.1109/CSF.2015.42.
  6. Aslan Askarov, Sebastian Hunt, Andrei Sabelfeld, and David Sands. Termination-insensitive noninterference leaks more than just a bit. In European Symposium on Research in Computer Security (ESORICS), pages 333-348. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-88313-5_22.
  7. Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Cătălin Hriţcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, and Andrew Tolmach. A verified information-flow architecture. SIGPLAN Not., 49(1):165-178, January 2014. URL: https://doi.org/10.1145/2578855.2535839.
  8. Gilles Barthe, Amitabh Basu, and Tamara Rezk. Security types preserving compilation. In Bernhard Steffen and Giorgio Levi, editors, Verification, Model Checking, and Abstract Interpretation, pages 2-15, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  9. Gilles Barthe, Benjamin Greégoire, and Vincent Laporte. Secure compilation of side-channel countermeasures: The case of cryptographic "constant time". In IEEE Computer Security Foundations Symposium (CSF), 2018. URL: https://doi.org/10.1109/CSF.2018.00031.
  10. Andrej Bauer and Matija Pretnar. Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming, 84(1):108-123, January 2015. Google Scholar
  11. Johan Bay and Aslan Askarov. Reconciling progress-insensitive noninterference and declassification. In IEEE Computer Security Foundations Symposium (CSF), June 2020. URL: https://doi.org/10.1109/CSF49147.2020.00015.
  12. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. Journal of Computer Security (JCS), 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  13. Riccardo Focardi, Carla Piazza, and Sabina Rossi. Proof methods for bisimulation based information flow security. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2002. Google Scholar
  14. Riccardo Focardi, Sabrina Rossi, and Andrei Sabelfeld. Bridging language-based and process calculi security. In FoSSaCS, 2005. URL: https://doi.org/10.1007/978-3-540-31982-5_19.
  15. Joseph A. Goguen and Jose Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy (S&P), 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  16. Simon Oddershede Gregersen, Johan Bay, Amin Timany, and Lars Birkedal. Mechanized logical relations for termination-insensitive noninterference. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434291.
  17. Andrew K. Hirsch and Ethan Cecchetti. Giving semantics to program-counter labels via secure effects. Proceedings of the ACM on Programming Languages, 5(POPL), January 2021. URL: https://doi.org/10.1145/3434316.
  18. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013. URL: https://doi.org/10.1145/2429069.2429093.
  19. Mauro Jaskelioff. Modular monad transformers. In Giuseppe Castagna, editor, Programming Languages and Systems, pages 64-79, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  20. Limin Jia and Steve Zdancewic. Encoding information flow in Aura. In Proceedings of the 2009 Workshop on Programming Languages and Analysis for Security (PLAS), pages 17-29, 2009. Google Scholar
  21. Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 2015. URL: https://doi.org/10.1145/2676726.2676980.
  22. Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, pages 94-105, 2015. URL: https://doi.org/10.1145/2804302.2804319.
  23. Oleg Kiselyov, Amr Sabry, and Cameron Swords. Extensible effects: an alternative to monad transformers. ACM SIGPLAN Notices, 48(12):59-70, 2013. Google Scholar
  24. Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. From c to interaction trees: Specifying, verifying, and testing a networked server. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019. URL: https://doi.org/10.1145/3293880.3294106.
  25. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. URL: https://doi.org/10.1145/1538788.1538814.
  26. Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers and modular interpreters. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 1995. URL: https://doi.org/10.1145/199448.199528.
  27. Jed Liu, Owen Arden, Michael D. George, and Andrew C. Myers. Fabric: Building open distributed systems securely by construction. Journal of Computer Security (JCS), 25(4-5):319-321, May 2017. URL: https://doi.org/10.3233/JCS-0559.
  28. Tom Magrino, Jed Liu, Owen Arden, Chin Isradisaikul, and Andrew C. Myers. Jif 3.5: Java information flow. Software release, 2016. URL: https://www.cs.cornell.edu/jif.
  29. Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2018. Version 8.8.1. URL: http://coq.inria.fr.
  30. Mae P. Milano and Andrew C. Myers. MixT: A language for mixing consistency in geodistributed transactions. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2018. URL: https://doi.org/10.1145/3192366.3192375.
  31. Eugenio Moggi. Computational lambda-calculus and monads. In LICS, pages 14-23, June 1989. Full version, titled Notions of Computation and Monads, in Information and Computation, 93(1), pp. 55-92, 1991. Google Scholar
  32. Andrew C. Myers. JFlow: Practical mostly-static information flow control. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), January 1999. URL: https://doi.org/10.1145/292540.292561.
  33. Andrew C. Myers and Barbara Liskov. Complete, safe information flow with decentralized labels. In IEEE Symposium on Security and Privacy (S&P), 1998. URL: https://doi.org/10.1109/SECPRI.1998.674834.
  34. Gordon Plotkin and John Power. Adequacy for algebraic effects. In Furio Honsell and Marino Miculan, editors, Foundations of Software Science and Computation Structures, pages 1-24, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  35. Gordon Plotkin and John Power. Notions of computation determine monads. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, pages 342-356, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. Google Scholar
  36. Gordon D Plotkin. A structural approach to operational semantics. Aarhus university, 1981. Google Scholar
  37. Gordon D. Plotkin and John Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69-94, 2003. Google Scholar
  38. Gordon D Plotkin and Matija Pretnar. Handling Algebraic Effects. Logical Methods in Computer Science, 9(4), December 2013. URL: https://doi.org/10.2168/LMCS-9(4:23)2013.
  39. Nadia Polikarpova, Deian Stefan, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama. Liquid information flow control. Proceedings of the ACM on Programming Languages, 4(ICFP), August 2020. URL: https://doi.org/10.1145/3408987.
  40. François Pottier and Vincent Simonet. Information flow inference for ML. ACM Transactions on Programming Languages and Systems (TOPLAS), 25(1):117-158, January 2003. URL: https://doi.org/10.1145/596980.596983.
  41. Willard Rafnsson and Andrei Sabelfeld. Compositional information-flow security for interactive systems. In IEEE Computer Security Foundations Symposium (CSF), 2014. URL: https://doi.org/10.1109/CSF.2013.8.
  42. Vineet Rajani and Deepak Garg. Types for information flow control: Labeling granularity and semantic models. In IEEE Computer Security Foundations Symposium (CSF), 2018. URL: https://doi.org/10.1109/CSF.2018.00024.
  43. John Reynolds. Types, abstraction and parametric polymorphism. Information Processing, 1983. Google Scholar
  44. Alejandro Russo, Koen Claessen, and John Hughes. A library for light-weight information-flow security in haskell. In ACM SIGPLAN Haskell Symposium, 2008. URL: https://doi.org/10.1145/1411286.1411289.
  45. Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5-19, January 2003. URL: https://doi.org/10.1109/JSAC.2002.806121.
  46. Andrei Sabelfeld and David Sands. A PER model of secure information flow in sequential programs. Higher-Order and Symbolic Computation, 14(1):59-91, 2001. URL: https://doi.org/10.1023/A:1011553200337.
  47. Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff. Monad transformers and algebraic effects: What binds them together. Technical Report CW699, Department of Computer Science, KU Leuven, 2016. Google Scholar
  48. Geoffery Smith. Probabilistic noninterference through weak probabilistic bisimulation. In Computer Security Foundations Workshop (CSFW), 2003. URL: https://doi.org/10.1109/CSFW.2003.1212701.
  49. Deian Stefan, Alejandro Russo, David Mazières, and John C. Mitchell. Disjunction category labels. In Nordic Conference on Security IT Systems (NordSec), October 2011. URL: https://doi.org/10.1007/978-3-642-29615-4_16.
  50. Wouter Swierstra. Data types à la carte. Journal of Functional Programming, 18(4):423-436, 2008. URL: https://doi.org/10.1017/S0956796808006758.
  51. Tsa-ching Tsai, Alejandro Russo, and John Hughes. A library for secure multi-threaded information flow in haskell. In IEEE Computer Security Foundations Symposium (CSF), 2007. URL: https://doi.org/10.1109/CSF.2007.6.
  52. Marco Vassena and Alejandro Russo. On formalizing information-flow control libraries. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS '16, pages 15-28, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2993600.2993608.
  53. Marco Vassena, Alejandro Russo, Pablo Buiras, and Lucas Waye. MAC: A verified static information-flow control library. Journal of Logical and Algebraic Methods in Programming (JLAMP), 95, 2018. URL: https://doi.org/10.1016/j.jlamp.2017.12.003.
  54. Marco Vassena, Alejandro Russo, Deepak Garg, Vineet Rajani, and Deian Stefan. From fine- to coarse-grained dynamic information flow control and back. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019. URL: https://doi.org/10.1145/3290389.
  55. Dennis Volpano and Geoffrey Smith. Eliminating covert flows with minimum typings. In IEEE Computer Security Foundations Workshop (CSFW), June 1997. URL: https://doi.org/10.1109/CSFW.1997.596807.
  56. Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security (JCS), 4(3), 1996. URL: https://doi.org/10.3233/JCS-1996-42-304.
  57. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: Representing recursive and impure programs in coq. Proceedings of the ACM on Programming Languages, 4(POPL), January 2020. URL: https://doi.org/10.1145/3371119.
  58. Drew Zagieboylo, G. Edward Suh, and Andrew C. Myers. Using information flow to design an ISA that controls timing channels. In IEEE Computer Security Foundations Symposium (CSF), June 2019. URL: https://doi.org/10.1109/CSF.2019.00026.
  59. Yannick Zakowski, Calvin Beck, Irene Yoon, Ilya Zaichuk, Vadim Zaliva, and Steve Zdancewic. Modular, compositional, and executable formal semantics for llvm ir. Proceedings of the ACM on Programming Languages, 5(ICFP), 2021. Google Scholar
  60. Yannick Zakowski, Paul He, Chung-Kil Hur, and Steve Zdancewic. An equational theory for weak bisimulation via generalized parameterized coinduction. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), January 2020. Google Scholar
  61. Steve Zdancewic and Andrew C Myers. Secure information flow via linear continuations. Higher-Order and Symbolic Computation, 15(2-3), 2002. URL: https://doi.org/10.1023/A:1020843229247.
  62. Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazières. Making information flow explicit in HiStar. Communications of the ACM, 54(11):93-101, November 2011. URL: https://doi.org/10.1145/2018396.2018419.
  63. Danfeng Zhang, Aslan Askarov, and Andrew C. Myers. Language-based control and mitigation of timing channels. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2012. URL: https://doi.org/10.1145/2254064.2254078.
  64. Lantian Zheng and Andrew C. Myers. End-to-end availability policies and noninterference. In IEEE Computer Security Foundations Workshop (CSFW), 2005. URL: https://doi.org/10.1109/CSFW.2005.16.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact