Secure information flow by self-composition
From MaRDI portal
Recommendations
Cites work
- A logic for information flow in object-oriented programs
- A semantic approach to secure information flow
- An Axiomatic Approach to Information Flow in Programs
- An axiomatic basis for computer programming
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Certification of programs for secure information flow
- Decidability and proof systems for language-based noninterference relations
- Integration of a Security Type System into a Program Logic
- Preserving Secrecy Under Refinement
- Relational separation logic
- Simple relational correctness proofs for static analyses and program transformations
- Soundness and Completeness of an Axiom System for Program Verification
- The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
Cited in
(46)- Certified verification of relational properties
- Model checking algorithms for hyperproperties (invited paper)
- Product programs and relational program logics
- Mediating secure information flow policies
- Formal verification of side-channel countermeasures using self-composition
- Distributed probabilistic input/output automata: expressiveness, (un)decidability and algorithms
- A certificate infrastructure for machine-checked proofs of conditional information flow
- Formalizing probabilistic noninterference
- Compositional methods for information-hiding
- Is Your Software on Dope?
- Modular verification of procedure equivalence in the presence of memory allocation
- Compiling Information-Flow Security to Minimal Trusted Computing Bases
- Self-adaptation and secure information flow in multiparty communications
- Efficient Information-Flow Verification Under Speculative Execution
- A Principled Approach to Tracking Information Flow in the Presence of Libraries
- Hoare logic for disjunctive information flow
- Combining Different Proof Techniques for Verifying Information Flow Security
- Verification conditions for source-level imperative programs
- Relational verification via invariant-guided synchronization
- Model-driven information flow security for component-based systems
- Paralocks, role-based information flow control and beyond
- Verifying procedural programs via constrained rewriting induction
- Self-composition by symbolic execution
- A verified information-flow architecture
- Static Analysis
- Programming Languages and Systems
- Lazy self-composition for security verification
- 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
- Software Verification of Hyperproperties Beyond k-Safety
- Explaining Hyperproperty Violations
- AutoHyper: explicit-state model checking for HyperLTL
- Certifying the fairness of KNN in the presence of dataset bias
- Searching for ribbon-shaped paths in fair transition systems
- Analysis of software patches using numerical abstract interpretation
- Abstract semantic dependency
- Alignment complete relational Hoare logics for some and all
- Predicate abstraction for hyperliveness verification
- Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties
- Timed hyperproperties
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Arrows for secure information flow
This page was built for publication: Secure information flow by self-composition
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3103613)
