Static Analysis

DOI10.1007/11547662MaRDI QIDQ5897442zbMATH OpenOpenAlexFDO

Authors Tachio Terauchi, Alex Aiken

Publication date 31 October 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11547662

Mathematics Subject Classification ID

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

Recommendations

• Secure information flow by self-composition
• Lazy self-composition for security verification
• Secure Information Flow as a Safety Property
• A semantic approach to secure information flow
• Security through safety. An approach to information flow control based on derivation of safety properties from a characterisation of insecure behaviour

Cited in

(29)

• Automated enforcement for relaxed information release with reference points
• Security design with interim public information
• Compositional model checking for multi-properties
• Decomposing data structure commutativity proofs with \(mn\)-differencing
• Product programs and relational program logics
• Formal verification of side-channel countermeasures using self-composition
• Precise quantitative information flow analysis -- a symbolic approach
• Quantitative information flow as safety and liveness hyperproperties
• Is Your Software on Dope?
• Modular verification of procedure equivalence in the presence of memory allocation
• Relational decomposition
• Secure information flow by self-composition
• Efficient Information-Flow Verification Under Speculative Execution
• Information theory and security: Quantitative information flow
• scientific article; zbMATH DE number 7319029 (Why is no real title available?)
• Relational verification via invariant-guided synchronization
• Verifying procedural programs via constrained rewriting induction
• Self-composition by symbolic execution
• Lazy self-composition for security verification
• Symbolic abstract heaps for polymorphic information-flow guard inference
• Sound symbolic execution via abstract interpretation and its application to security
• RHLE: modular deductive verification of relational \(\forall \exists\) properties
• Alignment complete relational Hoare logics for some and all
• Relational bytecode correlations
• Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties
• Product programs in the wild: retrofitting program verifiers to check information flow security
• Constraint-based relational verification
• Observational purity and encapsulation
• Model checking the observational determinism security property using PROMELA and SPIN

Describes a project that uses

Uses Software

• SLAM

This page was built for publication: Static Analysis

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