Dependability Engineering in Isabelle

TL;DR

This paper presents a formal, cyclic development process for dependability and security systems using Isabelle, integrating attack tree analysis with refinement to improve specification accuracy and safety assurance.

Contribution

It introduces the Isabelle Infrastructure framework with a formal property-preserving refinement process combined with attack tree analysis, applicable to security and safety systems.

Findings

Extended Isabelle Infrastructure framework with new refinement and attack analysis features

Applied the process to privacy analysis of a mobile COVID-19 warning app

Demonstrated the approach's effectiveness in system specification and security verification

Abstract

In this paper, we introduce a process of formal system development supported by interactive theorem proving in a dedicated Isabelle framework. This Isabelle Infrastructure framework implements specification and verification in a cyclic process supported by attack tree analysis closely inter-connected with formal refinement of the specification. The process is cyclic: in a repeated iteration the refinement adds more detail to the system specification. It is a known hard problem how to find the next refinement step: this problem is addressed by the attack based analysis using Kripke structures and CTL logic. We call this cyclic process the Refinement-Risk cycle (RR-cycle). It has been developed for security and privacy of IoT healthcare systems initially but is more generally applicable for safety as well, that is, dependability in general. In this paper, we present the extensions to the Isabelle Infrastructure framework implementing a formal notion of property preserving refinement interleaved with attack tree analysis for the RR-cycle. The process is illustrated on the specification development and privacy analysis of the mobile Corona-virus warning app.