Formal Methods and CyberSecurity

TL;DR

This paper explores the potential of formal methods to enhance cybersecurity, arguing that their application should extend beyond safety-critical systems to improve trust and security in broader contexts.

Contribution

It advocates for expanding the use of formal methods in cybersecurity beyond safety-critical applications, highlighting the need for better tools and broader adoption.

Findings

Formal methods are effective in safety-critical systems.

Current limitations restrict formal methods to safety-critical contexts.

Broader application of formal methods could improve cybersecurity trust.

Abstract

Formal methods have been largely thought of in the context of safety-critical systems, where they have achieved major acceptance. Tens of millions of people trust their lives every day to such systems, based on formal proofs rather than ``we haven't found a bug'' (yet!). Why is ``we haven't found a bug'' an acceptable basis for systems trusted with hundreds of millions of people's personal data? This paper looks at some of the issues in CyberSecurity, and the extent to which formal methods, ranging from ``fully verified'' to better tool support, could help. Alas The Royal Society (2016) only recommended formal methods in the limited context of ``safety critical applications'': we suggest this is too limited.