Intraprocedural Analysis Based on Symbolic Execution for Bug Detection

2021 ◽  
Vol 47 (8) ◽  
pp. 858-865
Author(s):  
A. E. Borodin ◽  
I. A. Dudina
Keyword(s):  
Symbolic Execution ◽  
Bug Detection

scholarly journals CONFUZZIUS: A Data Dependency-Aware Hybrid Fuzzer for Smart Contracts

2021 ◽  
Author(s):  
Christof Ferreira Torres ◽  
Antonio Ken Iannillo ◽  
Arthur Gervais ◽  
Radu State
Keyword(s):  
State Of The Art ◽  
Symbolic Execution ◽  
Hybrid Approach ◽  
Data Dependency ◽  
Smart Contracts ◽  
Dependency Analysis ◽  
Bug Detection ◽  
Code Coverage ◽  
Traditional Programs ◽  
Turing Complete

<div> <div> <p>Smart contracts are Turing-complete programs that are executed across a blockchain. Unlike traditional programs, once deployed, they cannot be modified. As smart contracts carry more value, they become more of an exciting target for attackers. Over the last years, they suffered from exploits costing millions of dollars due to simple programming mistakes. As a result, a variety of tools for detecting bugs have been proposed. Most of these tools rely on symbolic execution, which may yield false positives due to over-approximation. Recently, many fuzzers have been proposed to detect bugs in smart contracts. However, these tend to be more effective in finding shallow bugs and less effective in finding bugs that lie deep in the execution, therefore achieving low code coverage and many false negatives. An alternative that has proven to achieve good results in traditional programs is hybrid fuzzing, a combination of symbolic execution and fuzzing. In this work, we study hybrid fuzzing on smart contracts and present ConFuzzius, the first hybrid fuzzer for smart contracts. ConFuzzius uses evolutionary fuzzing to exercise shallow parts of a smart contract and constraint solving to generate inputs that satisfy complex conditions that prevent evolutionary fuzzing from exploring deeper parts. Moreover, ConFuzzius leverages dynamic data dependency analysis to efficiently generate sequences of transactions that are more likely to result in contract states in which bugs may be hidden. We evaluate the effectiveness of ConFuzzius by comparing it with state-of-the-art symbolic execution tools and fuzzers for smart contracts. Our evaluation on a curated dataset of 128 contracts and a dataset of 21K real-world contracts shows that our hybrid approach detects more bugs than state-of-the-art tools (up to 23%) and that it outperforms existing tools in terms of code coverage (up to 69%). We also demonstrate that data dependency analysis can boost bug detection up to 18%.</p> </div> </div>

scholarly journals Symbolic Execution Based Intra-Procedural Analysis for Search for Defects

2020 ◽  
Vol 32 (6) ◽  
pp. 87-100
Author(s):  
Alexey Evgenevich Borodin ◽  
Irina Aleksandrovna Dudina
Keyword(s):  
Symbolic Execution ◽  
Analysis Tool ◽  
Bug Detection ◽  
Call Graph ◽  
Quality Of Reports ◽  
Speed Up ◽  
Abstract Domains ◽  
Value Numbering ◽  
Static Analysis Tool

Svace is a static analysis tool for bug detection in C/C++/Java source code. To analyze a program, Svace performs an intra-procedure analysis of individual functions, starting from the leaves of a call-graph and moving towards the roots, and uses summaries of previously analyzed procedures at call-cites. In this paper, we overview the approaches and techniques employed by Svace for the intra-procedural analysis. This phase is performed by an analyzer engine and an extensible set of detectors. The core engine employs a symbolic execution approach with state merging. It uses value numbering to reduce the set of symbolic expressions, maintains points-to relationship graph for memory modeling, and performs strong and weak updates of program values. Detectors are responsible for discovering and reporting bugs. They calculate different properties of program values using a variety of abstract domains. All detectors work simultaneously orchestrated by the engine. Svace analysis is unsound and employs a variety of heuristics to speed-up. We designed Svace to analyze big projects (several MLOCs) in just a few hours and report as many warnings as possible, while keeping a good quality of reports ≥ 65 of true positives). For example, Tizen 5.5 (20MLOC) analysis takes 8.6 hours and produces 18,920 warnings, more than 70% of which are true-positive.

