FuzzNT : Checking for Program Non-termination

被引:2
|
作者
Karmarkar, Hrishikesh [1 ]
Medicherla, Raveendra Kumar [1 ]
Metta, Ravindra [1 ]
Yeduru, Prasanth [1 ]
机构
[1] TCS Res, Chennai, Tamil Nadu, India
来源
2022 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE MAINTENANCE AND EVOLUTION (ICSME 2022) | 2022年
关键词
non termination; abstract interpretation; fuzzing; verification; testing; software maintenance; C PROGRAMS;
D O I
10.1109/ICSME55016.2022.00049
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Unintended non-termination of programs could lead to attacks such as Denial-of-Service(DoS). Current testing techniques are not geared to detect such errors. Towards this, we present FuzzNT, a hybrid testing technique to check non-termination of C programs by combining Coverage Guided Fuzzing (CGF) and abstract interpretation based static analysis. Given a program P and the coverage test inputs generated using CGF, P is transformed into a set of specialized programs, each of which under-approximates P. Abstract interpretation is then used to check each of these smaller programs for non-termination. The key advantage of this approach for checking non-termination is that it reuses the test case corpus created during software development and maintenance. Our preliminary experimental evaluation of FuzzNT shows highly promising results.
引用
收藏
页码:409 / 413
页数:5
相关论文
共 41 条
  • [21] A Compositional Method for Deciding Program Termination
    Dimovski, Aleksandar
    ICT INNOVATIONS 2010, 2011, 83 : 71 - 80
  • [22] Cyclic proofs of program termination in separation logic
    Brotherston, James
    Bornat, Richard
    Calcagno, Cristiano
    ACM SIGPLAN NOTICES, 2008, 43 (01) : 101 - 112
  • [23] Deductively Verified Program Models for Software Model Checking
    Amilon, Jesper
    Gurov, Dilian
    LEVERAGING APPLICATIONS OF FORMAL METHOD, VERIFICATION AND VALIDATION: SPECIFICATION AND VERIFICATION, PT III, ISOLA 2024, 2025, 15221 : 8 - 25
  • [24] Static program transformations for efficient software model checking
    Vasudevan, S
    Abraham, JA
    BUILDING THE INFORMATION SOCIETY, 2004, 156 : 257 - 281
  • [25] FORMAL MODELLING OF PROGRAM DEPENDENCE NET FOR SOFTWARE MODEL CHECKING
    Li, Shuo
    Ding, Zhijun
    Pan, Meiqin
    COMPUTING AND INFORMATICS, 2024, 43 (05) : 1161 - 1184
  • [26] Program checking with certificates: Separating correctness-critical code
    Glesner, S
    FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 758 - 777
  • [27] From Non-Zenoness Verification to Termination
    Ganty, Pierre
    Genaim, Samir
    Lal, Ratan
    Prabhakar, Pavithra
    2015 ACM/IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CODESIGN (MEMOCODE), 2015, : 228 - 237
  • [28] Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking
    Fadiheh, Mohammad Rahmani
    Stoffel, Dominik
    Barrett, Clark
    Mitra, Subhasish
    Kunz, Wolfgang
    2019 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE), 2019, : 994 - 999
  • [29] Sound Runtime Assertion Checking for Memory Properties via Program Transformation
    Ly, Dara
    Kosmatov, Nikolai
    Loulergue, Frederic
    Signoles, Julien
    FORMAL ASPECTS OF COMPUTING, 2024, 36 (01)
  • [30] Specifying Fairness Constraints and Model Checking with Non-intensional Strategies
    Rubio, Ruben
    Marti-Oliet, Narciso
    Pita, Isabel
    Verdejo, Alberto
    REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2024, 2024, 14953 : 145 - 162