FORMALLY VERIFYING SECURITY PROPERTIES OF CHERI PROCESSORS

Summary from the TLDR InfoSec newsletter

Researchers used a new verification framework, VeriCHERI, to find and fix a vulnerability in a processor vulnerable to Meltdown-style attacks. VeriCHERI focuses on security properties rather than conforming to a specification, making it effective in detecting vulnerabilities like timing side channels. This approach enhances security verification for processors like CHERIoT Ibex, improving protection against attacks exploiting microarchitectural weaknesses.