Completed
Formal security properties
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Formal Modelling and Proof in the CHERI Design and Implementation Process
Automatically move to the next video in the Classroom when playback concludes
- 1 Microsoft: 70% of patched vulnerabilities are memory safety issues
- 2 Two fundamental problems
- 3 Rigorous engineering for hardware security
- 4 CHERI: hardware support for capabilities
- 5 Versions of CHERI
- 6 Fine-grained memory protection
- 7 Capability manipulations
- 8 Scalable software compartmentalisation
- 9 Protection domain transitions
- 10 A prose architecture description
- 11 A formal architecture model
- 12 The formal specification of Cload
- 13 Prose security properties
- 14 Formal security properties
- 15 Mapping instructions to abstract actions
- 16 Property about storing data
- 17 Monotonicity of reachable capabilities
- 18 Memory isolation between compartments
- 19 Conclusion
