2024/12/14 by Florian Kammüller, Kammüller, Florian
Computer Science · #FOS: Computer and information sciences #Information and Cyber Security #Logic in Computer Science (cs.LO) #Network Security and Intrusion Detection #Security and Verification in Computing #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2412.10949
openalex publication_date 2024/12/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In this paper, we extend the process of Security Engineering for the Isabelle Insider and Infrastructure framework (IIIf) by introducing Information Flow Security (IFC). To formalize the absence of information flows to lower levels, we use a concept of a ``Shadow'' inspired by Morgan. We relate it to the classical notion of Noninterference (NI) formalised in the IIIf. Apart from being an elegant concept, Morgan's concept of a shadow is interesting because it addresses a phenomenon called the ``refinement paradox'': information flow security is known to be not preserved by specification refinements in general. We use the formalisation of shadow and its equivalence to NI to exhibit conditions for a secure refinement for IIIf. As a running example to illustrate the problem, the concepts and the solution, we use an example of a flightradar system specification.