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
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

16:10 - 17:35: DeepSpec 2018 - Hardware and Low-Level OS Verification at Columbus Ballroom B
deepspec-2018-papers16:10 - 16:40
Zhong ShaoYale University
deepspec-2018-papers16:40 - 17:10
Adam ChlipalaMassachusetts Institute of Technology, USA
deepspec-2018-papers17:10 - 17:35