This article discusses a new technique to automatically generate test cases for object oriented programs. At the state of the art, the problem of generating adequate sets of complete test cases has not been satisfactorily solved yet. There are various techniques to automatically generate test cases (random testing, search-based testing, etc.) but each one has its own weaknesses. This article proposes an approach that distinctively combines dynamic symbolic execution, search-based testing and machine learning, to efficiently generate thorough class-level test suites. The preliminary data obtained carrying out some experiments confirm that we are going in the right direction.
Symbolic execution is a powerful systematic software analysis technique, but suffers from the high cost of constraint solving, which is the key supporting technology that affects the effectiveness of symbolic execution. Techniques like Green and GreenTrie reuse constraint solutions to speed up constraint solving for symbolic execution; however, these reuse techniques require syntactic/semantic equivalence or implication relationship between constraints. This paper introduces DeepSover, a novel approach to constraint solving with deep learning for symbolic execution. Our key insight is to utili…
Recent efforts in practical symbolic execution have successfully mitigated the path-explosion problem to some extent with search-based heuristics and compositional approaches. Similarly, due to an increase in the performance of cheap multi-core commodity computers, fuzzing as a viable method of random mutation-based testing has also seen promise. However, the possibility of combining symbolic execution and fuzzing, thereby providing an opportunity to mitigate drawbacks in each other, has not been sufficiently explored. Fuzzing could, for example, expedite path-exploration in symbolic execution…
Symbolic execution now becomes an indispensable technique for software testing and program analysis. There are several symbolic execution tools available off-the-shelf, and we need a practical benchmark approach to learn their capabilities. Therefore, this paper introduces a novel approach to benchmark symbolic execution tools in a fine-grained and efficient manner. In particular, our approach evaluates the performance of such tools against the known challenges faced by general symbolic execution techniques, such as floating-point numbers and symbolic memories. To this end, we first survey rel…
Fuzzing and symbolic execution are popular techniques for finding vulnerabilities and generating test-cases for programs. Fuzzing, a blackbox method that mutates seed input values, is generally incapable of generating diverse inputs that exercise all paths in the program. Due to the path-explosion problem and dependence on SMT solvers, symbolic execution may also not achieve high path coverage. A hybrid technique involving fuzzing and symbolic execution may achieve better function coverage than fuzzing or symbolic execution alone. In this paper, we present Munch, an open source framework imple…
We present a technique to automatically generate search heuristics for dynamic symbolic execution. A key challenge in dynamic symbolic execution is how to effectively explore the program's execution paths to achieve high code coverage in a limited time budget. Dynamic symbolic execution employs a search heuristic to address this challenge, which favors exploring particular types of paths that are most likely to maximize the final coverage. However, manually designing a good search heuristic is nontrivial and typically ends up with suboptimal and unstable outcomes. The goal of this paper is to …
In this presentation, we introduce our constraint-based repair approach, called SymDefFix. SymDefFix is based on ExtractFix [3] and replaces the dynamic analysis steps of ExtractFix to detect the error and find the potential fix locations in an input program with symbolic execution. We first briefly motivate and introduce our modifications of ExtractFix, and then demonstrate it with an example.
Regression testing ensures that a software system when it evolves still performs correctly and that the changes introduce no unintended side-effects. However, the creation of regression test cases that show divergent behavior needs a lot of effort. A solution is the idea of shadow symbolic execution, originally implemented based on KLEE for programs written in C, which takes a unifed version of the old and the new program and performs symbolic execution guided by concrete values to explore the changed behavior. In this work, we apply the idea of shadow symbolic execution to Java programs and, …
Symbolic execution is a classic technique for systematic bug finding, which has seen many applications in recent years but remains hard to scale. Recent work introduced ranged symbolic execution to distribute the symbolic execution task among different workers with minimal communication overhead using test inputs. However, each worker was restricted to perform only a depth-first search. This paper introduces a new approach to ranging, called test-depth partitioning, that allows the workers to employ different search strategies without compromising the completeness of the overall search. Experi…
Hybrid testing approaches that involve fuzz testing and symbolic execution have shown promising results in achieving high code coverage, uncovering subtle errors and vulnerabilities in a variety of software applications. In this paper we describe Badger - a new hybrid approach for complexity analysis, with the goal of discovering vulnerabilities which occur when the worst-case time or space complexity of an application is significantly higher than the average case. Badger uses fuzz testing to generate a diverse set of inputs that aim to increase not only coverage but also a resource-related co…
We introduce SeMu, a Dynamic Symbolic Execution technique that generates test inputs capable of killing stubborn mutants (killable mutants that remain undetected after a reasonable amount of testing). SeMu aims at mutant propagation (triggering erroneous states to the program output) by incrementally searching for divergent program behaviours between the original and the mutant versions. We model the mutant killing problem as a symbolic execution search within a specific area in the programs' symbolic tree. In this framework, the search area is defined and controlled by parameters that allow s…
Integrating Symbolic Execution with LLMs for Automated Generation of Program Specifications
Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；UCAS（中国科学院大学）；Sch. of Computer Science & Sch. of Artificial Intelligence, Shanghai Jiao Tong University（上海交通大学计算机科学与技术学院与人工智能学院）；School of Computer Science, Peking University（北京大学计算机学院）；Beijing Institute of Control Engineering（北京控制工程研究所）
Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numerical domains, existing symbolic execution techniques for heap-based programs are limited due to the lack of a succinct and precise description for symbolic values over unbounded heaps. In this work, we present a new symbolic execution method for heap-based programs based on separation logic. The essence of our proposal is context-sensitive lazy initialization, a novel approach for efficient test input generation. Our approach differs from existing approaches in two…
Many popular blockchain platforms are supporting smart contracts for building decentralized applications. However, the vulnerabilities within smart contracts have led to serious financial loss to their end users. For the EOSIO blockchain platform, effective vulnerability detectors are still limited. Furthermore, existing vulnerability detection tools can only support one blockchain platform. In this work, we present WANA, a cross-platform smart contract vulnerability detection tool based on the symbolic execution of WebAssembly bytecode. Furthermore, WANA proposes a set of test oracles to dete…
Dynamic symbolic execution is a widely used technique for automated software testing, designed for execution paths exploration and program errors detection. A hybrid approach has recently become widespread, when the main goal of symbolic execution is helping fuzzer increase program coverage. The more branches symbolic executor can invert, the more useful it is for fuzzer. A program control flow often depends on memory values, which are obtained by computing address indexes from user input. However, most DSE tools don't support such dependencies, so they miss some desired program branches. We i…
Automated test generation based on symbolic execution can be beneficial for systematically testing safety-critical software, to facilitate test engineers to pursue the strict testing requirements mandated by the certification standards, while controlling at the same time the costs of the testing process. At the same time, the development of safety-critical software is often constrained with programming languages or coding conventions that ban linguistic features which are believed to downgrade the safety of the programs, e.g., they do not allow dynamic memory allocation and variable-length arr…
The main reason for the standardization of network protocols, like QUIC, is to ensure interoperability between implementations, which poses a challenging task. Manual tests are currently used to test the different existing implementations for interoperability, but given the complex nature of network protocols, it is hard to cover all possible edge cases. State-of-the-art automated software testing techniques, such as Symbolic Execution (SymEx), have proven themselves capable of analyzing complex real-world software and finding hard to detect bugs. We present a SymEx-based method for finding in…
Guided fuzzing has, in recent years, been able to uncover many new vulnerabilities in real-world software due to its fast input mutation strategies guided by path-coverage. However, most fuzzers are unable to achieve high coverage in deeper parts of programs. Moreover, fuzzers heavily rely on the diversity of the seed inputs, often manually provided, to be able to produce meaningful results. In this paper, we present Wildfire, a novel open-source compositional fuzzing framework. Wildfire finds vulnerabilities by fuzzing isolated functions in a C-program and, then, using targeted symbolic execu…
Certification through auditing allows to ensure that critical embedded systems are secure. This entails reviewing their critical components and checking for dangerous execution paths. This latter task requires the use of specialized tools which allow to explore and replay executions but are also difficult to use effectively within the context of the audit, where time and knowledge of the code are limited. Fault analysis is especially tricky as the attacker may actively influence execution, rendering some common methods unusable and increasing the number of possible execution paths exponentiall…
IIT Kanpur（印度理工学院坎普尔分校）；National University of Singapore（新加坡国立大学）
Symbolic execution is a powerful technique for bug finding and program testing. It is successful in finding bugs in real-world code. The core reasoning techniques use constraint solving, path exploration, and search, which are also the same techniques used in solving combinatorial problems, e.g., finite-domain constraint satisfaction problems (CSPs). We propose CSP instances as more challenging benchmarks to evaluate the effectiveness of the core techniques in symbolic execution. We transform CSP benchmarks into C programs suitable for testing the reasoning capabilities of symbolic execution t…
Symbolic execution has shown its ability to find security-relevant flaws in software, but faces significant scalability challenges. There is a commonly held belief that manual intervention by an expert can help alleviate these limiting factors. However, there has been little formal investigation of this idea. In this paper, we present our experiences applying the KLEE symbolic execution engine to a new bug corpus, and of using manual intervention to alleviate the issues encountered. Our contributions are (1) Hemiptera, a novel corpus of over 130 bugs in real world software, (2) a comprehensive…
An effective way to maximize code coverage in software tests is through dynamic symbolic execution$-$a technique that uses constraint solving to systematically explore a program's state space. We introduce an open-source dynamic symbolic execution framework called Manticore for analyzing binaries and Ethereum smart contracts. Manticore's flexible architecture allows it to support both traditional and exotic execution environments, and its API allows users to customize their analysis. Here, we discuss Manticore's architecture and demonstrate the capabilities we have used to find bugs and verify…
Dynamic Symbolic Execution (DSE) is an important method for the testing of programs. An important system on DSE is KLEE which inputs a C/C++ program annotated with symbolic variables, compiles it into LLVM, and then emulates the execution paths of LLVM using a specified backtracking strategy. The major challenge in symbolic execution is path explosion. The method of abstraction learning has been used to address this. The key step here is the computation of an interpolant to represent the learnt abstraction. In this paper, we present a new interpolation algorithm and implement it on top of the …
Dynamic symbolic execution (DSE) is an effective method for automated program testing and bug detection. It is increasing the code coverage by the complex branches exploration during hybrid fuzzing. DSE tools invert the branches along some execution path and help fuzzer examine previously unavailable program parts. DSE often faces over- and underconstraint problems. The first one leads to significant analysis complication while the second one causes inaccurate symbolic execution. We propose strong optimistic solving method that eliminates irrelevant path predicate constraints for target branch…
Misconfiguration is a major cause of system failures. Prior solutions focus on detecting invalid settings that are introduced by user mistakes. But another type of misconfiguration that continues to haunt production services is specious configuration--settings that are valid but lead to unexpectedly poor performance in production. Such misconfigurations are subtle, so even careful administrators may fail to foresee them. We propose a tool called Violet to detect such misconfiguration. We realize the crux of specious configuration is that it causes some slow code path to be executed, but the ba…
We describe a technique for systematic testing of multi-threaded programs. We combine Quasi-Optimal Partial-Order Reduction, a state-of-the-art technique that tackles path explosion due to interleaving non-determinism, with symbolic execution to handle data non-determinism. Our technique iteratively and exhaustively finds all executions of the program. It represents program executions using partial orders and finds the next execution using an underlying unfolding semantics. We avoid the exploration of redundant program traces using cutoff events. We implemented our technique as an extension of…
Deep Neural Networks (DNN) are increasingly used in a variety of applications, many of them with substantial safety and security concerns. This paper introduces DeepCheck, a new approach for validating DNNs based on core ideas from program analysis, specifically from symbolic execution. The idea is to translate a DNN into an imperative program, thereby enabling program analysis to assist with DNN validation. A basic translation however creates programs that are very complex to analyze. DeepCheck introduces novel techniques for lightweight symbolic analysis of DNNs and applies them in the conte…
Enhancing Reliability of Symbolic Execution Tools for Smart Contract Analysis through Rule-Based False Positive Reduction
Lakehead University（拉科德湖大学）；United Arab Emirates University（阿联酋大学）；German Research Center for Artificial Intelligence（德国人工智能研究中心）；National University of Computer and Emerging Sciences（巴基斯坦国立计算机与新兴科学大学）
Automatic test-case generation techniques of symbolic execution and fuzzing are the most widely used methods to discover vulnerabilities in, both, academia and industry. However, both these methods suffer from fundamental drawbacks that stop them from achieving high path coverage that may, consequently, lead to discovering vulnerabilities at the numerical scale of static analysis. In this presentation, we examine systems-under-test (SUTs) at the granularity level of functions and postulate that achieving higher function coverage (execution of functions in a program at least once) than, both, s…
CPU cache is a limited but crucial storage component in modern processors, whereas the cache timing side-channel may inadvertently leak information through the physically measurable timing variance. Speculative execution, an essential processor optimization, and a source of such variances, can cause severe detriment on deliberate branch mispredictions. Despite static analysis could qualitatively verify the timing-leakage-free property under speculative execution, it is incapable of producing endorsements including inputs and speculated flows to diagnose leaks in depth. This work proposes a new…
