Using safety properties to generate vulnerability patches

Zhen Huang, David Lie, Gang Tan, Trent Jaeger

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

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

Fingerprint

Repair
Program interpreters
Computer programming languages
Engines
Defects

All Science Journal Classification (ASJC) codes

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

Cite this

Huang, Z., Lie, D., Tan, G., & Jaeger, T. (2019). Using safety properties to generate vulnerability patches. In Proceedings - 2019 IEEE Symposium on Security and Privacy, SP 2019 (pp. 539-554). [8835226] (Proceedings - IEEE Symposium on Security and Privacy; Vol. 2019-May). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/SP.2019.00071
Huang, Zhen ; Lie, David ; Tan, Gang ; Jaeger, Trent. / Using safety properties to generate vulnerability patches. Proceedings - 2019 IEEE Symposium on Security and Privacy, SP 2019. Institute of Electrical and Electronics Engineers Inc., 2019. pp. 539-554 (Proceedings - IEEE Symposium on Security and Privacy).
@inproceedings{ffebbbfbb29949e39666082f4f6ed8db,
title = "Using safety properties to generate vulnerability patches",
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.",
author = "Zhen Huang and David Lie and Gang Tan and Trent Jaeger",
year = "2019",
month = "5",
doi = "10.1109/SP.2019.00071",
language = "English (US)",
series = "Proceedings - IEEE Symposium on Security and Privacy",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "539--554",
booktitle = "Proceedings - 2019 IEEE Symposium on Security and Privacy, SP 2019",
address = "United States",

}

Huang, Z, Lie, D, Tan, G & Jaeger, T 2019, Using safety properties to generate vulnerability patches. in Proceedings - 2019 IEEE Symposium on Security and Privacy, SP 2019., 8835226, Proceedings - IEEE Symposium on Security and Privacy, vol. 2019-May, Institute of Electrical and Electronics Engineers Inc., pp. 539-554, 40th IEEE Symposium on Security and Privacy, SP 2019, San Francisco, United States, 5/19/19. https://doi.org/10.1109/SP.2019.00071

Using safety properties to generate vulnerability patches. / Huang, Zhen; Lie, David; Tan, Gang; Jaeger, Trent.

Proceedings - 2019 IEEE Symposium on Security and Privacy, SP 2019. Institute of Electrical and Electronics Engineers Inc., 2019. p. 539-554 8835226 (Proceedings - IEEE Symposium on Security and Privacy; Vol. 2019-May).

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

TY - GEN

T1 - Using safety properties to generate vulnerability patches

AU - Huang, Zhen

AU - Lie, David

AU - Tan, Gang

AU - Jaeger, Trent

PY - 2019/5

Y1 - 2019/5

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85072917463&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85072917463&partnerID=8YFLogxK

U2 - 10.1109/SP.2019.00071

DO - 10.1109/SP.2019.00071

M3 - Conference contribution

AN - SCOPUS:85072917463

T3 - Proceedings - IEEE Symposium on Security and Privacy

SP - 539

EP - 554

BT - Proceedings - 2019 IEEE Symposium on Security and Privacy, SP 2019

PB - Institute of Electrical and Electronics Engineers Inc.

ER -

Huang Z, Lie D, Tan G, Jaeger T. Using safety properties to generate vulnerability patches. In Proceedings - 2019 IEEE Symposium on Security and Privacy, SP 2019. Institute of Electrical and Electronics Engineers Inc. 2019. p. 539-554. 8835226. (Proceedings - IEEE Symposium on Security and Privacy). https://doi.org/10.1109/SP.2019.00071