March 14, 2019, 9:05 AM - 9:35 AM
Barrister's Hall - first floor
Boston University Law School
765 Commonwealth Avenue
Boston, MA 02215
Manuel Barbosa, University of Porto (FCUP) and INESC TEC
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.