FuSeBMC: A White-Box Fuzzer for Finding Security Vulnerabilities in C Programs (Competition Contribution)

被引：6

作者：

Alshmrany, Kaled M. ^{[1
]}

Menezes, Rafael S. ^{[2
]}

Gadelha, Mikhail R. ^{[3
]}

Cordeiro, Lucas C. ^{[4
]}

机构：

[1] Univ Manchester, Inst Publ Adm, Jeddah, Saudi Arabia

[2] Univ Fed Amazonas, Manaus, Amazonas, Brazil

[3] SIDIA Inst Ciencia & Tecnol, Manaus, Amazonas, Brazil

[4] Univ Manchester, Manchester, Lancs, England

来源：

FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2021) | 2021年 / 12649卷

基金：

英国工程与自然科学研究理事会;

关键词：

Automated Test-Case Generation; Symbolic Execution; Bounded Model Checking; Fuzzing; Security;

D O I：

10.1007/978-3-030-71500-7_19

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We describe and evaluate a novel white-box fuzzer for C programs named FuSeBMC, which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. FuSeBMC explores and analyzes C programs (1) to find execution paths that lead to property violations and (2) to incrementally inject labels to guide the fuzzer and the BMC engine to produce test-cases for code coverage. FuSeBMC successfully participates in Test-Comp'21 and achieves first place in the Cover-Error category and second place in the Overall category.

引用

页码：363 / 367

页数：5

共 8 条

[1] An orchestrated survey of methodologies for automated software test case generation [J].

Anand, Saswat ;

Burke, Edmund K. ;

Chen, Tsong Yueh ;

Clark, John ;

Cohen, Myra B. ;

Grieskamp, Wolfgang ;

Harman, Mark ;

Harrold, Mary Jean ;

McMinn, Phil ;

Bertolino, Antonia ;

Li, J. Jenny ;

Zhu, Hong .

JOURNAL OF SYSTEMS AND SOFTWARE, 2013, 86 (08) :1978-2001

[2] Second Competition on Software Testing: Test-Comp 2020 [J].

Beyer, Dirk .

FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2020), 2020, 12076 :505-519

[3] ESBMC: Scalable and Precise Test Generation based on the Floating-Point Theory (Competition Contribution) [J].

Gadelha, Mikhail R. ;

Menezes, Rafael ;

Monteiro, Felipe R. ;

Cordeiro, Lucas C. ;

Nicole, Denis .

FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING (FASE 2020), 2020, 12076 :525-529

[4] An Efficient Floating-Point Bit-Blasting API for Verifying C Programs [J].

Gadelha, Mikhail R. ;

Cordeiro, Lucas C. ;

Nicole, Denis A. .

SOFTWARE VERIFICATION, VSTTE 2020, NSV 2020, 2020, 12549 :178-195

[5] ESBMC v6.0: Verifying C Programs Using k-Induction and Invariant Inference (Competition Contribution) [J].

Gadelha, Mikhail R. ;

Monteiro, Felipe ;

Cordeiro, Lucas ;

Nicole, Denis .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, 2019, 11429 :209-213

[6] ESBMC 5.0 An Industrial-Strength C Model Checker [J].

Gadelha, Mikhail R. ;

Monteiro, Felipe R. ;

Morse, Jeremy ;

Cordeiro, Lucas C. ;

Fischer, Bernd ;

Nicole, Denis A. .

PROCEEDINGS OF THE 2018 33RD IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMTED SOFTWARE ENGINEERING (ASE' 18), 2018, :888-891

[7] Map2Check Using LLVM and KLEE [J].

Menezes, Rafael ;

Rocha, Herbert ;

Cordeiro, Lucas ;

Barreto, Raimundo .

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT II, 2018, 10806 :437-441

[8]

Niemetz A., 2014, Journal on Satisfiability, Boolean Modelling and Computation, V9, P53, DOI [10.3233/sat190101, DOI 10.3233/SAT190101]

← 1 →