Fromager: Verify and Evaluate Software with Zero-Knowledge of its Source Code

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: 

1. prove whether or not vulnerabilities exist in software without revealing how they are caused;
2. assess properties of cyberspace operations capabilities without accessing source code; and
3. 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: 

1. memory safety, 
2. integer overflow safety, 
3. performance security, 
4. information flow security, and 
5. 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: 

Figure 1: Architecture of Cheesecloth. Outputs public to the prover and verifier are in blue and outputs private to the prover are in gold. The verification process may be any process (automatic or interactive) that a user performs to synthesize a witness of a claim (such as a vulnerability trace or a proof of safety).

Figure 2: Architecture of Quark. Public inputs known to both the prover and verifier are in blue, and private inputs known only to the prover are in gold. Both inputs are provided by TA1 performers; in addition, TA1 performers may optionally provide their proof statement in a domain-specific language (DSL) which is then compiled down to SCALE bytecode. zkInterface acts as the API between TA1 and TA2 performers.

Key Contributions

Fromager’s salient contributions are:

1. drastically improved capabilities to optimize the encodings of proofs of vulnerability at a practical scale;
2. the novel capability to produce ZK proofs of security invariants of complex software;
3. 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
4. a novel commit-and-prove engine that sacrifices public verifiability to achieve linear asymptotic computation costs and sub-linear communication costs. 

Team

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)