Talks

Satisfiability Modulo Finite Fields (with applications to compilers to zero-knowledge proofs)

Alex Ozdemir - Stanford in the Center for Automated Reasoning

5105 Brendan Iribe Center for Computer Science and Engineering (IRB)

Monday, October 23, 2023, 11:00 am-12:00 pm

You are subscribed to this talk through .
You are watching this talk through .
You are subscribed to this talk. (unsubscribe, watch)
You are watching this talk. (unwatch, subscribe)
You are not subscribed to this talk. (watch, subscribe)

Abstract

We study satisfiability modulo the theory of finite fields and give a decision
procedure for this theory. We implement our procedure for prime fields inside
the cvc5 SMT solver.

We apply our solver to two automated verification tasks related to compilers
to zero-knowledge proofs (ZKPs). First, we do translation validation for ZKP
compilers as applied to boolean input computations. Second, we do bounded
verification for a key ZKP compiler pass: the "finite-field blaster". Along
the way, we find 4 bugs in an existing ZKP compiler.

Ultimately, our experiments show that ZKP compilers can have bugs and that
those bugs can be eliminated using the theory of finite fields.

References:

"Satisfiability Modulo Finite Fields": https://doi.org/10.1007/978-3-031-37703-7_8
"Bounded Verification for Finite-Field Blasting": https://doi.org/10.1007/978-3-031-37709-9_8

Bio

Alex Ozdemir is a PhD student at Stanford in the Center for Automated
Reasoning and the Applied Cryptography group. His research uses ideas from
cryptography, compilers, and verification to improve tools for *secure
computation* (such as zero-knowledge proofs and multi-party computations).

This talk is organized by Benjamin Quiring