Document Open Access Logo

Sheaf Semantics of Termination-Insensitive Noninterference

Authors Jonathan Sterling , Robert Harper

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2022.5.pdf
  • Filesize: 0.93 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Abstraction
  • Theory of computation → Denotational semantics
  • Theory of computation → Categorical semantics
  • Theory of computation → Type theory
  • Security and privacy → Formal methods and theory of security
Keywords
  • information flow
  • noninterference
  • denotational semantics
  • phase distinction
  • Artin gluing
  • modal type theory
  • topos theory
  • synthetic domain theory
  • synthetic Tait computability

Metrics

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

Abstract

We propose a new sheaf semantics for secure information flow over a space of abstract behaviors, based on synthetic domain theory: security classes are open/closed partitions, types are sheaves, and redaction of sensitive information corresponds to restricting a sheaf to a closed subspace. Our security-aware computational model satisfies termination-insensitive noninterference automatically, and therefore constitutes an intrinsic alternative to state of the art extrinsic/relational models of noninterference. Our semantics is the latest application of Sterling and Harper’s recent re-interpretation of phase distinctions and noninterference in programming languages in terms of Artin gluing and topos-theoretic open/closed modalities. Prior applications include parametricity for ML modules, the proof of normalization for cubical type theory by Sterling and Angiuli, and the cost-aware logical framework of Niu et al. In this paper we employ the phase distinction perspective twice: first to reconstruct the syntax and semantics of secure information flow as a lattice of phase distinctions between "higher" and "lower" security, and second to verify the computational adequacy of our sheaf semantics with respect to a version of Abadi et al.’s dependency core calculus to which we have added a construct for declassifying termination channels.

Cite As Get BibTex

Jonathan Sterling and Robert Harper. Sheaf Semantics of Termination-Insensitive Noninterference. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSCD.2022.5

Author Details

Jonathan Sterling
  • Department of Computer Science, Aarhus University, Denmark
Robert Harper
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • Sterling, Jonathan: This work was supported by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation.
  • Harper, Robert: This research was sponsored by the United States Air Force Office of Scientific Research awards FA95502110009 and FA9550-21-1-0385 (Tristan Nguyen, program manager). The views and conclusions contained in this document are those of the author and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, the U.S. government or any other entity.

Acknowledgements

We are grateful for insightful conversations with Aslan Askarov, Stephanie Balzer, Lars Birkedal, Martín Escardó, Marcelo Fiore, Daniel Gratzer, and Tom de Jong. Thanks to Jamie Vicary for funding a visit to Cambridge during which the first author learned some of the tools needed to complete this work satisfactorily. We thank Carlos Tomé Cortiñas, Fabian Ruch, and Sandro Stucki for proof-reading.

