The CyBOK Formal Methods Knowledge Area
Prof Steve Schneider
Director of Surrey Centre for Cyber Security, University of Surrey
The Cyber Security Body of Knowledge (CyBOK) is a project funded by the UK National Cyber Security Centre, to provide a body of work encapsulating the foundational knowledge for the emerging discipline of Cyber Security. Version 1.0 of CyBOK was released in October 2019, and an updated Version 1.1 was released in July 2021, which introduced two new chapters including a new chapter on Formal Methods for Security. The aim of Formal Methods is to introduce rigorous reasoning about systems based on discrete mathematics and logic, enabling particular (security) properties to be proven for systems and components. Formal Methods have been developing within Computer Science for over half a century, and have reached a level of maturity and tool support that mean they are now being used to verify critical systems. This talk will give an introduction to the content of the new CyBOK chapter which gives a broad overview of the variety of approaches available and what they actually offer. It will cover the foundations of the topic, in terms of approaches to specification, verification and tools, and also the application of Formal Methods at various levels of the system stack: hardware, protocols, software and systems, and configuration.