Secure information flow by self-composition

DOI10.1017/S0960129511000193zbMath1252.68072MaRDI QIDQ3103613

Gilles Barthe, Tamara Rezk, Pedro R. D'Argenio

Publication date: 8 December 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

security policiesproof carrying code

Mathematics Subject Classification ID

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

Related Items

Verifying Procedural Programs via Constrained Rewriting Induction, Timed hyperproperties, Product programs in the wild: retrofitting program verifiers to check information flow security, Product programs and relational program logics, Certified verification of relational properties, Formalizing Probabilistic Noninterference, An automated quantitative information flow analysis for concurrent programs, Symbolic abstract heaps for polymorphic information-flow guard inference, HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems, Sound symbolic execution via abstract interpretation and its application to security, RHLE: modular deductive verification of relational \(\forall \exists\) properties, Output-sensitive information flow analysis, Unnamed Item, Formal verification of side-channel countermeasures using self-composition, Verification conditions for source-level imperative programs, Is Your Software on Dope?, Modular Verification of Procedure Equivalence in the Presence of Memory Allocation, Distributed probabilistic input/output automata: expressiveness, (un)decidability and algorithms, Efficient Information-Flow Verification Under Speculative Execution, Model checking algorithms for hyperproperties (invited paper)

Cites Work

• Relational separation logic
• A semantic approach to secure information flow
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Simple relational correctness proofs for static analyses and program transformations
• Preserving Secrecy Under Refinement
• Integration of a Security Type System into a Program Logic
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• An Axiomatic Approach to Information Flow in Programs
• Certification of programs for secure information flow
• Soundness and Completeness of an Axiom System for Program Verification
• Decidability and proof systems for language-based noninterference relations
• A logic for information flow in object-oriented programs
• An axiomatic basis for computer programming