Security Engineering in IIIf, Part II -- Refinement and Noninterference

TL;DR

The paper tackles the challenge of preserving information-flow security under refinement in complex IIIf infrastructures by extending IIIf with Information Flow Control and introducing a shadow-based notion of ignorance. It formalizes a security-preserving refinement framework and proves that IFC coincides with Noninterference, enabling a refinement-preserving security analysis. The flight-radar case study demonstrates how implicit information flows arise and how a shadow-based approach can ensure secure refinements, supported by a formal refinement theorem. The work advances security engineering in IIIf by providing a principled method to reason about refinement while maintaining information-flow guarantees, with practical implications for privacy-preserving infrastructure design.

Abstract

In this paper, we add a second part to the process of Security Engineering to the Isabelle Insider and Infrastructure framework (IIIf) [31,16] by addressing an old difficult task of refining Information Flow Security (IFC). We address the classical notion of Noninterference representing absolute security in the sense of absence of information flows to lower levels. This notion is known to be not preserved by specification refinements in general, a phenomenon known as "refinement paradox" [33]. We use a solution for this problem that has been given by Morgan [33] for the refinement calculus for sequential program specifications and generalize it to general specifications of Infrastructures with actors, decentralization and policies in the IIIf. As a running example to illustrate the problem, the concepts and the solution, we use an example of a Flightradar system specification [20].

Figures (2)

• Figure 1: Structure of Isabelle Infrastructure framework (IIIf) extended with IFC for airplane monitoring.
• Figure 2: Flightradar systems publicly visualize airtraffic routes of airplanes, e.g. flightradar24 fli:24.