Manuel Barbosa, University of Porto (FCUP) and INESC TEC

Abstract

In this talk I will give an overview of a series of works where we have looked at the problem of formally verifying cryptographic software, including implementations of highly efficient low-level primitives, synthesis of provably secure zero-knowledge protocol implementations and various components in secure multiparty computation software stacks. The talk will cover the different formal verification techniques and tools, lessons learned, and ongoing work.