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

TL;DR

This paper extends the IIIf security framework by addressing the challenge of refining information flow security, specifically noninterference, in complex infrastructures with decentralization and policies, using a generalized solution to the refinement paradox.

Contribution

It generalizes Morgan's solution to the refinement paradox for noninterference to the IIIf framework, enabling secure refinement of specifications involving multiple actors and policies.

Findings

Successfully applied the generalized solution to a Flightradar system example

Demonstrated preservation of noninterference during specification refinement

Extended security engineering methods to complex decentralized infrastructures

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].