Using safety properties to generate vulnerability patches

Zhen Huang, David Lie, Gang Tan, Trent Jaeger

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

Security vulnerabilities are among the most critical software defects in existence. When identified, programmers aim to produce patches that prevent the vulnerability as quickly as possible, motivating the need for automatic program repair (APR) methods to generate patches automatically. Unfortunately, most current APR methods fall short because they approximate the properties necessary to prevent the vulnerability using examples. Approximations result in patches that either do not fix the vulnerability comprehensively, or may even introduce new bugs. Instead, we propose property-based APR, which uses human-specified, program-independent and vulnerability-specific safety properties to derive source code patches for security vulnerabilities. Unlike properties that are approximated by observing the execution of test cases, such safety properties are precise and complete. The primary challenge lies in mapping such safety properties into source code patches that can be instantiated into an existing program. To address these challenges, we propose Senx, which, given a set of safety properties and a single input that triggers the vulnerability, detects the safety property violated by the vulnerability input and generates a corresponding patch that enforces the safety property and thus, removes the vulnerability. Senx solves several challenges with property-based APR: it identifies the program expressions and variables that must be evaluated to check safety properties and identifies the program scopes where they can be evaluated, it generates new code to selectively compute the values it needs if calling existing program code would cause unwanted side effects, and it uses a novel access range analysis technique to avoid placing patches inside loops where it could incur performance overhead. Our evaluation shows that the patches generated by Senx successfully fix 32 of 42 real-world vulnerabilities from 11 applications including various tools or libraries for manipulating graphics/media files, a programming language interpreter, a relational database engine, a collection of programming tools for creating and managing binary programs, and a collection of basic file, shell, and text manipulation tools.

Original languageEnglish (US)
Title of host publicationProceedings - 2019 IEEE Symposium on Security and Privacy, SP 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages539-554
Number of pages16
ISBN (Electronic)9781538666609
DOIs
StatePublished - May 2019
Event40th IEEE Symposium on Security and Privacy, SP 2019 - San Francisco, United States
Duration: May 19 2019May 23 2019

Publication series

NameProceedings - IEEE Symposium on Security and Privacy
Volume2019-May
ISSN (Print)1081-6011

Conference

Conference40th IEEE Symposium on Security and Privacy, SP 2019
CountryUnited States
CitySan Francisco
Period5/19/195/23/19

All Science Journal Classification (ASJC) codes

  • Safety, Risk, Reliability and Quality
  • Software
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Using safety properties to generate vulnerability patches'. Together they form a unique fingerprint.

Cite this