Document Open Access Logo

Bounded-Deducibility Security (Invited Paper)

Authors Andrei Popescu , Thomas Bauereiss, Peter Lammich

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.3.pdf
  • Filesize: 0.8 MB
  • 20 pages

Document Identifiers

Author Details

Andrei Popescu
  • Department of Computer Science, University of Sheffield, UK
Thomas Bauereiss
  • Department of Computer Science and Technology, University of Cambridge, UK
Peter Lammich
  • Department of Computer Science, University of Twente, The Netherlands

Funding

The work presented here has been supported by: EPSRC through the grant "Verification of Web-based Systems (VOWS)" (EP/N019547/1); DFG through the grants "Security Type Systems and Deduction" (Ni 491/13-2) and "MORES - Modelling and Refinement of Security Requirements on Data and Processes (Hu 737/5-2)", part of "RS³ - Reliably Secure Software Systems" (SPP 1496); VeTSS through the grant "Formal Verification of Information Flow Security for Relational Databases"; Innovate UK through the Knowledge Transfer Partnership 010041 between Caritas Anchor House and Middlesex University: "The Global Noticeboard (GNB): a verified social media platform with a charitable, humanitarian purpose".

Acknowledgements

We are fortunate to have collaborated with some excellent researchers and developers on various parts of the implementation and verification work based on BD security: Sergey Grebenshchikov, Ping Hou, Sudeep Kanav and Ondřej Kunčar have contributed to CoCon, while Armando Pesenti Gritti and Franco Raimondi have contributed to CoSMed and CoSMeDis. We thank this paper’s reviewers for their helpful comments and suggestions.

Cite As Get BibTex

Andrei Popescu, Thomas Bauereiss, and Peter Lammich. Bounded-Deducibility Security (Invited Paper). In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.3

Abstract

We describe Bounded-Deducibility (BD) security, an expressive framework for the specification and verification of information-flow security. The framework grew by confronting concrete challenges of specifying and verifying fine-grained confidentiality properties in some realistic web-based systems. The concepts and theorems that constitute this framework have an eventful history of such "confrontations", often involving trial and error, which are reported in previous papers. This paper is the first to focus on the framework itself rather than the case studies, gathering in one place all the abstract results about BD security.

Subject Classification

ACM Subject Classification
  • Security and privacy → Formal security models
  • Security and privacy → Logic and verification
  • Security and privacy → Security requirements
Keywords
  • Information-flow security
  • Unwinding proof method
  • Compositionality
  • Verification

Metrics

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

