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 条
  • [1] Ahrendt Wolfgang., 2016, Lecture Notes in Computer Science
  • [2] Fifty years of Hoare's logic
    Apt, Krzysztof R.
    Olderog, Ernst-Ruediger
    [J]. FORMAL ASPECTS OF COMPUTING, 2019, 31 (06) : 751 - 807
  • [3] Combining test case generation and runtime verification
    Artho, C
    Barringer, H
    Goldberg, A
    Havelund, K
    Khurshid, S
    Lowry, M
    Pasareanu, C
    Rosu, G
    Sen, K
    Visser, W
    Washington, R
    [J]. THEORETICAL COMPUTER SCIENCE, 2005, 336 (2-3) : 209 - 234
  • [4] Formal verification of security protocol implementations: a survey
    Avalle, Matteo
    Pironti, Alfredo
    Sisto, Riccardo
    [J]. FORMAL ASPECTS OF COMPUTING, 2014, 26 (01) : 99 - 123
  • [5] A Survey of Symbolic Execution Techniques
    Baldoni, Roberto
    Coppa, Emilio
    D'Elia, Daniele Cono
    Demetrescu, Camil
    Finocchi, Irene
    [J]. ACM COMPUTING SURVEYS, 2018, 51 (03) : 1 - 39
  • [6] Banks G, 2006, LECT NOTES COMPUT SC, V4176, P343
  • [7] Barner S, 2005, LECT NOTES COMPUT SC, V3576, P153
  • [8] Beckert B., 2007, Verification of Object-Oriented Software. The KeY Approach, P69
  • [9] Tests from Witnesses Execution-Based Validation of Verification Results
    Beyer, Dirk
    Dangl, Matthias
    Lemberger, Thomas
    Tautschnig, Michael
    [J]. TESTS AND PROOFS, TAP 2018, 2018, 10889 : 3 - 23
  • [10] Bhatkar S, 2003, USENIX ASSOCIATION PROCEEDINGS OF THE 12TH USENIX SECURITY SYMPOSIUM, P105