Isabelle proof for CapFlow

CapFlow is a capability-based information flow control model. Formal specifications and verifications are provided by this repo.

• Dynamic_model: An abstract security model with dynamic information flow policies. Information flow security properties are defined in this model. This file contains dynamic unwinding conditions, dynamic noninterference theory and an inference framework.
• CapFlow: A concrete execution model based-on capability. This model is instantiated from Dynamic_model and inherites the security properties of the abstract model. This file specifies kernel events and provides formal security proofs of CapFlow.

Formal specifications and proofs in pdf can be found in document.