Automated Generation of Buffer Overflows Quick Fixes using Symbolic Execution and SMT
In many C programs, debugging requires significant effort and can consume a lot of time. Even if the bug’s cause is known, detect- ing a bug in such programs and generating a bug fix patch manually is a tedious task. In this paper, we present a novel approach used to generate bug fixes for buffer overflow automatically using static execution, code patch patterns, quick fix locations, user input saturation and Satisfia- bility Modulo Theories (SMT). The generated patches are syntactically correct, can be semi-automatically inserted into code and do not need additional human refinement. We evaluated our approach on 58 C open source programs contained in the Juliet test suite and measured an over- head of 0.59 % with respect to the bug detection time. We think that our approach is generalizable and can be applied with other bug checkers that we developed.
Automated Generation of Buffer Overflows Quick Fixes using Symbolic Execution and SMT
International Conference on Computer Safety, Reliability & Security (SAFECOMP), Delft, The Netherlands, September 2015. Springer LNCS
| Authors: | Paul Muntean, Vasantha Kommanapalli, Andreas Ibing, and Claudia Eckert |
| Year/month: | 2015/9 |
| Booktitle: | International Conference on Computer Safety, Reliability & Security (SAFECOMP), Delft, The Netherlands, September 2015. Springer LNCS |
| Editor: | LNCS |
| Fulltext: | safecomp15.pdf |
Abstract |
|
| In many C programs, debugging requires significant effort and can consume a lot of time. Even if the bug’s cause is known, detect- ing a bug in such programs and generating a bug fix patch manually is a tedious task. In this paper, we present a novel approach used to generate bug fixes for buffer overflow automatically using static execution, code patch patterns, quick fix locations, user input saturation and Satisfia- bility Modulo Theories (SMT). The generated patches are syntactically correct, can be semi-automatically inserted into code and do not need additional human refinement. We evaluated our approach on 58 C open source programs contained in the Juliet test suite and measured an over- head of 0.59 % with respect to the bug detection time. We think that our approach is generalizable and can be applied with other bug checkers that we developed. | |
Bibtex:
@inproceedings { SAFECOMP'15,author = { Paul Muntean and Vasantha Kommanapalli and Andreas Ibing and Claudia Eckert},
title = { Automated Generation of Buffer Overflows Quick Fixes using Symbolic Execution and SMT },
year = { 2015 },
month = { September },
booktitle = { International Conference on Computer Safety, Reliability & Security (SAFECOMP), Delft, The Netherlands, September 2015. Springer LNCS },
editor = { LNCS },
url = {https://www.sec.in.tum.de/i20/publications/automated-generation-of-buffer-overflows-quick-fixes-using-symbolic-execution-and-smt/@@download/file/safecomp15.pdf}
}