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

2021 ◽  
pp. 363-367 ◽  
Author(s):  
Kaled M. Alshmrany ◽  
Rafael S. Menezes ◽  
Mikhail R. Gadelha ◽  
Lucas C. Cordeiro
Keyword(s):  
Model Checking ◽  
Symbolic Execution ◽  
Bounded Model Checking ◽  
Test Cases ◽  
Security Vulnerabilities ◽  
C Programs ◽  
Code Coverage

AbstractWe describe and evaluate a novel white-box fuzzer for C programs named , which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. 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. successfully participates in Test-Comp’21 and achieves first place in the category and second place in the category.

scholarly journals Bounded model checking of C++ programs based on the Qt cross-platform framework

2017 ◽  
Vol 27 (3) ◽  
pp. e1632 ◽  
Author(s):  
Felipe R. Monteiro ◽  
Mário A. P. Garcia ◽  
Lucas C. Cordeiro ◽  
Eddie B. de Lima Filho
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
C Programs ◽  
Cross Platform

scholarly journals Handling loops in bounded model checking of C programs via k-induction

2015 ◽  
Vol 19 (1) ◽  
pp. 97-114 ◽  
Author(s):  
Mikhail Y. R. Gadelha ◽  
Hussama I. Ismail ◽  
Lucas C. Cordeiro
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
C Programs

Concurrent Bug Finding Based on Bounded Model Checking

2020 ◽  
Vol 30 (05) ◽  
pp. 669-694
Author(s):  
Milena Vujošević Janičić
Keyword(s):  
Model Checking ◽  
Software Verification ◽  
Symbolic Execution ◽  
Bounded Model Checking ◽  
Sequential Approach ◽  
Software Analysis ◽  
Verification Tool ◽  
Single Compound ◽  
Bug Finding ◽  
Reliable Software

Automated and reliable software verification is of crucial importance for development of high-quality software. Formal methods can be used for finding different kinds of bugs without executing the software, for example, for finding possible run-time errors. The methods like model checking and symbolic execution offer very precise static analysis but on real world programs do not always scale well. One way to tackle the scalability problem is to apply new concurrent and sequential approaches to complex algorithms used in these kinds of software analysis. In this paper, we compare different variants of bounded model checking and propose two concurrent approaches: concurrency of intra-procedural analysis and concurrency of inter-procedural analysis. We implemented these approaches in a software verification tool LAV, a tool that is based on bounded model checking and symbolic execution. For assessing the improvements gained, we experimentally compared the concurrent approaches with the standard bounded model checking approach (where all correctness conditions are put into a single compound formula) and with a sequential approach (where correctness conditions are checked separately, one after the other). The results show that, in many cases, the proposed concurrent approaches give significant improvements.

scholarly journals Cooperative verifier-based testing with CoVeriTest

2021 ◽  
Author(s):  
Dirk Beyer ◽  
Marie-Christine Jakobs
Keyword(s):  
Model Checking ◽  
Test Generation ◽  
Symbolic Execution ◽  
Bounded Model Checking ◽  
Test Suite ◽  
Hybrid Technique ◽  
Conditional Model ◽  
Level Information ◽  
High Level ◽  
Test Suite Generation

AbstractTesting is a widely applied technique to evaluate software quality, and coverage criteria are often used to assess the adequacy of a generated test suite. However, manually constructing an adequate test suite is typically too expensive, and numerous techniques for automatic test-suite generation were proposed. All of them come with different strengths. To build stronger test-generation tools, different techniques should be combined. In this paper, we study cooperative combinations of verification approaches for test generation, which exchange high-level information. We present CoVeriTest, a hybrid technique for test-suite generation. CoVeriTest iteratively applies different conditional model checkers and allows users to adjust the level of cooperation and to configure individual time limits for each conditional model checker. In our experiments, we systematically study different CoVeriTest cooperation setups, which either use combinations of explicit-state model checking and predicate abstraction, or bounded model checking and symbolic execution. A comparison with state-of-the-art test-generation tools reveals that CoVeriTest achieves higher coverage for many programs (about 15%).

scholarly journals Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

2020 ◽  
pp. 378-382
Author(s):  
Hernán Ponce-de-León ◽  
Florian Furbach ◽  
Keijo Heljanko ◽  
Roland Meyer
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Memory Models ◽  
Memory Model ◽  
Complete Analysis ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Model Checker ◽  
Safety Properties ◽  
C Programs

Abstract Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.

scholarly journals A Theory of Arrays with set and copy Operations

10.29007/q58t ◽  
2018 ◽  
Author(s):  
Stephan Falke ◽  
Carsten Sinz ◽  
Florian Merz
Keyword(s):  
Model Checking ◽  
Program Analysis ◽  
Software Verification ◽  
Symbolic Execution ◽  
Bounded Model Checking ◽  
Main Memory ◽  
Basic Theory ◽  
Analysis Software

The theory of arrays is widely used in order to model main memory in program analysis, software verification, bounded model checking, symbolic execution, etc. Nonetheless, the basic theory as introduced by McCarthy is not expressive enough for important practical cases since it only supports array updates at single locations. In programs, the memory is often modified using functions such as memset or memcpy/memmove, which modify a user-specified range of locations whose size might not be known statically. In this paper we present an extension of the theory of arrays with set and copy operations which make it possible to reason about such functions. We also discuss further applications of the theory.

Sign in / Sign up

Export Citation Format

Share Document