Hardware verification talk at Imperial College London

Stream: general

[Simon Hudon]

Hi everyone!

Sorry to be at the very last minute but my colleague Satnam Singh at Google is presenting our work on formal verification of cryptographic hardware at Imperial College London. We use Coq for the verification but I thought people here might still be interested. Message me and I can give you the Microsoft Teams link to join. The talk is starting right now.

[Simon Hudon]

This talk describes the specification, implementation and formal verification inside the Coq theorem prover of the AES crypto accelerator component of the OpenTitan silicon roof of trust. The approach we take is inspired by Adam Chlipala in his book Certified Programming with Dependent Types. We have developed a Lava-like domain specific hardware description language called Cava in Coq’s Gallina language which is designed to help describe low level data-path style circuits with a view to having tight control over resource utilization and performance. This allows us to specify, implement and formally verify high assurance systems in one model where specifications are plain Gallina functions that specify the desired behaviour of hardware components. Our system can extract circuit descriptions from our Coq DSL to SystemVerilog for implementation on FPGA circuits.

We are also planning on building on this work to also tackle the co-design of software and hardware where we extract both C code (or RISC -V machine code) and SystemVerilog and a register or bus-interface so we can reason about the end-to-end behaviour of a system comprising hardware and software.

SPEAKER BIO: Satnam Singh works at Google Research on the Oak project that is developing technology to promote secure and private computing. Satnam Singh has worked on projects dealing with custom hardware acceleration and compiler technology at Facebook, Microsoft and Xilinx and has held academic positions at the University of Glasgow and the University of Birmingham.