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 » Using Formal Methods to Eliminate Exploitable Bugs
Tweet

connect with us

Using Formal Methods to Eliminate Exploitable Bugs

Thursday, August 13, 2015 - 2:00pm-3:30pm

Kathleen Fisher, Tufts University

Abstract: 

For decades, formal methods have offered the promise of software that doesn’t have exploitable bugs. Until recently, however, it hasn’t been possible to verify software of sufficient complexity to be useful. Recently, that situation has changed. SeL4 is an open-source operating system microkernel efficient enough to be used in a wide range of practical applications. It has been proven to be fully functionally correct, ensuring the absence of buffer overflows, null pointer exceptions, use-after-free errors, etc., and to enforce integrity and confidentiality properties. The CompCert Verifying C Compiler maps source C programs to provably equivalent assembly language, ensuring the absence of exploitable bugs in the compiler. A number of factors have enabled this revolution in the formal methods community, including increased processor speed, better infrastructure like the Isabelle/HOL and Coq theorem provers, specialized logics for reasoning about low-level code, increasing levels of automation afforded by tactic languages and SAT/SMT solvers, and the decision to move away from trying to verify existing artifacts and instead focus on co-developing the code and the correctness proof. In this talk I will explore the promise and limitations of current formal methods techniques for producing useful software that provably does not contain exploitable bugs. I will discuss these issues in the context of DARPA’s HACMS program, which has as its goal the creation of high-assurance software for vehicles, including quad-copters, helicopters, and automobiles.

Kathleen Fisher is Professor in the Computer Science Department at Tufts University. Previously, she was a Principal Member of the Technical Staff at AT&T Labs Research, a Consulting Faculty Member in the Computer Science Department at Stanford University, and a program manager at DARPA where she started and managed the HACMS and PPAML programs. Kathleen's research focuses on advancing the theory and practice of programming languages and on applying ideas from the programming language community to the problem of ad hoc data management. The main thrust of her work has been in domain-specific languages to facilitate programming with massive amounts of ad hoc data. Kathleen is an ACM Fellow. She has served as program chair for FOOL, ICFP, CUFP, and OOPSLA. Kathleen is past Chair of the ACM Special Interest Group in Programming Languages (SIGPLAN), past Co-Chair of CRA's Committee on the Status of Women (CRA-W), a former editor of the Journal of Functional Programming, and an associated editor of TOPLAS.

Kathleen Fisher, Tufts 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.

View the slides

Presentation Video 

Presentation Audio

MP3 Download

Download Audio

  • 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