References

  1. Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. A core calculus of dependency. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '99, pages 147-160, San Antonio, Texas, USA, 1999. Association for Computing Machinery. URL: https://doi.org/10.1145/292540.292555.
  2. Mathieu Anel and André Joyal. Topo-logie. In Mathieu Anel and Gabriel Catren, editors, New Spaces in Mathematics: Formal and Conceptual Reflections, volume 1, chapter 4, pages 155-257. Cambridge University Press, 2021. URL: https://doi.org/10.1017/9781108854429.007.
  3. Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier. Théorie des topos et cohomologie étale des schémas, volume 269, 270, 305 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1972. Séminaire de Géométrie Algébrique du Bois-Marie 1963-1964 (SGA 4), Dirigé par M. Artin, A. Grothendieck, et J.-L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat. Google Scholar
  4. Steve Awodey. A Quillen model structure on the category of cartesian cubical sets. Unpublished notes, 2021. URL: https://github.com/awodey/math/blob/e8c715cc5cb6a966e736656bbe54d0483f9650fc/QMS/qms.pdf.
  5. Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:17, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.23.
  6. William J. Bowman and Amal Ahmed. Noninterference for free. In Kathleen Fisher and John H. Reppy, editors, Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, pages 101-113. Association for Computing Machinery, 2015. URL: https://doi.org/10.1145/2784731.2784733.
  7. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: a constructive interpretation of the univalence axiom. IfCoLog Journal of Logics and their Applications, 4(10):3127-3169, November 2017. URL: http://arxiv.org/abs/1611.02108.
  8. Tom de Jong and Martín Hötzel Escardó. Domain Theory in Constructive and Predicative Univalent Foundations. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1-28:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.28.
  9. M. Fiore, G. Plotkin, and J. Power. Complete cuboidal sets in axiomatic domain theory. In Logic in Computer Science, Symposium on, page 268, Los Alamitos, CA, USA, July 1997. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.1997.614954.
  10. Marcelo Fiore. Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, University of Edinburgh, November 1994. URL: https://era.ed.ac.uk/handle/1842/406.
  11. Marcelo P. Fiore. An enrichment theorem for an axiomatisation of categories of domains and continuous functions. Mathematical Structures in Computer Science, 7(5):591-618, October 1997. URL: https://doi.org/10.1017/S0960129597002429.
  12. Marcelo P. Fiore and Gordon D. Plotkin. An extension of models of axiomatic domain theory to models of synthetic domain theory. In Dirk van Dalen and Marc Bezem, editors, Computer Science Logic, 10th International Workshop, CSL '96, Annual Conference of the EACSL, Utrecht, The Netherlands, September 21-27, 1996, Selected Papers, volume 1258 of Lecture Notes in Computer Science, pages 129-149. Springer, 1996. URL: https://doi.org/10.1007/3-540-63172-0_36.
  13. Marcelo P. Fiore and Giuseppe Rosolini. The category of cpos from a synthetic viewpoint. In Stephen D. Brookes and Michael W. Mislove, editors, Thirteenth Annual Conference on Mathematical Foundations of Progamming Semantics, MFPS 1997, Carnegie Mellon University, Pittsburgh, PA, USA, March 23-26, 1997, volume 6 of Electronic Notes in Theoretical Computer Science, pages 133-150. Elsevier, 1997. URL: https://doi.org/10.1016/S1571-0661(05)80165-3.
  14. Marcelo P. Fiore and Giuseppe Rosolini. Two models of synthetic domain theory. Journal of Pure and Applied Algebra, 116(1):151-162, 1997. URL: https://doi.org/10.1016/S0022-4049(96)00164-8.
  15. Marcelo P. Fiore and Giuseppe Rosolini. Domains in H. Theoretical Computer Science, 264(2):171-193, August 2001. URL: https://doi.org/10.1016/S0304-3975(00)00221-8.
  16. Peter Freyd. On proving that 𝟏 is an indecomposable projective in various free categories. Unpublished manuscript, 1978. Google Scholar
  17. Daniel Gratzer. Normalization for multimodal type theory. To appear, Symposium on Logic in Computer Science Logic (LICS) '22, 2021. URL: http://arxiv.org/abs/2106.01414.
  18. Daniel Gratzer and Lars Birkedal. A stratified approach to Löb induction. To appear, International Conference on Formal Structures for Computation and Deduction (FSCD) '22, 2022. URL: https://jozefg.github.io/papers/a-stratified-approach-to-lob-induction.pdf.
  19. Daniel Gratzer, Michael Shulman, and Jonathan Sterling. Strict universes for Grothendieck topoi. Unpublished manuscript, February 2022. URL: https://doi.org/10.48550/arXiv.2202.12012.
  20. Daniel Gratzer and Jonathan Sterling. Syntactic categories for dependent type theory: sketching and adequacy. Unpublished manuscript, 2020. URL: http://arxiv.org/abs/2012.10783.
  21. Martin Hofmann and Thomas Streicher. Lifting Grothendieck universes. Unpublished note, 1997. URL: https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf.
  22. J. M. E. Hyland. First steps in synthetic domain theory. In Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini, editors, Category Theory, pages 131-156, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. Google Scholar
  23. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium: Volumes 1 and 2. Number 43 in Oxford Logical Guides. Oxford Science Publications, 2002. Google Scholar
  24. Chris Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of Univalent Foundations (after Voevodsky). Journal of the European Mathematical Society, 23:2071-2126, March 2021. URL: https://doi.org/10.4171/JEMS/1050.
  25. G. A. Kavvos. Modalities, cohesion, and information flow. Proceedings of the ACM on Programming Languages, 3(POPL), January 2019. URL: https://doi.org/10.1145/3290333.
  26. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of anonymous existence in Martin-Löf type theory. Logical Methods in Computer Science, 13(1):1-36, March 2017. URL: https://doi.org/10.23638/LMCS-13(1:15)2017.
  27. F. William Lawvere. Functorial Semantics of Algebraic Theories. Reprints in Theory and Applications of Categories, 4:1-121, 2004. URL: http://tac.mta.ca/tac/reprints/articles/5/tr5.pdf.
  28. F. William Lawvere. Axiomatic cohesion. Theory and Applications of Categories, 19:41-49, June 2007. URL: http://www.tac.mta.ca/tac/volumes/19/3/19-03.pdf.
  29. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis (Semantics Structures in Computation, V. 2). Kluwer Academic Publishers, Norwell, MA, USA, 2004. Google Scholar
  30. Cristina Matache, Sean Moss, and Sam Staton. Recursion and Sequentiality in Categories of Sheaves. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), volume 195 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:22, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.25.
  31. Yue Niu, Jonathan Sterling, Harrison Grodin, and Robert Harper. A cost-aware logical framework. Proceedings of the ACM on Programming Languages, 6(POPL), January 2022. URL: https://doi.org/10.1145/3498670.
  32. Ian Orton and Andrew M. Pitts. Axioms for modelling cubical type theory in a topos. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 24:1-24:19, Dagstuhl, Germany, 2016. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.24.
  33. Susan Owicki and David Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319-340, December 1976. URL: https://doi.org/10.1007/BF00268134.
  34. Wesley Phoa. Domain Theory in Realizability Toposes. PhD thesis, University of Edinburgh, July 1991. Google Scholar
  35. Bernhard Reus. Program Verification in Synthetic Domain Theory. PhD thesis, Ludwig-Maximilians-Universität München, München, November 1995. Google Scholar
  36. Bernhard Reus. Synthetic domain theory in type theory: Another logic of computable functions. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics, pages 363-380, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0105416.
  37. Bernhard Reus. Formalizing synthetic domain theory. Journal of Automated Reasoning, 23(3):411-444, 1999. URL: https://doi.org/10.1023/A:1006258506401.
  38. Bernhard Reus and Thomas Streicher. Naïve synthetic domain theory - a logical approach. Unpublished manuscript, September 1993. Google Scholar
  39. Bernhard Reus and Thomas Streicher. General synthetic domain theory - a logical approach. Mathematical Structures in Computer Science, 9(2):177-223, 1999. URL: https://doi.org/10.1017/S096012959900273X.
  40. Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures, 1:147-224, 2017. URL: http://arxiv.org/abs/1705.07442.
  41. Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. URL: https://doi.org/10.23638/LMCS-16(1:2)2020.
  42. Guiseppe Rosolini. Continuity and effectiveness in topoi. PhD thesis, University of Oxford, 1986. Google Scholar
  43. Patrick Schultz and David I. Spivak. Temporal Type Theory, volume 29 of Progress in Computer Science and Applied Logic. Birkhäuser Basel, 2019. URL: https://doi.org/10.1007/978-3-030-00704-1.
  44. Michael Shulman. Localization as an inductive definition, December 2011. URL: https://homotopytypetheory.org/2011/12/06/inductive-localization/.
  45. Michael Shulman. Reflective subfibrations, factorization systems, and stable units, December 2011. URL: https://golem.ph.utexas.edu/category/2011/12/reflective_subfibrations_facto.html.
  46. Michael Shulman. The univalence axiom for elegant reedy presheaves. Homology, Homotopy and Applications, 17:81-106, 2015. URL: https://doi.org/10.4310/HHA.2015.v17.n2.a6.
  47. Michael Shulman. All (∞,1)-toposes have strict univalent universes. Unpublished manuscript, April 2019. URL: http://arxiv.org/abs/1904.07004.
  48. Jonathan Sterling. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. PhD thesis, Carnegie Mellon University, 2021. CMU technical report CMU-CS-21-142. URL: https://doi.org/10.5281/zenodo.5709838.
  49. Jonathan Sterling and Carlo Angiuli. Normalization for cubical type theory. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-15, Los Alamitos, CA, USA, July 2021. IEEE Computer Society. URL: https://doi.org/10.1109/LICS52264.2021.9470719.
  50. Jonathan Sterling and Robert Harper. Logical relations as types: Proof-relevant parametricity for program modules. Journal of the ACM, 68(6), October 2021. URL: https://doi.org/10.1145/3474834.
  51. Thomas Streicher. Universes in toposes. In Laura Crosilla and Peter Schuster, editors, From Sets and Types to Topology and Analysis: Towards practical foundations for constructive mathematics, volume 48 of Oxford Logical Guides, pages 78-90. Oxford University Press, Oxford, 2005. URL: https://doi.org/10.1093/acprof:oso/9780198566519.001.0001.
  52. Thomas Streicher. A model of type theory in simplicial sets: A brief introduction to voevodsky’s homotopy type theory. Journal of Applied Logic, 12(1):45-49, 2014. URL: https://doi.org/10.1016/j.jal.2013.04.001.
  53. Paul Taylor. The fixed point property in synthetic domain theory. In [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pages 152-160, 1991. URL: https://doi.org/10.1109/LICS.1991.151640.
  54. Stephen Tse and Steve Zdancewic. Translating dependency into parametricity. In Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, pages 115-125, Snow Bird, UT, USA, 2004. Association for Computing Machinery. URL: https://doi.org/10.1145/1016850.1016868.
  55. Steven Vickers. Locales and toposes as spaces. In Marco Aiello, Ian Pratt-Hartmann, and Johan Van Benthem, editors, Handbook of Spatial Logics, pages 429-496. Springer Netherlands, Dordrecht, 2007. URL: https://doi.org/10.1007/978-1-4020-5587-4_8.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact