CS886 - Advanced Security-by-Design
| TIMETABLE | TEACHING MATERIAL |
| Credits | 20 |
| Level | 5 |
| Semester | Semester 2 |
| Availability | Not available as an elective. |
| Prerequisites |
|
| Learning Activities Breakdown | Lectures: 10 x 2hrs; Revision Lecture: 1 x 1hr; Tutorials: 9 x 1hrs; Labs 10 x 2hrs; Private Study/Homework 150 hrs |
| Items of Assessment | 3 |
| Assessment | 40% Coursework (2 x 20%); 60% Exam; |
| Lecturer | Jan de Muijnck-Hughes |
Aims and Objectives
The aim of CS886 is to provide students with sufficient grounding and experience over the extent to which formal methods can provide, at design time, strong mathematical guarantees about the correctness of our software programs and prevent routinely exploited vulnerabilities from occurring.
Learning Outcomes
At the end of this class learners should be able:
- to understand the different ways in which software can be insecure by design
- to understand the role and limitations that formal methods can have in addressing issues of software (in)security at design time
- to understand different approaches to formally reasoning about software programs at design time
- to apply formal methods at design time to mitigate known software vulnerabilities
- to identify software technologies that realise secure-by-design approaches
- 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:
- develop problem-solving skills in applying formal methods to solve problems in making software secure by design
- develop critical thinking skills when comparing various formal method techniques to address issues of software security
- be creative in learning how to approach the application of formal methods to address software security issues
Syllabus
The aim of this course is to help students understand how we can use formal methods to address, at design time, issues of software (in)security. Many of the top routinely exploited vulnerabilities arise due to flaws in the software that we engineer. Although software engineering practises such as Secure Software Development Lifecycle and Test-Driven Development can help mitigate software vulnerabilities, such vulnerabilities are nonetheless routinely found and exploited. By using formal methods at design time we can provide strong mathematical guarantees that many routinely exploited vulnerabilities cannot occur as our programs are correct-by-construction, allow testing to be targeted on other aspects of the software system.
In this course, we will be covering: principles &
paradigms—exploring theoretical models and considerations; and design & implementation—how theory is used in
practice. Specifically, when exploring the practical elements we will do so through consideration of two state-of-the-art
programming languages (Dafny and Idris) that enable realisation of different formal theories to ensure that our programs are correct-by-construction.
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 availably material.
- 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 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: 2024-08-05 11:58:57