Symbolic execution is a program analysis technique that aims to automatically identify interesting inputs for an application, using them to generate program executions covering different parts of the ...code. It is widely used in the context of vulnerability discovery and reverse engineering. In this paper we present SENinja, a symbolic execution plugin for the BinaryNinja disassembler. The tool allows the user to perform symbolic execution analyses directly within the user interface of the disassembler, and can be used to support a variety of reverse engineering tasks.
Symbolic execution is a well-known software testing technique that evaluates how a program runs when considering a symbolic input, i.e., an input that can initially assume any concrete value ...admissible for its data type. The dynamic twist of this technique is dubbed concolic execution and has been demonstrated to be a practical technique for testing even complex real-world programs. Unfortunately, developing concolic engines is hard. Indeed, an engine has to correctly instrument the program to build accurate symbolic expressions, which represent the program computation. Furthermore, to reason over such expressions, it has to interact with an SMT solver. Hence, several implementation bugs may emerge within the different layers of an engine.
In this article, we consider the problem of testing concolic engines. In particular, we propose several testing strategies whose main intuition is to exploit the concrete state kept by the executor to identify inconsistencies within the symbolic state. We integrated our strategies into three state-of-the-art concolic executors (SymCC, SymQEMU, and Fuzzolic, respectively) and then performed several experiments to show that our ideas can find bugs in these frameworks. Overall, our approach was able to discover more than 12 bugs across these engines.
•We identify the main steps carried out by recent concolic frameworks during their analysis, pinpointing where implementation bugs may emerge.•We propose a set of novel and practical ideas on how to identify implementation gaps in modern concolic executors.•We integrate our strategies into state-of-the-art concolic executors and perform experiments to show that our ideas can find bugs in these frameworks.
In the last few years, a large variety of approaches and methodologies have been explored in the context of software testing, ranging from black-box techniques, such as fuzzing, to white-box ...techniques, such as concolic execution, with a full spectrum of instances in between. Using these techniques, developers and security researchers have been able to identify in the last decade a large number of critical vulnerabilities in thousands of software projects.
In this article, we investigate how to improve the performance and effectiveness of concolic execution, proposing two main enhancements to the original approach. On one side, we devise a novel concolic executor that can analyze complex binary programs while running under QEMU and efficiently produce symbolic queries, which could generate valuable program inputs when solved. On the other side, we investigate whether techniques borrowed from the fuzzing domain can be applied to solve the symbolic queries generated by concolic execution, providing a viable alternative to accurate but expensive SMT solving techniques. We show that the combination of our concolic engine, Fuzzolic, and our approximate solver, Fuzzy-Sat, can perform better in terms of code coverage than popular state-of-the-art fuzzers on a variety of complex programs and can identify different unknown bugs in several real-world applications.
In this paper we develop simple and fast multicore parallel algorithms for counting the number of k-cliques in large undirected graphs, for any small constant k ≥ 4. Clique counting is an important ...problem in a variety of network analytics applications. Differently from existing solutions, which mainly target distributed memory settings (e.g., MapReduce), our algorithms work on off-the-shelf shared-memory multicore platforms.
We assess the effectiveness of our approach through an extensive experimental analysis on a variety of real-world graphs, considering different clique sizes and scalability on different numbers of cores. The experimental results show that our parallel algorithms largely outperform the running times of highly optimized sequential solutions and gracefully scale to non-trivial values of k even on medium/large graphs. For instance, computing hundreds of billions of cliques for rather demanding Web graphs and social networks requires about 15 min on a 32-core machine. As a by-product of our experimental analysis, we also compute the exact number of k-cliques with at most 20 nodes in many real-world networks from the SNAP repository.
Fuzzing Symbolic Expressions Borzacchiello, Luca; Coppa, Emilio; Demetrescu, Camil
2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)
Conference Proceeding
Recent years have witnessed a wide array of results in software testing, exploring different approaches and methodologies ranging from fuzzers to symbolic engines, with a full spectrum of instances ...in between such as concolic execution and hybrid fuzzing. A key ingredient of many of these tools is Satisfiability Modulo Theories (SMT) solvers, which are used to reason over symbolic expressions collected during the analysis. In this paper, we investigate whether techniques borrowed from the fuzzing domain can be applied to check whether symbolic formulas are satisfiable in the context of concolic and hybrid fuzzing engines, providing a viable alternative to classic SMT solving techniques. We devise a new approximate solver, FUZZY-SAT, and show that it is both competitive with and complementary to state-of-the-art solvers such as Z3 with respect to handling queries generated by hybrid fuzzers.
On the Dissection of Evasive Malware DElia, Daniele Cono; Coppa, Emilio; Palmaro, Federico ...
IEEE transactions on information forensics and security,
01/2020, Volume:
15
Journal Article
Peer reviewed
Open access
Complex malware samples feature measures to impede automatic and manual analyses, making their investigation cumbersome. While automatic characterization of malware benefits from recently proposed ...designs for passive monitoring, the subsequent dissection process still sees human analysts struggling with adversarial behaviors, many of which also closely resemble those studied for automatic systems. This gap affects the day-to-day analysis of complex samples and researchers have not yet attempted to bridge it. We make a first step down this road by proposing a design that can reconcile transparency requirements with manipulation capabilities required for dissection. Our open-source prototype BluePill (i) offers a customizable execution environment that remains stealthy when analysts intervene to alter instructions and data or run third-party tools, (ii) is extensible to counteract newly encountered anti-analysis measures using insights from the dissection, and (iii) can accommodate program analyses that aid analysts, as we explore for taint analysis. On a set of highly evasive samples BluePill resulted as stealthy as commercial sandboxes while offering new intervention and customization capabilities for dissection.
Largely known for attack scenarios, code reuse techniques at a closer look reveal properties that are appealing also for program obfuscation. We explore the popular return-oriented programming ...paradigm under this light, transforming program functions into ROP chains that coexist seamlessly with the surrounding software stack. We show how to build chains that can withstand popular static and dynamic deobfuscation approaches, evaluating the robustness and overheads of the design over common programs. The results suggest a significant amount of computational resources would be required to carry a deobfuscation attack for secret finding and code coverage goals.
Summary
Symbolic execution is a popular program analysis technique that allows seeking for bugs by reasoning over multiple alternative execution states at once. As the number of states to explore may ...grow exponentially, a symbolic executor may quickly run out of space. For instance, a memory access to a symbolic address may potentially reference the entire address space, leading to a combinatorial explosion of the possible resulting execution states. To cope with this issue, state‐of‐the‐art executors either concretize symbolic addresses that span memory intervals larger than some threshold or rely on advanced capabilities of modern satisfiability modulo theories solvers. Unfortunately, concretization may result in missing interesting execution states, for example, where a bug arises, while offloading the entire problem to constraint solvers can lead to very large query times. In this article, we first contribute to systematizing knowledge about memory models for symbolic execution, discussing how four mainstream symbolic executors deal with symbolic addresses. We then introduce MemSight, a new approach to symbolic memory that reduces the need for concretization: rather than mapping address instances to data as previous approaches do, our technique maps symbolic address expressions to data, maintaining the possible alternative states resulting from the memory referenced by a symbolic address in a compact, implicit form. Experiments on prominent programs show that MemSight, which we implemented in both Angr and Klee, enables the exploration of states that are unreachable for memory models that perform concretization and provides a performance level comparable with memory models relying on advanced solver theories.
PDF
