Zero-Knowledge Model Checking

TL;DR

This paper presents a zero-knowledge model checking approach that verifies software correctness without revealing the system, combining deductive certificates with zero-knowledge proofs for confidentiality-preserving verification.

Contribution

It introduces explicit-state and symbolic zero-knowledge model checking schemes using polynomial commitments and Farkas' lemma, enabling confidential formal verification.

Findings

Prototype demonstrates practical efficacy on temporal logic examples.

Methods verify correctness while preserving system confidentiality.

Approach applicable to safety-critical domains requiring secrecy.

Abstract

We introduce a technology to formally verify that a software system satisfies a temporal specification of functional correctness, without revealing the system itself. Our method combines a deductive approach to model checking to obtain a formal certificate of correctness for the system, with zero-knowledge proofs to convince an external verifier that the system -- kept secret -- complies with its specification of correctness -- made public. We consider proof certificates represented as ranking functions, and introduce both an explicit-state and a symbolic scheme for model checking in zero knowledge. Our explicit-state scheme assumes systems represented as transition graphs. We use polynomial commitments to convince the verifier that the public proof certificates correspond to the secret transition relation. Our symbolic scheme assumes systems specified as linear guarded commands and uses piecewise-linear ranking functions. We apply Farkas' lemma to obtain a witness for the validity of the ranking function with public and secret components, and employ sigma protocols for matrix multiplication and range proofs to convince the verifier of the witness's existence. We built a prototype to demonstrate the practical efficacy of our two schemes on linear temporal logic verification examples. Our technology enables formal verification in domains where both the safety and the confidentiality of the system under analysis are critical.