Abstract: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.
From: Florian Kammüller [view email]
[v1]
Sat, 14 Dec 2024 20:06:27 UTC (2,154 KB)
[v2]
Mon, 29 Jun 2026 08:55:18 UTC (2,136 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。