AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
We evaluated our tool on large-scale systems code from BIND, OpenSSL, and the Linux kernel, and we found a total of 79 bugs, including two OpenSSL denial-of-service vulnerabilities

Under-Constrained Symbolic Execution: Correctness Checking for Real Code

USENIX Annual Technical Conference, pp.49-64, (2016)

Cited by: 181|Views241
EI
Full Text
Bibtex
Weibo

Abstract

Software bugs are a well-known source of security vulnerabilities. One technique for finding bugs, symbolic execution, considers all possible inputs to a program but suffers from scalability limitations. This paper uses a variant, under-constrained symbolic execution, that improves scalability by directly checking individual functions, ra...More

Code:

Data:

0
Introduction
  • Software bugs pervade every level of the modern software stack, degrading both stability and security.
  • Current practice attempts to address this challenge through a variety of techniques, including code reviews, higherlevel programming languages, testing, and static analysis.
  • While these practices prevent many bugs from being released to the public, significant gaps remain.
  • It misses bugs that are only triggered by other inputs
  • Another broad technique, static analysis, is effective at discovering many classes of bugs.
  • Static tools often miss deep bugs that depend on specific input values
Highlights
  • Software bugs pervade every level of the modern software stack, degrading both stability and security
  • This paper presents UC-KLEE, a scalable framework implementing under-constrained symbolic execution for C/C++ systems code without requiring a manual specification or even a single testcase
  • We evaluated UC-KLEE’s checkers on over 20,000 functions from BIND, OpenSSL, and the Linux kernel
  • We have presented UC-KLEE, a novel framework for validating patches and applying checkers to individual C/C++ functions using under-constrained symbolic execution
  • We evaluated our tool on large-scale systems code from BIND, OpenSSL, and the Linux kernel, and we found a total of 79 bugs, including two OpenSSL denial-of-service vulnerabilities
  • Our preliminary experiments have shown that this use case results in a much higher rate of false positives, but we did find a number of interesting bugs, including the OpenSSL denial-of-service attack for which advisory CVE-2015-0291 [15, 22, 42] was issued
Results
  • The authors evaluated UC-KLEE on hundreds of patches from BIND and OpenSSL, two widely-used, security critical systems.
  • Each codebase contains about 400,000 lines of C code, making them reasonable measures of UC-KLEE’s scalability and robustness.
  • For this experiment, the authors used a maximum symbolic object size of 25,000 bytes and a maximum symbolic data structure depth of 9 objects.
  • The authors evaluated UC-KLEE’s checkers on over 20,000 functions from BIND, OpenSSL, and the Linux kernel.
  • The authors used the same minor code modifications described in § 3.2.1, and the authors again used a maximum input
Conclusion
  • Conclusions and future work

    The authors have presented UC-KLEE, a novel framework for validating patches and applying checkers to individual C/C++ functions using under-constrained symbolic execution.
  • One avenue for future work is to employ UC-KLEE as a tool for finding general bugs in a single version of a function, rather than cross-checking two functions or using specialized checkers.
  • The authors' preliminary experiments have shown that this use case results in a much higher rate of false positives, but the authors did find a number of interesting bugs, including the OpenSSL denial-of-service attack for which advisory CVE-2015-0291 [15, 22, 42] was issued.
  • The authors may target higher-level languages in the future, allowing the framework to assume many built-in invariants
Related work
  • This paper builds on prior work in symbolic execution [4], particularly KLEE [5] and our early work on UCKLEE [43]. Unlike our previous work, which targeted small library routines, this paper targets large systems

    62 24th USENIX Security Symposium and supports generalized checking.

    Other recent work has used symbolic execution to check patches. DiSE [39] performs whole program symbolic execution but prunes paths unaffected by a patch. Differential Symbolic Execution (DSE) [38] and regression verification [21] use abstraction to achieve scalability but may report false differences. By contrast, our approach soundly executes complete paths through each patched function, eliminating this source of false positives. Impact Summaries [2] complement our approach by soundly pruning paths and ignoring constraints unaffected by a patch.
Funding
  • This work was supported by DARPA under agreements 1190029-276707 and N660011024088, by the United States Air Force Research Laboratory (AFRL) through contract FA8650-10-C-7024, and by a National Science Foundation Graduate Research Fellowship under grant number DGE-0645962
