Roberto Guanciale

Assistant professor of computer science at KTH

Abstract

Verification of microkernels and and crypto routines requires analyses at the binary level. In order to automate these analyses, in the last years several binary analysis platforms have been introduced. These platforms share a common design: code is translated to an hardware-independent intermediate representation that is analyzed using architecture independent tools. The usage of these platforms introduces the need for trusting both the correctness of the translation and the correctness of the analyses. We overcome these problems by developing a binary analysis platform on top of the interactive theorem prover HOL4. The new platforms provides proof-producing transpilers, which support ARMv8 and CortexM0 programs, proof-producing weakest precondition generator, which can be used to verify if loop-free program fragment satisfies a contract, and is equipped with a new logic to verify unstructured binary programs.

Bio

Roberto Guanciale is an assistant professor within the Department of Theoretical Computer Science, EECS, KTH since 2015, where he works on system security and formal verification. He received his bachelor’s degree in Computer Science from University of Pisa in 2003, his Master from from University of Pisa in 2005, and his Ph.D. from IMT Lucca in 2009. He has been postdoctoral researcher at KTH (2012 - 2015). His research focuses on Computer Security, in particular on formal verification low level code and design of separation kernels. He also designed methods to analyze coordination of distributed services.

Slides