JMLKelinci plus : Detecting Semantic Bugs and Covering Branches with Valid Inputs Using Coverage-guided Fuzzing and Runtime Assertion Checking

被引:0
作者
Nilizadeh, Amirfarhad [1 ]
Leavens, Gary T. [1 ]
Pasareanu, Corina S. [2 ]
Noller, Yannic [3 ]
机构
[1] Univ Cent Florida, Orlando, FL USA
[2] Carnegie Mellon Univ, NASA Ames Res Ctr, Moffett Field, CA USA
[3] Natl Univ Singapore, Singapore, Singapore
关键词
Guided fuzzer; runtime assertion checking; testing; valid inputs; formal verification; semantic bug; branch coverage; TEST-CASE GENERATION; FORMAL VERIFICATION; JML; SPECIFICATION; ALGORITHMS; EXECUTION; DESIGN; SYSTEM; TOOL;
D O I
10.1145/3607538
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Testing to detect semantic bugs is essential, especially for critical systems. Coverage-guided fuzzing (CGF) and runtime assertion checking (RAC) are twowell-known approaches for detecting semantic bugs. CGF aims to generate test inputs with high code coverage. However, while CGF tools can be equipped with sanitizers to detect a fixed set of semantic bugs, they can otherwise only detect bugs that lead to a crash. Thus, the first problem we address is how to help fuzzers detect previously unknown semantic bugs that do not lead to a crash. Moreover, a CGF tool may not necessarily cover all branches with valid inputs, although invalid inputs are useless for detecting semantic bugs. So, the second problem is how to guide a fuzzer to maximize coverage using only valid inputs. However, RAC monitors the expected behavior of a program dynamically and can only detect a semantic bug when a valid test input shows that the program does not satisfy its specification. Thus, the third problem is how to provide high-quality test inputs for a RAC that can trigger potential bugs. The combination of a CGF tool and RAC solves these problems and can cover branches with valid inputs and detect semantic bugs effectively. Our study uses RAC to guarantee that only valid inputs reach the program under test using the program's specified preconditions, and it also uses RAC to detect semantic bugs using specified postconditions. A prototype tool was developed for this study, named JMLKelinci+. Our results show that combining a CGF tool with RAC will lead to executing the program under test only with valid inputs and that this technique can effectively detect semantic bugs. Also, this idea improves the feedback given to a CGF tool, enabling it to cover all branches faster in programs with non-trivial preconditions.(1)
引用
收藏
页数:24
相关论文
共 133 条
  • [51] Groce A, 2003, LECT NOTES COMPUT SC, V2648, P121
  • [52] GROCE A, 2015, ACM INT S SOFTW TEST, P414
  • [53] A Little Language for Testing
    Groce, Alex
    Pinto, Jervis
    [J]. NASA FORMAL METHODS (NFM 2015), 2015, 9058 : 204 - 218
  • [54] 7 MYTHS OF FORMAL METHODS
    HALL, A
    [J]. IEEE SOFTWARE, 1990, 7 (05) : 11 - 19
  • [55] A formal approach for the construction and verification of railway control systems
    Haxthausen, Anne E.
    Peleska, Jan
    Kinder, Sebastian
    [J]. FORMAL ASPECTS OF COMPUTING, 2011, 23 (02) : 191 - 219
  • [56] AN AXIOMATIC BASIS FOR COMPUTER PROGRAMMING
    HOARE, CAR
    [J]. COMMUNICATIONS OF THE ACM, 1969, 12 (10) : 576 - &
  • [57] Grammarinator: A Grammar-Based Open Source Fuzzer
    Hodovan, Renata
    Kiss, Akos
    Gyimothy, Tibor
    [J]. PROCEEDINGS OF THE 9TH ACM SIGSOFT INTERNATIONAL WORKSHOP ON AUTOMATING TEST CASE DESIGN, SELECTION, AND EVALUATION (A-TEST '18), 2018, : 45 - 48
  • [58] Towards formal verification of IoT protocols: A Review
    Hofer-Schmitz, Katharina
    Stojanovic, Branka
    [J]. COMPUTER NETWORKS, 2020, 174
  • [59] Hoffmann M. R., Java Code Coverage for Eclipse
  • [60] TSTL: the template scripting testing language
    Holmes, Josie
    Groce, Alex
    Pinto, Jervis
    Mittal, Pranjal
    Azimi, Pooria
    Kellar, Kevin
    O'Brien, James
    [J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2018, 20 (01) : 57 - 78