• 2018 Spectre and Meltdown: Raised awareness of timing side channels in modern processor microarchitecture. In following years, research by academia and industry to investigate and mitigate. Focus was on larger cores with performance optimizations like out-of-order execution and speculation, but even small low-power processors with in-order pipelines can be vulnerable.
• Meltdown-style attack: Exploits out-of-order execution to read from protected memory. Allows attacker to run code but not access certain memory locations. Out-of-order execution creates transient time window for early load access, creating race condition. In functionally correct implementation, illegally accessed data doesn't affect architectural state but may leave footprint in microarchitecture. Meltdown-style attacks can be created with simple in-order load instructions, and out-of-order execution amplifies the effect.
• Vulnerability in CHERIoT Ibex: Fits Meltdown-style category. PCC restricts fetching instructions from outside current compartment. Jump instruction with unaligned instructions leads to exception and flushed pipeline. VeriCHERI found potential attack can probe memory for specific bits, and probing result is in execution time and performance counter. CHERIoT team fixed by adjusting fetch FIFO.
• How detected: VeriCHERI is a new formal verification framework for CHERI-enhanced processors. Starts from abstract security requirements and formulates microarchitectural security properties. Different from previous methods focusing on design compliance. Consists of 4 security properties checked using commercial property checking tools. Verification times for CHERIoT Ibex range from seconds to 31 minutes. Refer to paper.
• Full citation: "VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL" by Anna Lena Duque Antón et al. Accepted for publication at ICCAD '24. Presents a novel approach to security verification without requiring ISA specification, checking against confidentiality and integrity objectives and using few unbounded properties to prove or disprove vulnerabilities. Demonstrated on a RISC-V based processor with a CHERI variant.