A Logical System for Modular Information Flow Verification

DOI10.1007/978-3-319-73721-8_20MaRDI QIDQ3296345zbMATH OpenOpenAlexFDO

Authors Adi Prabawa, Mahmudul Faisal Al Ameen, Benedict Lee, Wei-Ngan Chin

Publication date 7 July 2020

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

Full work available at URL https://doi.org/10.1007/978-3-319-73721-8_20

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• A verified information-flow architecture
• Computing Information Flow Using Symbolic Model-Checking
• A proof system for information flow security
• Static Analysis
• An automata based approach for verifying information flow properties
• An algebraic approach for reasoning about information flow

Cited in

(10)

• Security through safety. An approach to information flow control based on derivation of safety properties from a characterisation of insecure behaviour
• Hybrid information flow control for low-level code
• Using dependence graphs to assist verification and testing of information-flow properties
• Information flow control in software DB units based on formal verification
• A hybrid, dynamic logic for hybrid-dynamic information flow
• Model-driven information flow security for component-based systems
• Flexible dynamic information flow control in the presence of exceptions
• Static Analysis
• Combining Different Proof Techniques for Verifying Information Flow Security
• Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays

This page was built for publication: A Logical System for Modular Information Flow Verification

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