Formal Methods and CyberSecurity
It addresses the problem of inadequate security for personal data in cybersecurity systems, proposing a shift from incremental tool improvements to broader adoption of formal methods.
This paper examines the application of formal methods to cybersecurity, arguing that their current limited use in safety-critical systems should be expanded to protect personal data, as relying on the absence of found bugs is insufficient for systems trusted by hundreds of millions.
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.