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":https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcheriot.org%2Fbook%2F&data=05%7C02%7Clc985%40universityofcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636051326%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=jLHVbMafxYPh9T4weETpGRYNub4UVQ6%2BBR6XAgSW6HU%3D&reserved=0 "processor":https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FCherified%2FCheriot&data=05%7C02%7Clc985%40universityofcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636078224%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=Vp5ebPk1NcJzzJ6MCV2bjsiLYYZ2qGNPFQGvBTLbASQ%3D&reserved=0—a 32-bit CHERI variant—against its ISA using "Guru":https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FCherified%2FGuru&data=05%7C02%7Clc985%40universityofcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636097540%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=cUdHdPIRXQj%2FjnTSwkV5Lcqdpmik0KO2DGZd1AvmoT8%3D&reserved=0, a Rocq DSL building on "Kami":https://eur03.safelinks.protection.outlook.com/?url=http%3A%2F%2Fplv.csail.mit.edu%2Fkami%2F&data=05%7C02%7Clc985%40universityofcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636116146%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=a9foUOQAr%2F0JFOmdvx1yEaDK%2BbmlpKV%2F4Kp04Wzb3UQ%3D&reserved=0. 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":https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FCherified%2Fcheriot-abstract-spec&data=05%7C02%7Clc985%40universityofcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636136684%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=7TGZ0CVRw7%2BJv9rtp4Qm5emoui7QPl80Sz7va4QBF%2Bc%3D&reserved=0 for CHERIoT user code, which revealed "issues":https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FCHERIoT-Platform%2Fcheriot-rtos%2Fissues%2F589&data=05%7C02%7Clc985%40universityofcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636163052%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=Na5G8IjpNcWTtQcUHsXmJaTqriuqVJhyU8Nova7XwLI%3D&reserved=0 in the "CHERIoT microkernel":https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FCHERIoT-Platform%2Fcheriot-rtos&data=05%7C02%7Clc985%40universityofcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636192273%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=VK0KoQEAoUHLDjLmCcQCS1ld%2BXQ5S9SpVxCDmybMZ5g%3D&reserved=0’s 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.
