A Formal Development Cycle for Security Engineering in Isabelle
This work addresses security engineering for system developers by providing a formal framework, but it appears incremental as it builds on existing Isabelle Infrastructure tools.
The paper tackles the problem of formalizing security engineering processes by introducing a Refinement-Risk Cycle based on refinement in Isabelle, which integrates attack analysis and security refinement for system specifications, demonstrated through an IoT healthcare case study with GDPR and blockchain.
In this paper, we show a security engineering process based on a formal notion of refinement fully formalized in the proof assistant Isabelle. This Refinement-Risk Cycle focuses on attack analysis and security refinement supported by interactive theorem proving. Since we use a fully formalized model of infrastructures with actors and policies we can support a novel way of formal security refinement for system specifications. This formal process is built practically as an extension to the Isabelle Infrastructure framework with attack trees. We define a formal notion of refinement on infrastructure models. Thanks to the formal foundation of Kripke structures and branching time temporal logic in the Isabelle Infrastructure framework, these stepwise transformations can be interleaved with attack tree analysis thus providing a fully formal security engineering framework. The process is illustrated on an IoT healthcare case study introducing GDPR requirements and blockchain.