Fromager: Verify and Evaluate Software with Zero-Knowledge of its Source Code
Fromager is a research project in producing zero-knowledge (ZK) proofs about diverse properties of real-scale software.
Fromager encompasses two projects that address distinct Technical Areas (TAs) of the DARPA SIEVE program: Cheesecloth (TA1) and Quark (TA2). These two projects will work together to create a robust software platform with the goal of delivering the following zero-knowledge capabilities:
- prove whether or not vulnerabilities exist in software without revealing how they are caused;
- assess properties of cyberspace operations capabilities without accessing source code; and
- assure anti-tamper cyber-security techniques without revealing code details.
How do Cheesecloth and Quark work together?
Cheesecloth encodes proof statements for five classes of software properties:
- memory safety,
- integer overflow safety,
- performance security,
- information flow security, and
- functional equivalence.
Cheesecloth uses a rich instruction set to efficiently encode these proof statements. The instruction set is derived from SCALE bytecode, a bytecode used for the SCALE secure multi-party computation (MPC) engine.
Quark takes the proof statements emitted by Cheesecloth and executes them on one of two distinct ZK platforms, the first based on a “commit-and-prove” approach, and the other based on an “MPC-in-the-head” approach. A central theme of Quark is that both of these platforms leverage techniques from MPC and aim to adapt many of the innovations that have occurred in the MPC space in recent years to the ZK paradigm.
The architecture for these TAs help show how they work together:
Fromager’s salient contributions are:
- drastically improved capabilities to optimize the encodings of proofs of vulnerability at a practical scale;
- the novel capability to produce ZK proofs of security invariants of complex software;
- new approaches inspired by MPC to efficiently mix Boolean and arithmetic operations, and the use of specialized operators in proofs to decrease concrete complexity; and
- a novel commit-and-prove engine that sacrifices public verifiability to achieve linear asymptotic computation costs and sub-linear communication costs.
Fromager engages a diverse international team. Galois will lead the effort with research contributions from faculty at Katholieke Universiteit. Leuven (Belgium), Aarhus University (Denmark), Columbia University (USA), and researchers at QEDIT Corporation (Israel).
Distribution Statement “A” (Approved for Public Release, Distribution Unlimited)