This project contains the Isabelle/HOL formalisation and soundness proof for an security-preserving refinement for concurrent systems. It contains two case studies, i.e., the IPC mechanism of ARINC 653 multicore and a sealed-bid auction system.
The project is developed by Isabelle/HOL 2024, older version may need some slight adjustments. You can load theorems by dragging them in the Isabelle/HOL GUI
SecurityModel : General security model for intransitive noninterference and unwinding theorem Refinement: General security-preserving refinement PiCore_Language, PiCore_Semantics: The language used to formalize security for concurrent systems PiCore_IFS : Security model for concurrent systems PiCore_Refine, PiCore_Sim: Security-Preserving refinement and unwinding-simulation for concurrent systems VHelper: Auxiliary lemmas
RG_Com, RG_Tran, RG_Hoare: Imperative Language used for case study PiCore_SIMP_Syntax, PiCore_SIMP_Ref: The interface to integrate language to our framework ARINC653_MultiCore_Que : IPC mechanism for ARINC 653 multicore Auction: Seal-bid auction system