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 (computational logic, abstract interpretation and type systems) that go beyond simple testing and provide strong guarantees about the security of software systems. We will consider conventional topics briefly, but the main goal is to learn how to produce and evaluate evidence for security-relevant claims: proofs, validated witnesses/certificates, and type-checked guarantees, together with clearly stated assumptions and limitations.
We organize the course around three professions that will be increasingly important in the age of AI when the focus will shift from manually writing code to specifying requirements and producing evidence that the specification is satisfied:
- Proof Engineer. Writing precise specifications and invariants, and using mechanized deductive verification (e.g., Dafny) to produce checkable proofs. We will also discuss how verified models/oracles can be used to validate production code using coverage-guided differential testing.
- Static Analysis Engineer. Designing sound program analyses (abstract interpretation) that scale beyond manual proofs. Instead of relying on "no warnings", we emphasize analyzers that output structured evidence (such as invariants or witnesses) together with independent validation of that evidence.
- Type Systems Engineer. Understanding how type systems enforce properties by construction, and how to use types to prevent whole classes of security-relevant misuse. We will use ownership types as a central case study for what a compiler can guarantee, and how explicit contracts become proof obligations when crossing unsafe boundaries.
The course has one lecture and one lab per week. Labs are designed to support the theory: you will implement small systems and verification/analysis components, and write specifications/proofs in a verification-oriented language when appropriate.
You are encouraged to propose your own application domain or case study (individually or in a group) to connect the verification methods to your interests.