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.
About Prof Steve Schneider
Steve Schneider is Professor of Secure Systems and Director of the Surrey Centre for Cyber Security at the University of Surrey, where he has been since 2004. He was previously in the Department of Computer Science at Royal Holloway, University of London over the period 1994-2004. He gained his doctorate from the University of Oxford in 1990, and held post-doctoral positions there prior to joining Royal Holloway.He has worked in the area of concurrency theory, specifically the process algebra Communicating Sequential Processes (CSP), and its timed version Timed CSP. He has also worked with the B-Method and with Event-B, their relationship to CSP, and their application to safety and security verification. From 1994 he has worked on the application of formal methods and security around modelling and verification of security protocols, and in non-interference. Since 2004 he has been working in the area of Secure Electronic Voting. He was involved in the design and development of the Prêt à Voter verifiable voting system including its implementation for use in the vVote system used in the 2014 State Election in the State of Victoria, Australia. He is currently interested in more general approaches to secure electronic voting, and the use of Distributed Ledger Technologies in this domain, and more generally.He is a member of the editorial team of the Cyber Security Body of Knowledge, and is the Editor of the Knowledge Area on Formal Methods for Security.Sponsored by
Official Media Partners
Supported by
