Secure information flow by self-composition
From MaRDI portal
Publication:3103613
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)
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
Unnamed Item, Verifying Procedural Programs via Constrained Rewriting Induction, An automated quantitative information flow analysis for concurrent programs, RHLE: modular deductive verification of relational \(\forall \exists\) properties, Verification conditions for source-level imperative programs, Timed hyperproperties, Product programs in the wild: retrofitting program verifiers to check information flow security, Certified verification of relational properties, Model checking algorithms for hyperproperties (invited paper), Product programs and relational program logics, Formal verification of side-channel countermeasures using self-composition, Distributed probabilistic input/output automata: expressiveness, (un)decidability and algorithms, Formalizing Probabilistic Noninterference, Is Your Software on Dope?, Modular Verification of Procedure Equivalence in the Presence of Memory Allocation, Efficient Information-Flow Verification Under Speculative Execution
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
