Doctoral Thesis Proposal - Quang Dao
November 20, 2026 10:00AM—11:30AM
Location:
4405
-
Gates and Hillman Centers
Speaker:
QUANG DAO,
Ph.D. Student, Computer Science Department, Carnegie Mellon University
https://quangvdao.github.io/
A succinct cryptographic proof lets anyone check a computation much faster than running it; it is zero-knowledge if it reveals nothing about the computation's private data. Such proofs have moved from theory into the real world: they let a person prove they are over 18 without revealing anything else, and let a blockchain verify thousands of transactions without re-executing them. Nevertheless, deployment remains difficult. Proving is still too slow for many applications, many deployed systems are broken against a large quantum computer, and complex protocols and implementations invite bugs, some of which would have let attackers create unlimited counterfeit money without detection.
This thesis tackles these problems along two directions. The first is to design proof systems that are faster and secure against quantum computers. At its center is Akita, a lattice-based polynomial commitment scheme, the first to combine proofs under 80 KB, verification under 20 ms, and post-quantum security from a standard lattice assumption (Module-SIS). We will add zero knowledge to Akita, and commitments to binary-field data, which make hash functions such as SHA-3 much cheaper to prove.
We use Akita in two applications. First, Lattice Jolt proves correct execution of RISC-V programs 2 to 4 times faster than the elliptic-curve version of Jolt, which is not post-quantum, with proofs of similar size. Second, Aerie compresses many Falcon signatures (soon standardized by NIST as FN-DSA) into one short proof that they are all valid, and we will extend it to ML-DSA, NIST's main post-quantum signature standard.
The second direction is to rule out bugs in the protocols themselves, with machine-checked proofs in the Lean proof assistant. Since such proofs are only as good as their statements, we introduce VCVio, a framework of shared, auditable security definitions for human- and AI-written proofs. On top of VCVio, we are building ArkLib, a modular framework in which we have verified several well-known interactive protocols. We will prove the security of the Fiat–Shamir and BCS transformations, which make these protocols non-interactive, and prove that Jolt's core protocol accepts exactly the correct runs of RISC-V programs, as defined by RISC-V's official formal specification.
Thesis Committee:
Aayush Jain (Co-Chair)
Riad Wahby (Co-Chair)
Bryan Parno
Justin Thaler (a16z Frontier & Georgetown University)
Contact
Matt Stewart