Paper Info
Title
Automated Generation of Buffer Overflow Quick Fixes Using Symbolic Execution and SMT.
Abstract
In many C programs, debugging requires significant effort and can consume a lot of time. Even if the bug's cause is known, detecting 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 Satisfiability 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 overhead 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.
Year
DOI
Venue
2015
10.1007/978-3-319-24255-2_32
SAFECOMP
Keywords
Field
DocType
Program repair, Symbolic execution, Software bugs
Test suite,Programming language,Computer science,Software bug,Symbolic execution,Software regression,Operating system,Buffer overflow,Debugging,Satisfiability modulo theories
Conference
Volume
ISSN
Citations 
9337
0302-9743
4
PageRank 
References 
Authors
0.39
21
4
Name
Order
Citations
PageRank
Paul Muntean1114.32
Vasantha Kommanapalli240.39
Andreas Ibing37215.39
Claudia Eckert47613.13