Modular and automatic formal verification of a RISC-V processor with security mechanisms

on YouTube ↗18m

" summary

A 32‑bit RISC‑V core in Kôika HDL is extended with privilege levels, PMP regions, traps, a hardware shadow stack and landing pads and compiled into an IR that is encoded to an SMT problem. Formal proofs show PMP violations trigger exceptions and that compiled IR properties refine back to the Kôika circuit; goals that took minutes in the proof assistant become seconds with an SMT solver. Current proofs target single‑cycle input/output relations; work focuses on per‑rule modularization and a working landing‑pad toolchain.

AI-written summary · about

" chapters (10)

1. 0:00Formal hardware verification intro
2. 1:06KOA hardware description overview
3. 2:54KOA rule conflicts handling
4. 4:23KOA to IR for proofs
5. 6:35RISC-V security extensions
6. 8:23SMT solvers for automation
7. 9:28Control flow integrity pads
8. 11:56Modular proof design challenges
9. 12:39Conclusion and future work
10. 13:26Q&A on verification