In December 2019, my colleague James Davenport from the University of Bath presented our work at the 1st International Workshop on “Formal Methods — Fun for Everybody” (FMFun 2019). This paper focuses on James’ work in teaching security and formal methods, as well as linking to our wider work on computing curricula; effective learning, teaching and assessment in computing (especially for cyber security); as well as professional body degree accreditation.
The papers from this workshop have taken a while to appear in the formal Springer proceedings, but were finally published this week. The abstract of our paper is below; you can access the full paper online, or via my institutional repository:
Cybersecurity Education and Formal Methods
James H. Davenport and Tom Crick
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!); but 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 these issues in cybersecurity, and the extent to which formal methods, ranging from “fully verified” to better tool support, could help. More importantly, recent policy reports and curricula initiatives appear to recommended formal methods in the limited context of “safety critical applications”; we suggest this is too limited in scope and ambition. Not only are formal methods needed in cybersecurity, the repeated and very public weaknesses of the cybersecurity industry provide a powerful motivation for formal methods.
Keywords: Formal methods, cybersecurity, curricula
https://doi.org/10.1007/978-3-030-71374-4_8
(also see: Publications)
Digital, Data & Policy 