BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Full Stack Verification of CHERI systems - Murali Vijayaraghavan\,
  MIT
DTSTART:20251117T110000Z
DTEND:20251117T120000Z
UID:TALK240673@talks.cam.ac.uk
CONTACT:Luisa Cicolini
DESCRIPTION:At Google\, we are exploring how CHERI can be used to build ne
 xt-generation systems that deliver strong privacy and security guarantees 
 with lower overhead\, coupled with formal methods that prove both function
 al correctness and security across the entire stack. This is active WIP.\n
 \nOur 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%7C49a50445bdfa4b79ade35
 47b4f3986e9%7C1%7C0%7C638978397636051326%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0e
 U1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjo
 yfQ%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%4
 0universityofcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b77
 98f0%7C49a50445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636078224%7CUnk
 nown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4
 zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=Vp5ebPk1NcJzzJ6MC
 V2bjsiLYYZ2qGNPFQGvBTLbASQ%3D&reserved=0—a 32-bit CHERI variant—agains
 t its ISA using "Guru":https://eur03.safelinks.protection.outlook.com/?url
 =https%3A%2F%2Fgithub.com%2FCherified%2FGuru&data=05%7C02%7Clc985%40univer
 sityofcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C
 49a50445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636097540%7CUnknown%7C
 TWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIk
 FOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=cUdHdPIRXQj%2FjnTSwkV5Lc
 qdpmik0KO2DGZd1AvmoT8%3D&reserved=0\, a Rocq DSL building on "Kami":https:
 //eur03.safelinks.protection.outlook.com/?url=http%3A%2F%2Fplv.csail.mit.e
 du%2Fkami%2F&data=05%7C02%7Clc985%40universityofcambridgecloud.onmicrosoft
 .com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b4f3986e9
 %7C1%7C0%7C638978397636116146%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1hcGkiOnRy
 dWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ%3D%3D%7
 C0%7C%7C%7C&sdata=a9foUOQAr%2F0JFOmdvx1yEaDK%2BbmlpKV%2F4Kp04Wzb3UQ%3D&res
 erved=0. Guru supports hardware design\, proof\, and hardware generation w
 ithin a unified framework\, enabling correct-by-construction development. 
 We have also defined an "multithreaded execution model":https://eur03.safe
 links.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FCherified%2Fc
 heriot-abstract-spec&data=05%7C02%7Clc985%40universityofcambridgecloud.onm
 icrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b
 4f3986e9%7C1%7C0%7C638978397636136684%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1h
 cGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ
 %3D%3D%7C0%7C%7C%7C&sdata=7TGZ0CVRw7%2BJv9rtp4Qm5emoui7QPl80Sz7va4QBF%2Bc%
 3D&reserved=0 for CHERIoT user code\, which revealed "issues":https://eur0
 3.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FCHERIoT
 -Platform%2Fcheriot-rtos%2Fissues%2F589&data=05%7C02%7Clc985%40universityo
 fcambridgecloud.onmicrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50
 445bdfa4b79ade3547b4f3986e9%7C1%7C0%7C638978397636163052%7CUnknown%7CTWFpb
 GZsb3d8eyJFbXB0eU1hcGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjo
 iTWFpbCIsIldUIjoyfQ%3D%3D%7C0%7C%7C%7C&sdata=Na5G8IjpNcWTtQcUHsXmJaTqriuqV
 JhyU8Nova7XwLI%3D&reserved=0 in the "CHERIoT microkernel":https://eur03.sa
 felinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FCHERIoT-Pla
 tform%2Fcheriot-rtos&data=05%7C02%7Clc985%40universityofcambridgecloud.onm
 icrosoft.com%7Cac79b2c97d994ce7060d08de1b7798f0%7C49a50445bdfa4b79ade3547b
 4f3986e9%7C1%7C0%7C638978397636192273%7CUnknown%7CTWFpbGZsb3d8eyJFbXB0eU1h
 cGkiOnRydWUsIlYiOiIwLjAuMDAwMCIsIlAiOiJXaW4zMiIsIkFOIjoiTWFpbCIsIldUIjoyfQ
 %3D%3D%7C0%7C%7C%7C&sdata=VK0KoQEAoUHLDjLmCcQCS1ld%2BXQ5S9SpVxCDmybMZ5g%3D
 &reserved=0’s multicore support through manual code inspection. We are a
 ddressing these issues and extending our framework to verify that the micr
 okernel conforms to this execution model. The microkernel’s minimality
 —about 400 instructions to handle exceptions\, interrupts/thread switchi
 ng\, and process switching—makes it a tractable target for full formal v
 erification. By composing the proofs of processor and microkernel correctn
 ess\, we aim to demonstrate a fully verified hardware/OS stack that enforc
 es isolation for user applications.\n\nLooking ahead\, we plan to reimagin
 e the notion of Trusted Execution Environments (TEEs) using CHERI and form
 al verification—eliminating reliance on memory encryption and instead fo
 rmally proving the required properties: isolation of user applications fro
 m each other and from the platform\, and authenticated updates of the OS a
 nd user applications.\n\n**Speaker Bio:**\nMurali Vijayaraghavan received 
 his Ph.D. from MIT\, where his research focused on Rocq-based DSLs for des
 igning and formally verifying processors and cache hierarchies\, as well a
 s generating synthesizable hardware circuits. His work centers on advancin
 g the adoption of formal methods in industry and reducing the trusted comp
 uting base (TCB) in complex systems. This line of research has naturally l
 ed him to explore the use of CHERI to provide memory safety for applicatio
 ns and strong compartmentalization between them with a minimal TCB.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR