Formal specification, modelling and reasoning about the security of systems, software and protocols, covering the fundamental approaches, techniques and tool support.
Learn Alloy
Alloy
Alloy is an open source language and analyzer for software modeling. It has been used in a wide range of applications, from finding holes in security mechanisms to designing telephone switching networks.
Learn TLA+
Learn TLA+
TLA+ is a “formal specification language”, a means of designing systems that lets you directly test those designs. Developed by the Turing award-winner Leslie Lamport, TLA+ has been endorsed by companies like AWS, Microsoft, and Crowdstrike.
Read the CyBOK Formal Methods for Security Knowledge Area introduction
CyBOK Introduction
The Cyber Security Body Of Knowledge is a comprehensive Body of Knowledge to inform and underpin education and professional training for the cyber security sector. The CyBOK project aims to bring cyber security into line with the more established sciences by distilling knowledge from major internationally-recognised experts to form a Cyber Security Body of Knowledge that will provide much-needed foundations for this emerging topic. The project, funded by the National Cyber Security Programme, is led by the University of Bristol's Professor Awais Rashid, along with other leading cyber security experts - including Professor Andrew Martin, Professor Steve Schneider, Dr Yulia Cherdantseva, Dr Rod Chapman and Dr Marina Krotofil.