A Software Framework for Global Sparse Analyzers and Their Verified Validators
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.
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
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.
(U): User inputs
(P): Pre-built in ZooBerry
(PU): Pre-built & parameterized by user inputs
(E): Extracted from Coq to OCaml
Git repository: ZooBerry @ GitHub
You can run the ZooBerry-generated analyzers on pre-processed C files. The validator runs with the
$ ./zb_itv -validate test.i
- 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.
|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).