Dependability Engineering in Isabelle
This addresses the challenge of ensuring security and privacy in IoT healthcare systems, with broader applicability to safety, though it is incremental as it extends an existing framework.
The paper tackles the problem of formal system development for dependability by introducing a cyclic process called the Refinement-Risk cycle, which integrates attack tree analysis with formal refinement in Isabelle, and demonstrates it on a mobile coronavirus warning app.
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.