The Morello ISA semantics, proof, and test generation
summary
Formal work translates the ~62,000-line ASL Morello spec into a theorem‑prover model, generates Isabelle proofs that check a monotonicity theorem (software cannot forge capabilities), and runs full proof builds that take about seven hours. The process covers roughly 400 instructions, finds concrete bugs (two missing capability checks and capability‑compression faults), and produces an emulator plus SMT‑based testing as a test oracle and high‑coverage test suite for hardware/software bring‑up.
AI-written summary · about
chapters (11)
- 0:00Morello ISA semantics intro
- 1:04Motivation for formal security verification
- 2:09Formal model from ASL specs
- 3:54Capability checks and exceptions
- 4:34Reachable capabilities and monotonicity
- 6:41Proving monotonicity theorem
- 7:46Proof effort and automation
- 8:49Bugs found in verification
- 9:30Test generation from formal model
- 10:11Verification limitations
- 11:16Q&A
related talks
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
12mISA Formal Task Group Update
36mTowards a Formally-verified Software Toolchain for open ISAs
23mVellvm: Formalizing the Informal
53mSemantics-based program manipulation in the age of LLMs
14mScaling Instruction-Selection Verification against Authoritative ISA Semantics
01h 05mMuch Still to Do in Compiler Verification (A Perspective from the CakeML Project)
01h 06mVerifying a compiler through equational means