scholarly journals Diversifying Focused Testing for Unit Testing

2021 ◽  
Vol 30 (4) ◽  
pp. 1-24
Author(s):  
Héctor D. Menéndez ◽  
Gunel Jahangirova ◽  
Federica Sarro ◽  
Paolo Tonella ◽  
David Clark
Keyword(s):  
Search Algorithm ◽  
Symbolic Execution ◽  
Specific Area ◽  
Test Suite ◽  
Constraint Solving ◽  
Test Case ◽  
Unit Testing ◽  
Bug Detection ◽  
Mutation Score ◽  
The Given

Software changes constantly, because developers add new features or modifications. This directly affects the effectiveness of the test suite associated with that software, especially when these new modifications are in a specific area that no test case covers. This article tackles the problem of generating a high-quality test suite to cover repeatedly a given point in a program, with the ultimate goal of exposing faults possibly affecting the given program point. Both search-based software testing and constraint solving offer ready, but low-quality, solutions to this: Ideally, a maximally diverse covering test set is required, whereas search and constraint solving tend to generate test sets with biased distributions. Our approach, Diversified Focused Testing (DFT), uses a search strategy inspired by GödelTest. We artificially inject parameters into the code branching conditions and use a bi-objective search algorithm to find diverse inputs by perturbing the injected parameters, while keeping the path conditions still satisfiable. Our results demonstrate that our technique, DFT, is able to cover a desired point in the code at least 90% of the time. Moreover, adding diversity improves the bug detection and the mutation killing abilities of the test suites. We show that DFT achieves better results than focused testing, symbolic execution, and random testing by achieving from 3% to 70% improvement in mutation score and up to 100% improvement in fault detection across 105 software subjects.

scholarly journals CONFUZZIUS: A Data Dependency-Aware Hybrid Fuzzer for Smart Contracts

2021 ◽  
Author(s):  
Christof Ferreira Torres ◽  
Antonio Ken Iannillo ◽  
Arthur Gervais ◽  
Radu State
Keyword(s):  
State Of The Art ◽  
Symbolic Execution ◽  
Hybrid Approach ◽  
Data Dependency ◽  
Smart Contracts ◽  
Dependency Analysis ◽  
Bug Detection ◽  
Code Coverage ◽  
Traditional Programs ◽  
Turing Complete

<div> <div> <p>Smart contracts are Turing-complete programs that are executed across a blockchain. Unlike traditional programs, once deployed, they cannot be modified. As smart contracts carry more value, they become more of an exciting target for attackers. Over the last years, they suffered from exploits costing millions of dollars due to simple programming mistakes. As a result, a variety of tools for detecting bugs have been proposed. Most of these tools rely on symbolic execution, which may yield false positives due to over-approximation. Recently, many fuzzers have been proposed to detect bugs in smart contracts. However, these tend to be more effective in finding shallow bugs and less effective in finding bugs that lie deep in the execution, therefore achieving low code coverage and many false negatives. An alternative that has proven to achieve good results in traditional programs is hybrid fuzzing, a combination of symbolic execution and fuzzing. In this work, we study hybrid fuzzing on smart contracts and present ConFuzzius, the first hybrid fuzzer for smart contracts. ConFuzzius uses evolutionary fuzzing to exercise shallow parts of a smart contract and constraint solving to generate inputs that satisfy complex conditions that prevent evolutionary fuzzing from exploring deeper parts. Moreover, ConFuzzius leverages dynamic data dependency analysis to efficiently generate sequences of transactions that are more likely to result in contract states in which bugs may be hidden. We evaluate the effectiveness of ConFuzzius by comparing it with state-of-the-art symbolic execution tools and fuzzers for smart contracts. Our evaluation on a curated dataset of 128 contracts and a dataset of 21K real-world contracts shows that our hybrid approach detects more bugs than state-of-the-art tools (up to 23%) and that it outperforms existing tools in terms of code coverage (up to 69%). We also demonstrate that data dependency analysis can boost bug detection up to 18%.</p> </div> </div>

Sign in / Sign up

Export Citation Format

Share Document