Decidability and proof systems for language-based noninterference relations

DOI10.1145/1111037.1111044MaRDI QIDQ5348913zbMATH OpenOpenAlexFDO

Authors Mads Dam

Publication date 21 August 2017

Published in Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1111037.1111044

zbMATH Keywords

information flowintransitive noninterferencelanguage-based securitymulti-level securitynoninterference

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Proving concurrent noninterference
• Formal verification of language-based concurrent noninterference
• Computer Science Logic
• A proof system for abstract non-interference
• Abstract non-interference

Cited in

(13)

• Redundant proofs of non-interference in Levin-Gries CSP program proofs
• Factorization of behavioral integrity
• Noninterference in a predicative polymorphic calculus for access control
• Fine-grained and coarse-grained reactive noninterference
• Secure information flow by self-composition
• Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus
• A proof system for abstract non-interference
• Proving concurrent noninterference
• May testing, non-interference, and compositionality
• Towards SOS meta-theory for language-based security
• Unwinding Conditions for Security in Imperative Languages
• Automata, Languages and Programming
• Branching bisimulation semantics enables noninterference analysis of reversible systems

This page was built for publication: Decidability and proof systems for language-based noninterference relations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5348913)