Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Home
  • Attend
    • Registration Information
    • Registration Discounts
    • Venue, Hotel, and Travel
    • Students and Grants
    • Co-located Events
      • SOUPS 2016
      • HotCloud '16
      • HotStorage '16
  • Program
    • At a Glance
    • Technical Sessions
  • Activities
    • Birds-of-a-Feather Sessions
    • Poster Session
  • Participate
    • Instructions for Authors and Speakers
    • Call for Papers
    • Call for Practitioner Talks
  • Sponsorship
  • About
    • Organizers
    • Help Promote!
    • Questions
    • Past Conferences
  • Home
  • Attend
  • Program
  • Activities
  • Participate
  • Sponsorship
  • About

sponsors

Gold Sponsor
Gold Sponsor
Gold Sponsor
Gold Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Industry Partner
Industry Partner
Industry Partner

help promote

USENIX ATC '16

Get
Help Promote graphics!

connect with us


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by @usenix

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home ยป Under-Constrained Symbolic Execution: Correctness Checking for Real Code
Tweet

connect with us

Under-Constrained Symbolic Execution: Correctness Checking for Real Code

Authors: 

David A. Ramos and Dawson Engler, Stanford University

Best Paper at USENIX Security '15: Link to Paper

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, rather than whole programs. We present UC-KLEE, a novel, scalable framework for checking C/C++ systems code, along with two use cases. First, we use UC-KLEE to check whether patches introduce crashes. We check over 800 patches from BIND and OpenSSL and find 12 bugs, including two OpenSSL denial-of-service vulnerabilities. We also verify (with caveats) that 115 patches do not introduce crashes. Second, we use UC-KLEE as a generalized checking framework and implement checkers to find memory leaks, uninitialized data, and unsafe user input. We evaluate the checkers on over 20,000 functions from BIND, OpenSSL, and the Linux kernel, find 67 bugs, and verify that hundreds of functions are leak free and that thousands of functions do not access uninitialized data.

David A. Ramos, Stanford University

Dawson Engler, Stanford University

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {196225,
author = {David A. Ramos and Dawson Engler},
title = {{Under-Constrained} Symbolic Execution: Correctness Checking for Real Code},
booktitle = {2016 USENIX Annual Technical Conference (USENIX ATC 16)},
year = {2016},
address = {Denver, CO},
url = {https://www.usenix.org/conference/atc16/technical-sessions/presentation/ramos},
publisher = {USENIX Association},
month = jun,
}
Download

Presentation Audio

MP3 Download

Download Audio

  • Log in or    Register to post comments

Gold Sponsors

Silver Sponsors

Media Sponsors & Industry Partners

© USENIX

  • Privacy Policy
  • Contact Us