Reference
  • Alert (TA14-098A): OpenSSL ’Heartbleed’ vulnerability (CVE2014-0160). https://www.us-cert.gov/ncas/alerts/ TA14-098A, April 2014.
    Findings
  • BACKES, J., PERSON, S., RUNGTA, N., AND TKACHUK, O. Regression verification using impact summaries. In Proc. of SPIN Symposium on Model Checking of Software (SPIN) (2013).
    Google ScholarLocate open access versionFindings
  • BIND. https://www.isc.org/downloads/bind/.[4] BOYER, R. S., ELSPAS, B., AND LEVITT, K. N. Select – a formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices 10, 6 (June 1975), 234–45.
    Locate open access versionFindings
  • [5] CADAR, C., DUNBAR, D., AND ENGLER, D. KLEE: Unassisted and automatic generation of high-coverage tests for complex sys- 24th USENIX Security Symposium 63 tems programs. In Proc. of Symp. on Operating Systems Design and Impl (OSDI) (2008).
    Google ScholarLocate open access versionFindings
  • [6] CHOU, A. On detecting heartbleed with static analysis. http://security.coverity.com/blog/2014/Apr/ on-detecting-heartbleed-with-static-analysis. html, 2014.
    Findings
  • [7] CLAUSE, J., LI, W., AND ORSO, A. Dytan: a generic dynamic taint analysis framework. In Proc. of Intl. Symp. on Software Testing and Analysis (ISSTA) (2007).
    Google ScholarLocate open access versionFindings
  • [8] CUI, H., HU, G., WU, J., AND YANG, J. Verifying systems rules using rule-directed symbolic execution. In Proc. of Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2013).
    Google ScholarLocate open access versionFindings
  • [9] CVE-2008-1447: DNS Cache Poisoning Issue (”Kaminsky bug”). https://kb.isc.org/article/AA-00924.
    Findings
  • [10] CVE-2012-3868. https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2012-3868, Jul 2012.
    Findings
  • [11] CVE-2014-0160. https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2014-0160, April 2014.
    Findings
  • [12] CVE-2014-0198. https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2014-0198, May 2014.
    Findings
  • [13] CVE-2014-3513. https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2014-3513, Oct 2014.
    Findings
  • [14] CVE-2015-0206. https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2015-0206, Jan 2015.
    Findings
  • [15] CVE-2015-0291. https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2015-0291, Mar 2015.
    Findings
  • [16] CVE-2015-0292. https://web.nvd.nist.gov/view/vuln/detail?vulnId=CVE-2015-0292, Mar 2015.
    Findings
  • [17] DENG, X., LEE, J., AND ROBBY. Bogor/kiasan: A k-bounded symbolic execution for checking strong heap properties of open systems. In Proc. of the 21st IEEE International Conference on Automated Software Engineering (2006), pp. 157–166.
    Google ScholarLocate open access versionFindings
  • [18] ENGLER, D., AND DUNBAR, D. Under-constrained execution: making automatic code destruction easy and scalable. In Proc. of the Intl. Symposium on Software Testing and Analysis (ISSTA) (2007).
    Google ScholarLocate open access versionFindings
  • [19] ENGLER, D., YU CHEN, D., HALLEM, S., CHOU, A., AND CHELF, B. Bugs as deviant behavior: A general approach to inferring errors in systems code. In Proc. of the 18th ACM Symposium on Operating Systems Principles (SOSP ’01) (2001).
    Google ScholarLocate open access versionFindings
  • [20] FREIER, A. RFC 6101: The Secure Sockets Layer (SSL) Protocol Version 3.0. Internet Engineering Task Force (IETF), Aug 2011.
    Google ScholarFindings
  • [21] GODLIN, B., AND STRICHMAN, O. Regression verification: proving the equivalence of similar programs. Software Testing, Verification and Reliability 23, 3 (2013), 241–258.
    Google ScholarLocate open access versionFindings
  • [22] GOODIN, D. OpenSSL warns of two high-severity bugs, but no Heartbleed. Ars Technica (March 2015).
    Google ScholarLocate open access versionFindings
  • [23] HASTINGS, R., AND JOYCE, B. Purify: Fast detection of memory leaks and access errors. In Proc. of the USENIX Winter Technical Conference (USENIX Winter ’92) (Dec. 1992), pp. 125– 138.
    Google ScholarLocate open access versionFindings
  • [24] HAUSWIRTH, M., AND CHILIMBI, T. M. Low-overhead memory leak detection using adaptive statistical profiling. In Proc. of the Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS) (2004).
    Google ScholarLocate open access versionFindings
  • [25] INTERNATIONAL TELECOMMUNICATION UNION. ITU-T Recommendation X.680: Abstract Syntax Notation One (ASN.1): Specification of basic notation, Nov 2008.
    Google ScholarFindings
  • [26] KHURSHID, S., PASAREANU, C. S., AND VISSER, W. Generalized symbolic execution for model checking and testing. In Proc. of Intl. Conf. on Tools and Algos. for the Construction and Analysis of Sys. (2003).
    Google ScholarFindings
  • [27] LAHIRI, S., HAWBLITZEL, C., KAWAGUCHI, M., AND REBELO, H. SymDiff: A language-agnostic semantic diff tool for imperative programs. In Proc. of Intl. Conf. on Computer Aided Verification (CAV) (2012).
    Google ScholarLocate open access versionFindings
  • [28] LAHIRI, S. K., MCMILLAN, K. L., SHARMA, R., AND HAWBLITZEL, C. Differential assertion checking. In Proc. of Joint Meeting on Foundations of Software Engineering (FSE) (2013).
    Google ScholarLocate open access versionFindings
  • [29] LATTNER, C., AND ADVE, V. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In Proc. of the Intl. Symp. on Code Generation and Optimization (CGO) (2004).
    Google ScholarLocate open access versionFindings
  • [30] LUK, C.-K., COHN, R., MUTH, R., PATIL, H., KLAUSER, A., LOWNEY, G., WALLACE, S., REDDI, V. J., AND HAZELWOOD, K. Pin: building customized program analysis tools with dynamic instrumentation. In Proc. of ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI) (2005).
    Google ScholarLocate open access versionFindings
  • [31] MARINESCU, P. D., AND CADAR, C. High-coverage symbolic patch testing. In Proc. of Intl. SPIN Symp. on Model Checking Software (2012).
    Google ScholarLocate open access versionFindings
  • [32] MARINESCU, P. D., AND CADAR, C. KATCH: High-coverage testing of software patches. In Proc. of 9th Joint Mtg. on Foundations of Software Engineering (FSE) (2013).
    Google ScholarLocate open access versionFindings
  • [33] NECULA, G. C., MCPEAK, S., AND WEIMER, W. Ccured: type-safe retrofitting of legacy code. In Proc. of Symp. on Principles of Programming Languages (POPL) (2002).
    Google ScholarLocate open access versionFindings
  • [34] NETHERCOTE, N., AND SEWARD, J. Valgrind: a framework for heavyweight dynamic binary instrumentation. In Proc. of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI ’07) (June 2007), pp. 89–100.
    Google ScholarLocate open access versionFindings
  • [35] NEWSOME, J., AND SONG, D. Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software. In Proc. of Network and Distributed Systems Security Symp. (NDSS) (2005).
    Google ScholarLocate open access versionFindings
  • [36] OpenSSL. https://www.openssl.org/source.
    Findings
  • [37] PARTUSH, N., AND YAHAV, E. Abstract semantic differencing for numerical programs. In Proc. of Intl. Static Analysis Symposium (SAS) (2013).
    Google ScholarLocate open access versionFindings
  • [38] PERSON, S., DWYER, M. B., ELBAUM, S., AND PA SA REANU, C. S. Differential symbolic execution. In Proc. of ACM SIGSOFT Intl. Symposium on Foundations of Software Engineering (FSE) (2008), pp. 226–237.
    Google ScholarLocate open access versionFindings
  • [39] PERSON, S., YANG, G., RUNGTA, N., AND KHURSHID, S. Directed incremental symbolic execution. In Proc. of ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI) (2011).
    Google ScholarLocate open access versionFindings
  • [40] PA SA REANU, C. S., AND RUNGTA, N. Symbolic PathFinder: Symbolic execution of java bytecode. In Proc. of the IEEE/ACM International Conf. on Automated Software Engineering (ASE) (2010).
    Google ScholarLocate open access versionFindings
  • [41] QI, D., ROYCHOUDHURY, A., AND LIANG, Z. Test generation to expose changes in evolving programs. In Proc. of IEEE/ACM Intl. Conf. on Automated Software Engineering (ASE) (2010).
    Google ScholarLocate open access versionFindings
  • [42] RAMOS, D. A. Under-constrained symbolic execution: correctness checking for real code. PhD thesis, Stanford University, 2015.
    Google ScholarFindings
  • [43] RAMOS, D. A., AND ENGLER, D. R. Practical, low-effort equivalence verification of real code. In Proc. of Intl. Conf. on Computer Aided Verification (CAV) (2011).
    Google ScholarLocate open access versionFindings
  • [44] UNANGST, T. Commit e76e308f (tedu): on today’s episode of things you didn’t want to learn. http://anoncvs.estpak.ee/cgi-bin/cgit/openbsd-src/commit/lib/libssl?id=e76e308f, Apr 2014.
    Findings
  • [45] XIE, Y., AND AIKEN, A. Context- and path-sensitive memory leak detection. In Proc. of the Intl. Symp. on Foundations of Software Engineering (FSE) (2005).
    Google ScholarLocate open access versionFindings
  • [46] XIE, Y., AND AIKEN, A. Scalable error detection using boolean satisfiability. In Proc. of the 32nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (POPL) (2005), pp. 351–363.
    Google ScholarLocate open access versionFindings
Author
David A. Ramos
David A. Ramos
Your rating :
0

 

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn
小科