Taint Analysis of Security Code in the KLEE Symbolic Execution Engine

2012 ◽  
pp. 264-275 ◽  
Author(s):  
Ricardo Corin ◽  
Felipe Andrés Manzano
Keyword(s):  
Symbolic Execution ◽  
Taint Analysis ◽  
Execution Engine

scholarly journals The Optimization of a Symbolic Execution Engine for Detecting Runtime Errors

2017 ◽  
Vol 23 (2) ◽  
pp. 573-597
Author(s):  
István Kádár
Keyword(s):  
Search Strategy ◽  
Symbolic Execution ◽  
Real Life ◽  
Time Frame ◽  
Basic Block ◽  
Test Execution ◽  
Execution Engine ◽  
Branching Points ◽  
Java Programs ◽  
Null Pointer

In a software system, most of the runtime failures may come to light only during test execution, and this may have a very high cost. To help address this problem, a symbolic execution engine called RTEHunter, which has been developed at the Department of Software Engineering at the University of Szeged, is able to detect runtime errors (such as null pointer dereference, bad array indexing, division by zero) in Java programs without actually running the program in a real-life environment. Applying the theory of symbolic execution, RTEHunter builds a tree, called a symbolic execution tree, composed of all the possible execution paths of the program. RTEHunter detects runtime issues by traversing the symbolic execution tree and if a certain condition is fulfilled the engine reports an issue. However, as the number of execution paths increases exponentially with the number of branching points, the exploration of the whole symbolic execution tree becomes impossible in practice. To overcome this problem, different kinds of constraints can be set up over the tree. E.g. the number of symbolic states, the depth of the execution tree, or the time consumption could be restricted. Our goal in this study is to find the optimal parametrization of RTEHunter in terms of the maximum number of states, maximum depth of the symbolic execution tree and search strategy in order to find more runtime issues in a shorter time. Results on three open-source Java systems demonstrate that more runtime issues can be detected in the 0 to 60 basic block-depth levels than in deeper ones within the same time frame. We also developed two novel search strategies for traversing the tree based on the number of null pointer references in the program and on linear regression that performs better than the default depth-first search strategy.

An analysis on secure coding using symbolic execution engine

2016 ◽  
Vol 12 (3) ◽  
pp. 177-184 ◽  
Author(s):  
Joon-Ho Kim ◽  
Myung-Chul Ma ◽  
Jae-Pyo Park
Keyword(s):  
Symbolic Execution ◽  
Execution Engine ◽  
Secure Coding

Tuning parallel symbolic execution engine for better performance

2017 ◽  
Vol 12 (1) ◽  
pp. 86-100 ◽  
Author(s):  
Anil Kumar Karna ◽  
Jinbo Du ◽  
Haihao Shen ◽  
Hao Zhong ◽  
Jiong Gong ◽  
...  
Keyword(s):  
Symbolic Execution ◽  
Execution Engine

scholarly journals BugMiner: Mining the Hard-to-Reach Software Vulnerabilities through the Target-Oriented Hybrid Fuzzer

Electronics ◽  
2020 ◽  
Vol 10 (1) ◽  
pp. 62
Author(s):  
Fayozbek Rustamov ◽  
Juhwan Kim ◽  
Jihyeon Yu ◽  
Hyunwook Kim ◽  
Joobeom Yun
Keyword(s):  
Real World ◽  
Symbolic Execution ◽  
Automated Software Testing ◽  
Software Vulnerabilities ◽  
Concolic Execution ◽  
Execution Engine ◽  
Innovative Methodology ◽  
Target Sites ◽  
Dynamic Symbolic Execution ◽  
Automated Software

Greybox Fuzzing is the most reliable and essentially powerful technique for automated software testing. Notwithstanding, a majority of greybox fuzzers are not effective in directed fuzzing, for example, towards complicated patches, as well as towards suspicious and critical sites. To overcome these limitations of greybox fuzzers, Directed Greybox Fuzzing (DGF) approaches were recently proposed. Current DGFs are powerful and efficient approaches that can compete with Coverage-Based Fuzzers. Nevertheless, DGFs neglect to accomplish stability between usefulness and proficiency, and random mutations make it hard to handle complex paths. To alleviate this problem, we propose an innovative methodology, a target-oriented hybrid fuzzing tool that utilizes a fuzzer and dynamic symbolic execution (also referred to as a concolic execution) engine. Our proposed method aims to generate inputs that can quickly reach the target sites in each sequence and trigger potential hard-to-reach vulnerabilities in the program binary. Specifically, to dive deep into the target binary, we designed a proposed technique named BugMiner, and to demonstrate the capability of our implementation, we evaluated it comprehensively on bug hunting and crash reproduction. Evaluation results showed that our proposed implementation could not only trigger hard-to-reach bugs 3.1, 4.3, 2.9, 2.0, 1.8, and 1.9 times faster than Hawkeye, AFLGo, AFL, AFLFast, QSYM, and ParmeSan respectively but also scale to several real-world programs.

Sign in / Sign up

Export Citation Format

Share Document