The Kami project within DeepSpec deals with proving the correctness of digital-hardware components like multicore processor systems. I’ll review the big ideas of Kami and then focus on two relatively recent developments: a novel kind of formal semantics for the instruction set we are using, and proofs that hardware-software systems don’t leak information through timing side channels.

Mon 18 Jun

Displayed time zone: Eastern Time (US & Canada) change