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.

翻译：我们提出一种技术，可在不泄露软件系统本身的前提下，形式化验证该系统是否满足功能正确性的时序规范。该方法将模型检验的演绎方法与零知识证明相结合：前者为系统生成形式化正确性证书，后者则用于向外部验证者证明——被保密的系统符合公开的正确性规范。我们以排名函数作为证明证书的表示形式，并分别提出显式状态与符号化两种零知识模型检验方案。显式状态方案假设系统以迁移图形式表示，通过多项式承诺向验证者证明公开的证明证书与秘密的迁移关系相对应。符号化方案假设系统以线性守卫命令形式指定，并采用分段线性排名函数；我们应用法卡斯引理获取包含公开与秘密组件的排名函数有效性证据，通过矩阵乘法的西格玛协议与范围证明向验证者证实该证据的存在性。我们构建了原型系统，在线性时序逻辑验证实例上验证了两种方案的实际效能。该技术可应用于分析与系统的安全性与机密性均至关重要的领域，实现形式化验证。