Browse

ZooBerry: A Software Framework for Global Sparse Analyzers and Their Verified Validators
ZooBerry: 프로그램 정적 분석기 및 검산기 자동 생성 시스템

Cited 0 time in Web of Science Cited 0 time in Scopus
Authors
조성근
Advisor
이광근
Major
공과대학 전기·컴퓨터공학부
Issue Date
2018-02
Publisher
서울대학교 대학원
Keywords
programming languagestatic analysisformal program verificationsparse analysis
Description
학위논문 (박사)-- 서울대학교 대학원 : 공과대학 전기·컴퓨터공학부, 2018. 2. 이광근.
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.
Language
English
URI
https://hdl.handle.net/10371/140708
Files in This Item:
Appears in Collections:
College of Engineering/Engineering Practice School (공과대학/대학원)Dept. of Computer Science and Engineering (컴퓨터공학부)Theses (Ph.D. / Sc.D._컴퓨터공학부)
  • mendeley

Items in S-Space are protected by copyright, with all rights reserved, unless otherwise indicated.

Browse