Mechanized logical relations for termination-insensitive noninterference
| Autor: | Amin Timany, Simon Oddershede Gregersen, Johan Bay, Lars Birkedal |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Information-Flow Control
Programming language Computer science Proof assistant Iris 020207 software engineering Logical Relations 0102 computer and information sciences 02 engineering and technology Semantic data model computer.software_genre 01 natural sciences Logical relations Program Logics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Modal 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Safety Risk Reliability and Quality computer Software Program logic Impredicativity |
| Zdroj: | Gregersen, S O, Bay, J, Timany, A & Birkedal, L 2021, ' Mechanized logical relations for termination-insensitive noninterference ', Proceedings of the ACM on Programming Languages, vol. 5, no. POPL, 10 . https://doi.org/10.1145/3434291 |
| ISSN: | 2475-1421 |
| DOI: | 10.1145/3434291 |
| Popis: | We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic model of this type system and show that well-typed programs satisfy termination-insensitive noninterference. Our semantic approach supports compositional integration of syntactically well-typed and syntactically ill-typed---but semantically sound---components, which we demonstrate through several interesting examples. We define our model using logical relations on top of the Iris program logic framework; to capture termination-insensitivity, we develop a novel language-agnostic theory of Modal Weakest Preconditions. We formalize all of our theory and examples in the Coq proof assistant. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|