ZooBerry: A Software Framework for Global Sparse Analyzers and Their Verified Validators

Abstract

In this dissertation, we report a software framework, called ZooBerry, that fills the gap between static analysis designs (abstract semantics and their soundness proofs) and their faithful yet scalable implementations (industrial-strength global analyzers whose results can be automatically checked correct). The input to ZooBerry is an abstract semantics (an analysis specification) and its soundness proof, both in Coq. For scalable implementation, ZooBerry automatically integrates into the abstract semantics the general sparse analysis technology that streamlines both the spatial and temporal footprints of the generated analyzers. For faithful implementation, ZooBerry also generates a verified validator (and its safety proof in Coq) that will check the correctness of each analysis result of the generated sparse analyzer.

ZooBerry's performance is tested in realistic settings. We have implemented two analyzers for C programs, together with their validators, that detect buffer overrun and format string bugs. Both analyzers' cost performance is like they take 10-20 minutes to globally analyze 100KLoC of C benchmarks. From the format string bug analyzer we were able to find two security vulnerabilities that are confirmed (CVE-2015-8106 and CVE-2015-8107) by the security community. The generated validators took additional 5-9% of the analysis time to check the correctness of analysis results.