ZooBerry

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.

Introduction

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.

Performance

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.

Source Code

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

Abstract semantics
- (U) Abstract domain: DomAbs.v DomArrayBlk.v DomBasic.v DomMem.v
- (E) Abstract domain: DomAbs.ml DomArrayBlk.ml DomBasic.ml DomMem.ml
- (U) Abstract semantics: SemAbs.v SemEval.v SemMem.v SemPrune.v
- (E) Abstract semantics: SemAbs.ml SemEval.ml SemMem.ml SemPrune.ml
Soundness proof of abstract semantics
- (U) Soundness proof: SemProof.v
- (U) Access-soundness proof: AccProof.v
Sparse analyzer
- (P_U) Main-analysis: Worklist.ml Sparse.ml
- (P_U) Pre-analysis: Pre.ml
- (P_U) Data dependency generator: Dug.ml
Verified validator
- (P_U) Fixpoint checker: GenFunc.v
- (E) Fixpoint checker: GenFunc.ml
- (P) Concrete semantics: DomCon.v SemCon.v
- (P_U) Soundness + access-soundness: UserProofType.v
- (P_U) Correctness proof of validator: SemInsenLocal.v SemSenLocal.v SemSen.v CorInsenLocal.v CorSenLocal.v CorSen.v CorFin.v GenProof.v

Download

Git repository: ZooBerry @ GitHub
Source tarball: zooberry.tar.gz (0.4MB)
Linux binaries (x86_64): buffer overrun analyzer (5.6MB), format string vulnerability analyzer (5.7MB)

You can run the ZooBerry-generated analyzers on pre-processed C files. The validator runs with the -validate option.
```
$ ./zb_itv -validate test.i
```

Papers

ZooBerry: A Software Framework for Global Sparse Analyzers and Their Verified Validators. [pdf]
Sungkeun Cho, Jeehoon Kang, Chung-Kil Hur, and Kwangkeun Yi.
Submitted.

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.

People


Sungkeun Cho	Jeehoon Kang	Chung-Kil Hur	Kwangkeun Yi

Contact

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

Acknowledgement

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).