Verifying RISC-V Physical Memory Protection

Kevin Cheang, Cameron Rasmussen, Dayeol Lee +3

We formally verify an open-source hardware implementation of physical memory protection (PMP) in RISC-V, which is a standard feature used for memory isolation in security critical…