Software Security
This course is an introduction to quality-based security. We aim to learn methods for software understanding: the rigorous practice of constructing and assessing software-controlled systems to verify their functionality, safety, and security.
We will mainly explore machine reasoning techniques, from computational logic to abstract interpretation, that go beyond simple testing and provide strong guarantees about the security of software systems. We will consider threat-modelling and conventional topics briefly, but the idea is to focus on a couple of interesting industrial case studies that apply formal approaches.
- AWS: Cedar. We will consider the problem of access control, including the theory, and why these authorization solutions, like Google's Zanzibar or Amazon's Verified Permissions, are needed. We will then look at how Amazon's policy engine Cedar works and how it was implemented, using Dafny (then Lean) and coverage-guided fuzzing.
- Meta: Infer. Code-level vulnerabilities are still a thing. We will look at how one can verify the absence of vulnerabilities using automated software verification. We will study some of the underlying theory, including abstract interpretation and separation logic, so that we can understand how to use these tools properly.
- Low-Level Type Systems. By the end of the course, Chad Nester will show type-theoretic approaches to ensuring memory safety. He will focus on explaining the core ideas rather than immediately jumping to something complicated like Rust's borrow checker, but at least you will understand things! ;)
- Also, please propose your own case study!! Either as an individual or group project that replaces the exam, or suggest something we should do.
Grading and Requirements
There will be weekly moodle tests; and hands-on exercises that we discuss in the labs. The questions in the quiz and the exam will be based on the theory and conclusions; doing the practical work is optional. The exam can be replaced or supplemented by a project.