Document Open Access Logo

Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security

Authors Robert Sison , Toby Murray

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.27.pdf
  • Filesize: 0.61 MB
  • 19 pages

Document Identifiers

Author Details

Robert Sison
  • Data61, CSIRO, Australia
  • UNSW Sydney, Australia
Toby Murray
  • University of Melbourne, Australia

Funding

  • Sison, Robert: Australian Government RTP Scholarship & Data61 Research Project Award

Acknowledgements

We would like to thank our anonymous reviewers, as well as Carroll Morgan, Kai Engelhardt, Gerwin Klein, Christine Rizkallah, Matthew Brecknell, Johannes Åman Pohjola, and Qian Ge, for their very helpful feedback on earlier versions of this paper.

Cite AsGet BibTex

Robert Sison and Toby Murray. Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.27

Abstract

It is common to prove by reasoning over source code that programs do not leak sensitive data. But doing so leaves a gap between reasoning and reality that can only be filled by accounting for the behaviour of the compiler. This task is complicated when programs enforce value-dependent information-flow security properties (in which classification of locations can vary depending on values in other locations) and complicated further when programs exploit shared-variable concurrency. Prior work has formally defined a notion of concurrency-aware refinement for preserving value-dependent security properties. However, that notion is considerably more complex than standard refinement definitions typically applied in the verification of semantics preservation by compilers. To date it remains unclear whether it can be applied to a realistic compiler, because there exist no general decomposition principles for separating it into smaller, more familiar, proof obligations. In this work, we provide such a decomposition principle, which we show can almost halve the complexity of proving secure refinement. Further, we demonstrate its applicability to secure compilation, by proving in Isabelle/HOL the preservation of value-dependent security by a proof-of-concept compiler from an imperative While language to a generic RISC-style assembly language, for programs with shared-memory concurrency mediated by locking primitives. Finally, we execute our compiler in Isabelle on a While language model of the Cross Domain Desktop Compositor, demonstrating to our knowledge the first use of a compiler verification result to carry an information-flow security property down to the assembly-level model of a non-trivial concurrent program.

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
  • Security and privacy → Information flow control
  • Software and its engineering → Compilers
Keywords
  • Secure compilation
  • Information flow security
  • Concurrency
  • Verification

Metrics

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

Related Versions

Supplementary Materials

