Checking and Automating Confidentiality Theory in Isabelle/UTP

TL;DR

This paper presents a formal approach to verifying confidentiality properties in programs using Isabelle/UTP, addressing theoretical issues and demonstrating practical verification of examples from Bank's confidentiality framework.

Contribution

It introduces a mechanised formalization of Bank's confidentiality theory within Isabelle/UTP and identifies theoretical issues in the original framework.

Findings

Mechanised confidentiality verification in Isabelle/UTP

Identification of theoretical issues in Bank's framework

Successful formal verification of example confidentiality properties

Abstract

The severity of recent vulnerabilities discovered on modern CPUs, e.g., Spectre [1], highlights how information leakage can have devas-tating effects to the security of computer systems. At the same time, it suggests that confidentiality should be promoted as a normal part of program verification, to discover and mitigate such vulnerabili-ties early in development. The theory we propose is primarily based on Bank's theory [2], a framework for reasoning about confidentiali-ty properties formalised in the Unifying Theories of Programming (UTP) [3]. We mechanised our encoding in the current implementa-tion of UTP in the Isabelle theorem prover, Isabelle/UTP [4]. We have identified some theoretical issues in Bank's original framework. Finally, we demonstrate how our mechanisation can be used to for-mally verify of some of the examples from Bank's work.