Islaris: Verification of Machine Code Against Authoritative ISA Semantics
summary
Islaris verifies machine code against authoritative ISA mechanizations by pruning huge Sail models with SMT-backed Isla symbolic execution into compact Isla traces, then proving code correct in Coq using an Iris-based program logic with automated tactics (lia_run, bb_solve). Sail’s ARM model is ~125,000 lines so ARM translation validation is infeasible, but a semi-automatic translation validation succeeds for RISC-V. The toolset verifies real artifacts: a PKVM exception handler, an exception-level switch that writes 42 into x0, and a compiled binary-search with function-pointer comparisons, and it scales though some SMT checks remain the bottleneck.
AI-written summary · about
chapters (6)
- 0:00Start
- 0:11Why machine code verification?
- 1:39Existing Mechanised ISA Semantics in Sail
- 8:43Verifying relevant aspects: Iris-based program logic
- 10:53Verification of a hypercall setup and invocation
- 12:25What else is in the paper?
related talks
36mTowards a Formally-verified Software Toolchain for open ISAs
02h 49mA Tour of the RISC V ISA Formal Specification
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
09mSemi-Automated Translation of a Formal ISA Specification to Hardware
14mScaling Instruction-Selection Verification against Authoritative ISA Semantics
16mThe Morello ISA semantics, proof, and test generation
20mSail RISC-V: Status and Future Challenges
59mTutorial: High Level Sail Overview