CS886 - Advanced Security-by-Design

Aims and Objectives

This course aims to equip students with an understanding of how formal methods can be applied at design time to address software security issues. By using mathematically grounded techniques, students will learn how to eliminate common classes of vulnerabilities, ensure program correctness, and enable more focused testing of other system aspects.

Learning Outcomes

At the end of this class learners should be able:

1. to understand the different ways in which software can be insecure by design
2. to understand the role and limitations that formal methods can have in addressing issues of software (in)security at design time
3. to understand different approaches to formally reasoning about software programs at design time
4. to apply formal methods at design time to mitigate known software vulnerabilities
5. to identify software technologies that realise secure-by-design approaches
6. to design and implement significant software that is ‘Secure-by-Design' and know where the built software is secure and where further analysis is required

Students will also develop transferable skills such as:

1. develop problem-solving skills in applying formal methods to solve problems in making software secure by design
2. develop critical thinking skills when comparing various formal method techniques to address issues of software security
3. be creative in learning how to approach the application of formal methods to address software security issues

Syllabus

The course covers both theory and practice: key principles and paradigms, and their application in design and implementation. Practically, students will work with Dafny and Idris to build verified programs using modern formal techniques.

• Sofware (In)Security and Formal Methods
  • How software can fail, what formal methods are and how they can and cannot help.
• Secure-by-Design Approaches
  • Design-by-Contract using Dafny; Correctness-by-Construction using Idris;
• Applications
  • Memory Safety; Data Security; Information Security; 
  • Securing Program Behaviour and Communication;
  • Programming Language Security and Compiler Verification;

Recommended Reading

This list is indicative only – the class lecturer may recommend alternative reading material. Please do not purchase any of the reading material listed below until you have confirmed with the class lecturer that it will be used for this class.

This course will preference, where suitable, copy-left and freely available material. 

• 'Three Times' the ‘official’ pre-reading for the module.
• Pre-existing teaching materials for Dafny and Idris.
• Open access academic papers and books. 
  • Aaron Stump, 2016, Verified Functional Programming in Agda. https://dl.acm.org/doi/book/10.1145/2841316
  • Programming Language Foundations in Agda Open source online textbook. Available at: https://plfa.github.io/
• Paid books, which are also available in the University Library, that are of interest include but not limited to the following:
  • K Rustan M. Leino, 2023, Program Proofs, MIT Press https://mitpress.mit.edu/9780262546232/program-proofs/ 
  • Edwin Brady, 2017, Type-Driven Development with Idris, Manning. https://www.manning.com/books/type-driven-development-with-idris

Last updated: 2026-08-25 11:46:35