Verification Around the Hardware-Software Interface: Instruction Set, Processors, and Side Channels
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
|16:10 - 16:40|
Zhong ShaoYale University
|16:40 - 17:10|
Adam ChlipalaMassachusetts Institute of Technology, USA
|17:10 - 17:35|