Teaching Formal Methods as Part of a Security Module
The computer science curriculum at the University of Exeter focuses on the applied software engineering and data science aspects. Hence, there are very few modules focusing on the foundations and theory. Instead, of having dedicated theory-focused modules, theory is embedded into applied modules. One such example is our approach of integrating formal methods, mostly in the form of model checking, into our second year undergraduate cyber security module.
In this module, we integrate a roughly three weeks long section on security protocols, with a focus on their formal modelling and formal analysis. In these three weeks, we use a holistic approach for teaching the security objectives of security protocols, their analysis of actual implementations using a network sniffer, their formal verification using a model checker (and comparing it to an approaches based on interactive theorem proving).
This approach has been developed over the course of eight years at two UK universities: The University of Sheffield and the University of Exeter. In this paper, we focus on our experience in Exeter, at which we are offering the module in the form discussed in this paper since the academic year 2019/2020. While the module usually is delivered as synchronous in-person delivery, during the COVID-19 pandemic we also delivered the module successfully as (asynchronous) remote delivery. For the remote delivery, we replaced the lectures by pre-recorded videos and the lab sessions had been taught in flipped-classroom-style, with weekly synchronous drop-in sessions offered online.
We report, in more detail, on our experience with this integrated approach in our paper at the Formal Methods Teaching Workshop (FMTea 2024) [1]. The workshop will take place on the 10th of September 2024 – feel free to join us!