Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Home
  • Attend
    • Venue, Hotel, and Travel
    • Students and Grants
    • Co-Located Workshops
  • Program
    • At a Glance
    • Technical Sessions
    • Poster Session
  • Activities
    • Birds-of-a-Feather Sessions
    • Poster Session
    • WiPs
  • Participate
    • Call for Papers
      • Important Dates
      • Symposium Organizers
      • Symposium Topics
      • Refereed Papers
      • Shadow PC
      • Symposium Activities
      • Submitting Papers
    • Instructions for Participants
  • Sponsorship
  • About
    • Symposium Organizers
    • Services
    • Questions
    • Help Promote!
    • Past Symposia
  • Home
  • Attend
    • Venue, Hotel, and Travel
    • Students and Grants
    • Co-Located Workshops
  • Program
  • Activities
  • Participate
    • Call for Papers
    • Instructions for Participants
  • Sponsorship
  • About
    • Symposium Organizers
    • Services
    • Questions
    • Help Promote!
    • Past Symposia

sponsors

Platinum Sponsor
Gold Sponsor
Gold Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Bronze Sponsor
Bronze Sponsor
General 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

help promote

USENIX Security '16 button

Get more
Help Promote graphics!

connect with usenix


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by USENIXSecurity

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
Awarded Best 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.

Ramos PDF
View the slides

Presentation Video 

Presentation Audio

MP3 Download

Download Audio

Award: 
Best Paper
  • Log in or    Register to post comments

Open access to the USENIX Security '15 videos sponsored by Symantec.

Platinum Sponsors

Gold Sponsors

Silver Sponsors

Bronze Sponsors

General Sponsors

Media Sponsors & Industry Partners

Open Access Publishing Partner

© USENIX

  • Privacy Policy
  • Contact Us