Full Stack Verification of CHERI systems

Add to your list(s) Download to your calendar using vCal

• Murali Vijayaraghavan, MIT
• Monday 17 November 2025, 11:00-12:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Luisa Cicolini.

At Google, we are exploring how CHERI can be used to build next-generation systems that deliver strong privacy and security guarantees with lower overhead, coupled with formal methods that prove both functional correctness and security across the entire stack. This is active WIP .

Our work begins with formally verifying the functional correctness of a CHERIoT processor 32-bit CHERI variant—against its ISA using Guru, a Rocq DSL building on Kami. Guru supports hardware design, proof, and hardware generation within a unified framework, enabling correct-by-construction development. We have also defined an multithreaded execution model for CHER IoT user code, which revealed issues in the CHERIoT microkernel multicore support through manual code inspection. We are addressing these issues and extending our framework to verify that the microkernel conforms to this execution model. The microkernel’s minimality—about 400 instructions to handle exceptions, interrupts/thread switching, and process switching—makes it a tractable target for full formal verification. By composing the proofs of processor and microkernel correctness, we aim to demonstrate a fully verified hardware/OS stack that enforces isolation for user applications.

Looking ahead, we plan to reimagine the notion of Trusted Execution Environments (TEEs) using CHERI and formal verification—eliminating reliance on memory encryption and instead formally proving the required properties: isolation of user applications from each other and from the platform, and authenticated updates of the OS and user applications.

Speaker Bio: Murali Vijayaraghavan received his Ph.D. from MIT , where his research focused on Rocq-based DSLs for designing and formally verifying processors and cache hierarchies, as well as generating synthesizable hardware circuits. His work centers on advancing the adoption of formal methods in industry and reducing the trusted computing base (TCB) in complex systems. This line of research has naturally led him to explore the use of CHERI to provide memory safety for applications and strong compartmentalization between them with a minimal TCB .

This talk is part of the compiler socials series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Computer Architecture Group Meeting
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• compiler socials
• yk449

Note that ex-directory lists are not shown.