A Software Framework for Global Sparse Analyzers and Their Verified Validators

Sungkeun Cho, Jeehoon Kang, Chung-Kil Hur, and Kwangkeun Yi
Programming Research Lab. & Software Foundations Lab., Seoul National University.


ZooBerry is a software framework that fills the gap between static analysis designs (abstract semantics and their soundness proofs) and their faithful yet scalable implementations (global analyzers whose results can be automatically checked correct). The inputs to ZooBerry are an abstract semantics and its soundness proof, both in Coq. The outputs of ZooBerry are a global sparse analyzer and a verified validator.

Inputs and outputs of ZooBerry

  • For scalable implementation, ZooBerry automatically integrates into the abstract semantics the sparse analysis technology that streamlines both the spatial and temporal footprints of the generated analyzers.

  • For faithful implementation, the ZooBerry-generated validator checks the correctness of each analysis result of the generated sparse analyzer. The correctness of the validator is formally proven in Coq.


Using ZooBerry, we implementated two analyzers for C programs: an interveral analyzer for buffer overrun bugs and a taint analyzer for format string bugs.

  • Scalability: Both analyzers’ cost performance is like they take 10-20 minutes to globally analyze 100KLoC of C benchmarks.

  • Usefulness: By using the ZooBerry-generated taint analyzer, together with our interactive false-alarm classification technology, we could identify security vulnerabilities in latex2rtf and a2ps (CVE-2015-8106 and CVE-2015-8107).

  • Validation overhead: The generated validators took additional 5-9% of the analysis time to check the correctness of analysis results.

Components of ZooBerry

ZooBerry contains a sparse analyzer and a verified validator that are parameterized by user inputs, which are abstract semantics and its soundness proof, as depicted below. Except for the user inputs (dashed boxes), the others (solid boxes) are pre-built in ZooBerry. Most of the pre-built parts except for the concrete semantics depend on the user inputs. For example, the pre-/main-analyzers can run only when the abstract semantics is provided and the correctness proof of validator is completed when the soundness proof of the abstract semantics is provided. The user-provided abstract semantics is shared by the sparse analyzer and the verified validator and the soundness proof is only used by the latter.

Components of ZooBerry

Source Code

(U): User inputs
(P): Pre-built in ZooBerry
(PU): Pre-built & parameterized by user inputs
(E): Extracted from Coq to OCaml

  1. Abstract semantics
  2. Soundness proof of abstract semantics
  3. Sparse analyzer
  4. Verified validator



  • ZooBerry: A Software Framework for Global Sparse Analyzers and Their Verified Validators. [pdf]
    Sungkeun Cho, Jeehoon Kang, Chung-Kil Hur, and Kwangkeun Yi.
  • Towards Scalable Translation Validation of Static Analyzers. [pdf] [web]
    Jeehoon Kang, Sungkeun Cho, Joonwon Choi, Chung-Kil Hur, and Kwangkeun Yi.
    Technial report. Research On Software Analysis for Error-free Computing Center, Seoul National University. 2014.


skcho jhkang gil kwang
Sungkeun Cho Jeehoon Kang Chung-Kil Hur Kwangkeun Yi


For general questions regarding ZooBerry, please send email to zooberry _at_ ropas.snu.ac.kr.


This work was partly supported by Samsung Electronics(grant No. SRFC-IT1502-07, No. 0421-20150073), by Institute for Information & Communications Technology Promotion(grant No. B0717-16-0098) of Korea Ministry of Science, ICT and Future Planning, and by National Research Foundation of Korea(BK21 Plus grant No. 21A20151113068).

Copyright (c) 2017, Programming Research Laboratory & Software Foundations Laboratory, Seounal National University.