References

  1. Carmine Abate, Roberto Blanco, Deepak Garg, Catalin Hritcu, Marco Patrignani, and Jérémy Thibault. Exploring Robust Property Preservation for Secure Compilation. CoRR, abs/1807.04603, 2018. URL: http://arxiv.org/abs/1807.04603.
  2. G. Barthe, B. Grégoire, and V. Laporte. Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic “Constant-Time”. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pages 328-343, July 2018. Google Scholar
  3. Gilles Barthe, Tamara Rezk, and Amitabh Basu. Security Types Preserving Compilation. Comput. Lang. Syst. Struct., 33(2):35-59, July 2007. URL: https://doi.org/10.1016/j.cl.2005.05.002.
  4. Gilles Barthe, Tamara Rezk, Alejandro Russo, and Andrei Sabelfeld. Security of Multithreaded Programs by Compilation. ACM Trans. Inf. Syst. Secur., 13(3):21:1-21:32, July 2010. URL: https://doi.org/10.1145/1805974.1805977.
  5. Mark Beaumont, Jim McCarthy, and Toby Murray. The Cross Domain Desktop Compositor: Using Hardware-Based Video Compositing for a Multi-Level Secure User Interface. In Annual Computer Security Applications Conference (ACSAC), pages 533-545, 2016. Google Scholar
  6. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, September 2010. URL: http://dl.acm.org/citation.cfm?id=1891823.1891830.
  7. Florian Dewald, Heiko Mantel, and Alexandra Weber. AVR processors as a platform for language-based security. In Computer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I, pages 427-445, 2017. URL: https://doi.org/10.1007/978-3-319-66402-6_25.
  8. Qian Ge, Yuval Yarom, Tom Chothia, and Gernot Heiser. Time Protection: the Missing OS Abstraction. In Eurosys19, Dresden, Germany, March 2019. ACM. Google Scholar
  9. Qian Ge, Yuval Yarom, and Gernot Heiser. No Security Without Time Protection: We Need a New Hardware-Software Contract. In Asia-Pacific Workshop on Systems (APSys), Korea, August 2018. ACM SIGOPS. Google Scholar
  10. Joseph Goguen and José Meseguer. Security Policies and Security Models. In Proceedings of the IEEE Symposium on Security and Privacy, pages 11-20, Oakland, California, USA, April 1982. IEEE Computer Society. Google Scholar
  11. Cliff B. Jones. Development Methods for Computer Programs including a Notion of Interference. D.Phil. thesis, University of Oxford, June 1981. Google Scholar
  12. Thierry Kaufmann, Hervé Pelletier, Serge Vaudenay, and Karine Villegas. When Constant-Time Source Yields Variable-Time Binary: Exploiting Curve25519-donna Built with MSVC 2015. In Cryptology and Network Security, pages 573-582, Cham, 2016. Springer International Publishing. Google Scholar
  13. Paul Kocher, Jann Horn, Anders Fogh, , Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. Spectre Attacks: Exploiting Speculative Execution. In 40th IEEE Symposium on Security and Privacy (S&P'19), 2019. Google Scholar
  14. Ramana Kumar, Magnus Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179-191, San Diego, January 2014. ACM Press. Google Scholar
  15. Xavier Leroy. A Formally Verified Compiler Back-end. J. Autom. Reason., 43(4):363-446, December 2009. URL: https://doi.org/10.1007/s10817-009-9155-4.
  16. Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Anders Fogh, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. Meltdown: Reading Kernel Memory from User Space. In 27th USENIX Security Symposium (USENIX Security 18), 2018. Google Scholar
  17. Andreas Lochbihler. Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler. Journal of Automated Reasoning, 61(1):243-332, June 2018. URL: https://doi.org/10.1007/s10817-018-9452-x.
  18. Luísa Lourenço and Luís Caires. Dependent Information Flow Types. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 317-328, Mumbai, India, January 2015. ACM. Google Scholar
  19. Heiko Mantel, David Sands, and Henning Sudbrock. Assumptions and Guarantees for Compositional Noninterference. In IEEE Computer Security Foundations Symposium, pages 218-232, Cernay-la-Ville, France, June 2011. IEEE. Google Scholar
  20. Toby Murray, Robert Sison, and Kai Engelhardt. COVERN: A logic for compositional verification of information flow control. In European Symposium on Security and Privacy, London, United Kingdom, April 2018. IEEE. Google Scholar
  21. Toby Murray, Robert Sison, Edward Pierzchalski, and Christine Rizkallah. Compositional Security-Preserving Refinement for Concurrent Imperative Programs. Archive of Formal Proofs, June 2016. , Formal proof development. URL: http://isa-afp.org/entries/Dependent_SIFUM_Refinement.shtml.
  22. Toby Murray, Robert Sison, Edward Pierzchalski, and Christine Rizkallah. Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. In IEEE Computer Security Foundations Symposium, pages 417-431, Lisbon, Portugal, June 2016. Google Scholar
  23. Marco Patrignani, Amal Ahmed, and Dave Clarke. Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work. ACM Comput. Surv., 51(6):125:1-125:36, February 2019. URL: https://doi.org/10.1145/3280984.
  24. Marco Patrignani and Deepak Garg. Secure Compilation and Hyperproperty Preservation. In IEEE 30th Computer Security Foundations Symposium, CSF 2017, Santa Barbara, USA, August 21 - 25, 2017, CSF'17, 2017. Google Scholar
  25. Marco Patrignani and Deepak Garg. Robustly Safe Compilation. In Programming Languages and Systems, pages 469-498, Cham, 2019. Springer International Publishing. Google Scholar
  26. Anton Podkopaev, Ori Lahav, and Viktor Vafeiadis. Bridging the Gap Between Programming Languages and Hardware Weak Memory Models. Proc. ACM Program. Lang., 3(POPL):69:1-69:31, January 2019. URL: https://doi.org/10.1145/3290382.
  27. Andrei Sabelfeld and David Sands. Probabilistic Noninterference for Multi-Threaded Programs. In Proceedings of the 13th IEEE Workshop on Computer Security Foundations, CSFW '00, pages 200-, Washington, DC, USA, 2000. IEEE Computer Society. URL: http://dl.acm.org/citation.cfm?id=794200.795151.
  28. Mark Staples, Ross Jeffery, June Andronick, Toby Murray, Gerwin Klein, and Rafal Kolanski. Productivity for Proof Engineering. In Empirical Software Engineering and Measurement, page 15, Turin, Italy, September 2014. Google Scholar
  29. F. Del Tedesco, D. Sands, and A. Russo. Fault-Resilient Non-interference. In 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pages 401-416, June 2016. Google Scholar
  30. Danfeng Zhang, Yao Wang, G. Edward Suh, and Andrew C. Myers. A Hardware Design Language for Timing-Sensitive Information-Flow Security. In Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '15, pages 503-516, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2694344.2694372.
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 Imprint Privacy Contact