13 citations · 19 across the 5 of their papers we have counts for
3 papers · 1 filter
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…
Cerberus: A Formal Approach to Secure and Efficient Enclave Memory Sharing
Dayeol Lee, Kevin Cheang, Alexander Thomas +7
Hardware enclaves rely on a disjoint memory model, which maps each physical address to an enclave to achieve strong memory isolation. However, this severely limits the performance…
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu +6
UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combi…