References

  1. The Diaspora project. https://diasporafoundation.org/, 2016.
  2. The AngularJS Web Framework, 2021. URL: https://angularjs.org/.
  3. Aslan Askarov and Stephen Chong. Learning is change in knowledge: Knowledge-based security for dynamic policies. In CSF, pages 308-322, 2012. Google Scholar
  4. Aslan Askarov and Andrew C. Myers. Attacker control and impact for confidentiality and integrity. Logical Methods in Computer Science, 7(3), 2011. Google Scholar
  5. Aslan Askarov and Andrei Sabelfeld. Gradual release: Unifying declassification, encryption and key release policies. In IEEE Symposium on Security and Privacy, pages 207-221, 2007. Google Scholar
  6. Aslan Askarov and Andrei Sabelfeld. Tight enforcement of information-release policies for dynamic languages. In CSF, pages 43-59, 2009. Google Scholar
  7. Thomas Bauereiss, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. CoSMed: A Confidentiality-Verified Social Media Platform. In ITP, 2016. Google Scholar
  8. Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. CoSMeDis: A distributed social media platform with formally verified confidentiality guarantees. In IEEE Symposium on Security and Privacy, pages 729-748, 2017. Google Scholar
  9. Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. CoSMed: A Confidentiality-Verified Social Media Platform. J. Autom. Reasoning, 61(1-4):113-139, 2018. Google Scholar
  10. Thomas Bauereiss and Andrei Popescu. Compositional BD Security. Archive of Formal Proofs, 2021. URL: https://www.isa-afp.org/entries/Compositional_BD_Security.html.
  11. Thomas Bauereiss and Andrei Popescu. CoSMed: A confidentiality-verified social media platform. Archive of Formal Proofs, 2021. URL: https://www.isa-afp.org/entries/CoSMed.html.
  12. Thomas Bauereiss and Andrei Popescu. CoSMeDis: A confidentiality-verified distributed social media platform. Archive of Formal Proofs, 2021. URL: https://www.isa-afp.org/entries/CoSMeDis.html.
  13. Annalisa Bossi, Damiano Macedonio, Carla Piazza, and Sabina Rossi. Information flow in secure contexts. Journal of Computer Security, 13(3):391-422, 2005. URL: http://content.iospress.com/articles/journal-of-computer-security/jcs235.
  14. Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In POST, pages 265-284, 2014. Google Scholar
  15. Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe, and Helmut Seidl. Model checking information flow in reactive systems. In VMCAI, pages 169-185, 2012. Google Scholar
  16. Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for model checking HyperLTL and HyperCTL*. In International Conference on Computer Aided Verification, pages 30-48. Springer, 2015. Google Scholar
  17. Riccardo Focardi and Roberto Gorrieri. Classification of security properties (Part I: Information flow). In FOSAD, pages 331-396, 2000. Google Scholar
  18. Joseph A. Goguen and José Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11-20, 1982. Google Scholar
  19. Joseph A. Goguen and José Meseguer. Unwinding and inference control. In IEEE Symposium on Security and Privacy, pages 75-87, 1984. Google Scholar
  20. Florian Haftmann. Code Generation from Specifications in Higher-Order Logic. Ph.D. thesis, Technische Universität München, 2009. Google Scholar
  21. Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In FLOPS 2010, pages 103-117, 2010. Google Scholar
  22. Joseph Y. Halpern and Kevin R. O'Neill. Secrecy in multiagent systems. ACM Trans. Inf. Syst. Secur., 12(1), 2008. Google Scholar
  23. Sudeep Kanav, Peter Lammich, and Andrei Popescu. A conference management system with verified document confidentiality. In CAV, pages 167-183, 2014. Google Scholar
  24. Heiko Mantel. Possibilistic definitions of security - an assembly kit. In CSFW, pages 185-199, 2000. Google Scholar
  25. Heiko Mantel. On the composition of secure systems. In IEEE Symposium on Security and Privacy, pages 88-101, 2002. Google Scholar
  26. Heiko Mantel. A Uniform Framework for the Formal Specification and Verification of Information Flow Security. PhD thesis, University of Saarbrücken, 2003. Google Scholar
  27. Daryl McCullough. Specifications for multi-level security and a hook-up property. In IEEE Symposium on Security and Privacy, 1987. Google Scholar
  28. Daryl McCullough. A hookup theorem for multilevel security. IEEE Trans. Software Eng., 16(6):563-568, 1990. Google Scholar
  29. John McLean. Security models. In Encyclopedia of Software Engineering, 1994. Google Scholar
  30. Toby C. Murray, Andrei Sabelfeld, and Lujo Bauer. Special issue on verified information flow security. Journal of Computer Security, 25(4-5):319-321, 2017. Google Scholar
  31. Tobias Nipkow and Gerwin Klein. Concrete Semantics: With Isabelle/HOL. Springer, 2014. Google Scholar
  32. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  33. Andrei Popescu, Johannes Hölzl, and Tobias Nipkow. Proving concurrent noninterference. In CPP, pages 109-125, 2012. Google Scholar
  34. Andrei Popescu, Johannes Hölzl, and Tobias Nipkow. Formalizing probabilistic noninterference. In CPP, pages 259-275. Springer, 2013. Google Scholar
  35. Andrei Popescu and Peter Lammich. Bounded-deducibility security. Archive of Formal Proofs, 2014. URL: https://www.isa-afp.org/entries/Bounded_Deducibility_Security.html.
  36. Andrei Popescu and Peter Lammich. CoCon: A confidentiality-verified conference management system. Archive of Formal Proofs, 2021. URL: https://www.isa-afp.org/entries/CoCon.html.
  37. Andrei Popescu, Peter Lammich, and Ping Hou. CoCon: A conference management system with formally verified document confidentiality. J. Autom. Reason., 65(2):321-356, 2021. Google Scholar
  38. Markus N. Rabe, Peter Lammich, and Andrei Popescu. A shallow embedding of HyperCTL. Archive of Formal Proofs, 2014, 2014. Google Scholar
  39. Willard Rafnsson and Andrei Sabelfeld. Compositional information-flow security for interactive systems. In CSF, pages 277-292, 2014. Google Scholar
  40. Yoram Moses Ronald Fagin, Joseph Y. Halpern and Moshe Vardi. Reasoning about knowledge. MIT Press, 2003. Google Scholar
  41. John Rushby. Noninterference, transitivity, and channel-control security policies. Technical report, Computer Science Laboratory SRI International, December 1992. URL: http://www.csl.sri.com/papers/csl-92-2/.
  42. Andrei Sabelfeld and Andrew C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5-19, 2003. Google Scholar
  43. Andrei Sabelfeld and David Sands. Probabilistic noninterference for multi-threaded programs. In CSFW, pages 200-214, 2000. Google Scholar
  44. Andrei Sabelfeld and David Sands. Declassification: Dimensions and principles. Journal of Computer Security, 17(5):517-548, 2009. Google Scholar
  45. The Scalatra Web Framework, 2021. URL: http://scalatra.org/.
  46. D. Sutherland. A model of information. In 9th National Security Conf., pages 175-183, 1986. Google Scholar
  47. Dennis Volpano, Geoffrey Smith, and Cynthia Irvine. A sound type system for secure flow analysis. Journal of Computer Security, 4(2,3):167-187, 1996. Google Scholar
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