S-Space College of Engineering/Engineering Practice School (공과대학/대학원) Dept. of Computer Science and Engineering (컴퓨터공학부) Theses (Ph.D. / Sc.D._컴퓨터공학부)
ZooBerry: A Software Framework for Global Sparse Analyzers and Their Verified Validators
ZooBerry: 프로그램 정적 분석기 및 검산기 자동 생성 시스템
- 공과대학 전기·컴퓨터공학부
- Issue Date
- 서울대학교 대학원
- 학위논문 (박사)-- 서울대학교 대학원 : 공과대학 전기·컴퓨터공학부, 2018. 2. 이광근.
- 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.