TY - GEN
T1 - Zero Knowledge Static Program Analysis
AU - Fang, Zhiyong
AU - Darais, David
AU - Near, Joseph P.
AU - Zhang, Yupeng
N1 - Funding Information:
We thank Michael Walfish for helpful discussions which inspired this work. This material is based upon work supported by DARPA under Contract No. HR001120C0087 and by NSF under awards CCF-2119939. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of DARPA.
Publisher Copyright:
© 2021 ACM.
PY - 2021/11/12
Y1 - 2021/11/12
N2 - Static program analysis tools can automatically prove many useful properties of programs. However, using static analysis to prove to a third party that a program satisfies a property requires revealing the program's source code. We introduce the concept of zero-knowledge static analysis, in which the prover constructs a zero-knowledge proof about the outcome of the static analysis without revealing the program. We present novel zero-knowledge proof schemes for intra- and inter-procedural abstract interpretation. Our schemes are significantly more efficient than the naive translation of the corresponding static analysis algorithms using existing schemes. We evaluate our approach empirically on real and synthetic programs; with a pairing-based zero knowledge proof scheme as the backend, we are able to prove the control flow analysis on a 2,000-line program in 1,738s. The proof is only 128 bytes and the verification time is 1.4ms. With a transparent zero knowledge proof scheme based on discrete-log, we generate the proof for the tainting analysis on a 12,800-line program in 406 seconds, the proof size is 282 kilobytes, and the verification time is 66 seconds.
AB - Static program analysis tools can automatically prove many useful properties of programs. However, using static analysis to prove to a third party that a program satisfies a property requires revealing the program's source code. We introduce the concept of zero-knowledge static analysis, in which the prover constructs a zero-knowledge proof about the outcome of the static analysis without revealing the program. We present novel zero-knowledge proof schemes for intra- and inter-procedural abstract interpretation. Our schemes are significantly more efficient than the naive translation of the corresponding static analysis algorithms using existing schemes. We evaluate our approach empirically on real and synthetic programs; with a pairing-based zero knowledge proof scheme as the backend, we are able to prove the control flow analysis on a 2,000-line program in 1,738s. The proof is only 128 bytes and the verification time is 1.4ms. With a transparent zero knowledge proof scheme based on discrete-log, we generate the proof for the tainting analysis on a 12,800-line program in 406 seconds, the proof size is 282 kilobytes, and the verification time is 66 seconds.
KW - static program analysis
KW - zero knowledge proofs
UR - http://www.scopus.com/inward/record.url?scp=85119340193&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85119340193&partnerID=8YFLogxK
U2 - 10.1145/3460120.3484795
DO - 10.1145/3460120.3484795
M3 - Conference contribution
AN - SCOPUS:85119340193
T3 - Proceedings of the ACM Conference on Computer and Communications Security
SP - 2951
EP - 2967
BT - CCS 2021 - Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security
PB - Association for Computing Machinery
T2 - 27th ACM Annual Conference on Computer and Communication Security, CCS 2021
Y2 - 15 November 2021 through 19 November 2021
ER -