At the University of Strathclyde the MSc in Cyber Security is divided into three themes that each explore a different area of cyber security: Human Factors, Security-by-Design, and Systems Security.
CS886 Advanced Security-by-Design forms the second part of the Security-by-Design theme, which explores more technical elements of cyber security together with a look at the formal modelling and analysis of these technical elements.
This page provides a public description of the course and its syllabus. Students access deployed course material through our Moodle instance and the contents are not accessible to the general public.
If there are any queries or comments about the course then please do get in contact.
Aim
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 Objectives
- 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
Transferable Skills
- 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
Prerequisites
Prior to this class, students will have completed the prerequisite courses:
- Security Protocols and Threat Models
- which investigates the security of how our code interacts with other external systems;
- Information Security Fundamentals
- a theme agnostic intro course that provides introductory information about security issues affecting code;
CS886 will focus on how we can provide strong guarantees over the security of our code during its design, using well-studied mathematical techniques and their realisation in tooling.
Syllabus
- Note
- The syllabus is subject to change.
The course will be divided into three phases: Course Overview and Introduction; Security-by-Design; and Applications of Formal Methods to address issues of (In)Security. A fourth phase is a revision session.
Each of these Phases will address, in conjunction with the final written examination, Learning Objectives 1-5 and lay the foundations for addressing Learning Objective 6, which will be addressed through the assessed coursework.
Phase 1 (Week 1): Course Overview and Introduction.
The first phase of the course primarily addresses Learning Objectives 1-2, and will provide students with an understanding of how software can be insecure by design. This first phase also provides an overview of the course itself and operation. Core topics for this phase are:
Week 1a: Course Overview.
Introductory face-the-front lecture to introduce the students to the class and how it is expected to run.
Week 1b: Overview of Software (In)Security.
Detail different ways in which software can fail, and link in which the previous course in theme (Software Protocols and Threat models).
Week 1c: Introduction to Formal Methods and how they address issues of software (in)security.
This will provide an introduction to formal methods in general. Suggested topics for introduction include:
- Model Checking
- SPIN; Promela; Petri-nets; TLA+;
- Program Logics
- Proverif; Tamarin; Hoare Logics; Separation Logic;
- Type Systems
- Dependent types; Session types; linear types; TypeState; and other advanced type systems;
- Maths & Theorem Proving based approaches
- Maths; Coq; Lean4; and Isabelle;
Woven throughout this discussion will be: What can formal methods give us? (design time guarantees about software); and What formal methods can not give us (yet);
Phase 2 (Weeks 2-3): Secure-By-Design
The second phase will look at how we can use specific styles of formal methods to reason about software. For this iteration of the course, we propose focusing on: Design by Contract; and Correctness-by-Construction. Other topics may be considered in the future. The second phase of the course primarily addresses Learning Objective 2-3 and 5, and begins addressing Objective 4 through example. The foundations for Learning Objective 6 will also be given and provide students with an understanding of the different ways in which we can make software secure by design.
Week 2: Design by contract approaches
Design-by-Contract provides a style of software verification in which we use logics to reason about software properties. For example: safety; liveness; termination; et cetera. Practically, Design-By-Contract requires we specify expected and required conditions of program execution and invariants. We will introduce the theory (Hoare Logics), and mention implementations: PREfast; SAL; JML; Verifast (uses separation logic). We will pair the theoretical discussion with examples in the verification-aware programming language Dafny.
- Tutorial
- Dafny
Week 3: Correctness-by-construction
Correctness-by-Construction is a style of software verification in which we build up our software, requiring it to be correct by default. Practically, we can encode similar properties as seen with Design-By-Contract, but we can also do much more precise reasoning. We will introduce a particular theory in more depth, namely dependent types, but under the auspices of the Idris programming language. Other implementations (Coq; Lean4; Agda) will be mentioned, and we will make the relation to Interactive theorem proving.
- Tutorial
- Idris
Phase 3 (Weeks 4-10): Applications
The final phase of the course tackles Learning Objectives 3, 5, & 6. Various software vulnerabilities will be introduced, discussed, and their prevention using techniques and tooling from Phase 2 explored. Below we give a selection of suggestive topics, and note that other topics may be considered in the future. Each topic will be paired with a tutorial to provide further exploration of the topic using the software tooling introduced in Phase 2.
1 Week on Memory Safety
- Buffer Overflows
- Bounds checking; safe c; stack canaries; checked C
- Aliasing
- Capabilities (CHERI)
- Compartmentalisation
- Rust (Separation Logic), Linear Types (Quantitative Type-Theory)
- Tutorial
- Reasoning about lists
1 Week on Security of Information
- Access Control Models
- Information Flow
- Tutorial
- Information Flow
1 Week on Data Security
- Input validation
- Parsing
- Tutorial
- Scrubbing Data
1 Week on Securing Program Behaviour
- TOCTOU
- Race conditions
- Conformance (Session Types)
- Type state
- Tutorial
- file access api
1 Week on Program Language Security
- What makes a programming language safe?
- Type-safety
- Memory-safety
- Tutorial
- Simply-Typed Lambda Calculus
1 Week on Whole Program/Compiler Verification
- Using formal methods to reason about whole programs and language implementations;
- Project Everest; Bedrock; sel4
- Tutorial
- Well-Typed Interpreter
1 Week with a Guest Lecture
We will find a practitioner to come talk about their own experiences using formal methods to secure software.
‘Phase 4’ (Week 11)
We end the course in Week 11 with a student led revision session.