Search

Ethereum is the most widely used open-source public chain project, with smart contracts serving as the pattern for developing decentralized applications. The prevalence of attacks against smart contracts has increased in recent years due to the attached amounts of high-value cryptocurrency. Various attacks against smart contracts have caused significant financial losses, amounting to hundreds of millions of dollars. As manual auditing of smart contracts is time-consuming and costly, automatic detection of vulnerabilities is crucial. Existing work does not dig deeper into contextual information contained in the program, which suffers from the difficulty of covering paths with more complex conditions. In this paper, we propose Ethchecker, a smart contract vulnerability detection tool which combines fuzzing and symbolic execution techniques together. Particularly, we propose an analysis module to extract static information from smart contracts. Besides, the tool introduces a genetic algorithm to enlarge code coverage, while considering the contextual information of the code. The results of the experiment show that in terms of F1-score for vulnerability detection, Ethchecker outperforms sFuzz by an average of 21.89% and outperforms Mythril by an average of 12.5%. Furthermore, in the comparison experiments on a dataset consisting of 1000 long smart contract codes (comprising over 3000 instructions), the proposed algorithm can improve the code coverage by 18.56% compared to the random fuzzing algorithm. In addition, we also used Ethchecker to test against 8922 randomly crawled real-world smart contracts. The result demonstrates the stability of this tool. [ABSTRACT FROM AUTHOR]

This article introduces novel tools to automatically generate pertinent Ada values in order to produce higher quality tests for Ada subprograms. A first tool will generate valid Ada values based on a structural analysis of the types of the parameters of the subprogram under test following various customizable strategies. Those values will then be filtered in order to satisfy the specifications of the subprogram, and new coverage criteria for executable specifications will be used to assess the relevance of the generated testsuite. This first set of values will then be used as seeds both for a fuzzing process, and a symbolic execution campaign, from which values of interest will be then extracted. This integrated process will enable users to generate a high value starting test corpus, which can then be expanded upon by domain-specific tests. [ABSTRACT FROM AUTHOR]

Summary: Constraint solving is the enabling technique for symbolic execution. The advancement of constraint solving boosts the development and application of symbolic execution. Modern Satisfiability Modulo Theories (SMT) solvers provide the mechanism of solving strategy, allowing users to control the solving procedure. This mechanism significantly improves the solver's generalization ability. We observe that the symbolic executions of different programs are different constraint solving problems. Therefore, we propose synthesizing solving strategies for a program to fit the program's symbolic execution best. To achieve this, we propose an adaptive framework for synthesizing solving strategies, in which the constraints are classified into different categories, and the solving strategies are synthesized for different categories on demand. We propose novel synthesis algorithms that combine the offline trained deep learning models and online tuning to synthesize the solving strategy. The algorithms balance the synthesis overhead and the improvement achieved by the synthesized solving strategy. We have implemented our method on the state‐of‐the‐art symbolic execution engine KLEE for C programs and Symbolic Pathfinder (SPF) for Java programs. The results of the extensive experiments indicate that our method effectively improves the efficiency of symbolic execution. For the Coreutils benchmark, our method, on average, increases the numbers of paths and queries by 74.37% and 73.94% under Breadth First Search (BFS), respectively. Besides, we applied our method to a different benchmark of C programs and a benchmark of Java programs to validate the generalization ability. The results demonstrate that for the C benchmark, our method increases the numbers of paths and queries by 71.09% and 70.60% under BFS, respectively; For the Java benchmark, our method increases the numbers of paths and queries by 50.31% and 49.93% under BFS, respectively. These results show that our method has a good generalization ability. [ABSTRACT FROM AUTHOR]

Automatic Exploit Generation (AEG) involves automatically discovering paths in a program that trigger vulnerabilities, thereby generating exploits. While there is considerable research on heap-related vulnerability detection, such as detecting Heap Overflow and Use After Free (UAF) vulnerabilities, among contemporary heap-automated exploit techniques, only certain automated exploit techniques can hijack program control flow to the shellcode. An important limitation of this approach is that it cannot effectively bypass Linux's protection mechanisms. To solve this problem, we introduced Automatic Advanced Heap Exploit Generation (AAHEG). It first applies symbolic execution to analyze heap-related primitives in files and then detects potential heap-related vulnerabilities without a source code. After identifying these vulnerabilities, AAHEG builds an exploit abstract syntax tree (AST) to identify one or more successful exploit strategies, such as fast bin attack and Safe-unlink. AAHEG then selects exploitable methods via an abstract syntax tree (AST) and performs final testing to produce the final exploit. AAHEG chose to generate advanced heap-related exploits because the exploits can bypass Linux protections. Basically, AAHEG can automatically detect heap-related vulnerabilities in binaries without source code, build an exploit AST, choose from a variety of advanced heap exploit methods, bypass all Linux protection mechanisms, and generate final file-form exploit based on pwntools which can pass local and remote testing. Experimental results show that AAHEG successfully completed vulnerability detection and exploit generation for 20 Capture The Flag (CTF) binary files, 11 of which have all protection mechanisms enabled. [ABSTRACT FROM AUTHOR]

Memory corruption is a serious class of software vulnerabilities, which requires careful attention to be detected and removed from applications before getting exploited and harming the system users. Symbolic execution is a well-known method for analyzing programs and detecting various vulnerabilities, e.g., memory corruption. Although this method is sound and complete in theory, it faces some challenges, such as path explosion, when applied to real-world complex programs. In this paper, we present a method for improving the efficiency of symbolic execution and detecting four classes of memory corruption vulnerabilities in executable codes, i.e., heap-based buffer overflow, stack-based buffer overflow, use-after-free, and double-free. We perform symbolic execution only on test units rather than the whole program to lower the chance of path explosion. In our method, test units are considered parts of the program's code, which might contain vulnerable statements and are statically identified based on the specifications of memory corruption vulnerabilities. Then, each test unit is symbolically executed to calculate path and vulnerability constraints for each statement of the unit, which determine the conditions on unit input data for executing that statement or activating vulnerabilities in it, respectively. Solving these constraints gives us input values for the test unit, which execute the desired statements and reveal vulnerabilities in them. Finally, we use machine learning to approximate the correlation between system and unit input data. Thereby, we generate system inputs that enter the program, reach vulnerable instructions in the desired test unit, and reveal vulnerabilities in them. This method is implemented as a plug-in for angr framework and evaluated using a group of benchmark programs. The experiments show its superiority over similar tools in accuracy and performance. [ABSTRACT FROM AUTHOR]

Security attacks abuse software vulnerabilities of IoT devices; hence, detecting and eliminating these vulnerabilities immediately are crucial. Fuzzing is an efficient method to identify vulnerabilities automatically, and many publications have been released to date. However, fuzzing for embedded systems has not been studied extensively owing to various obstacles, such as multi-architecture support, crash detection difficulties, and limited resources. Thus, the article introduces fuzzing techniques for embedded systems and the fuzzing differences for desktop and embedded systems. Further, we collect state-of-the-art technologies, discuss their advantages and disadvantages, and classify embedded system fuzzing tools. Finally, future directions for fuzzing research of embedded systems are predicted and discussed. [ABSTRACT FROM AUTHOR]

In this paper, we present an algebraic approach to the precise and global verification and explanation of Rectifier Neural Networks, a subclass of Piece-wise Linear Neural Networks (PLNNs), i.e., networks that semantically represent piece-wise affine functions. Key to our approach is the symbolic execution of these networks that allows the construction of semantically equivalent Typed Affine Decision Structures (TADS). Due to their deterministic and sequential nature, TADS can, similarly to decision trees, be considered as white-box models and therefore as precise solutions to the model and outcome explanation problem. TADS are linear algebras, which allows one to elegantly compare Rectifier Networks for equivalence or similarity, both with precise diagnostic information in case of failure, and to characterize their classification potential by precisely characterizing the set of inputs that are specifically classified, or the set of inputs where two network-based classifiers differ. All phenomena are illustrated along a detailed discussion of a minimal, illustrative example: the continuous XOR function. [ABSTRACT FROM AUTHOR]

The software packages of the Debian distribution include more than twenty-seven thousand maintainer scripts in total, almost all of them being written in the Posix shell language. These scripts are executed with root privileges at installation, update, and removal of a package, which makes them critical for system maintenance. While the Debian policy provides guidance for package maintainers producing the scripts, only few tools exist to check the compliance of a script to that policy. We present CoLiS, a software platform for discovering violations of non-trivial properties required by the Debian policy in maintainer scripts. We describe our methodology which is based on symbolic execution and feature tree constraints, and we give an overview of the toolchain. We obtain promising results: our toolchain is effective in analysing a large set of Debian maintainer scripts, and it has already detected over 150 policy violations that have led to bug reports, more than two-third of them now being fixed. [ABSTRACT FROM AUTHOR]

Fuzzing is an effective approach to discover bugs in programs, especially memory corruption bugs, using randomly generated test cases. However, without prior knowledge of the target program, the fuzzer can generate only a limited number of test cases because of sanity checks. To solve this problem, recent studies have proposed hybrid fuzzers that observe the context of a target program using symbolic execution; these fuzzers generate test cases to bypass the sanity check. While hybrid fuzzers explore "deep" bugs in the target program, they generate many ineffective test cases. In this paper, we propose a concolic execution algorithm that combines deep reinforcement learning with a hybrid fuzzing solution, Dr.PathFinder. When the reinforcement learning agent encounters a branch during concolic execution, it evaluates the state and determines the search path. In this process,"shallow" paths are pruned, and "deep" paths are searched first. This reduces unnecessary exploration, allowing the efficient memory usage and alleviating the state explosion problem. In experiments with the CB-multios dataset for deep bug cases, Dr.PathFinder discovered approximately five times more bugs than AFL and two times more than Driller-AFL. In addition to finding more bugs, Dr.PathFinder generated 19 times fewer test cases and used at least 2 % less memory than Driller-AFL. While it performed well in finding bugs located in deep paths, Dr.PathFinder had limitation to find bugs located at shallow paths, which we discussed. [ABSTRACT FROM AUTHOR]

In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, automatic checkpoints and reverse stepping, support for source-level information about functions and variables in C and C++ programs and structured heap visualisation. Additionally, DivSIM is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker, and with abstract bitcode generated by LART (LLVM Abstraction and Refinement Tool), making it suitable for direct analysis of abstract and/or symbolic programs and counterexamples. [ABSTRACT FROM AUTHOR]

Mutation testing is basically a fault-based software testing technique, which has been proposed to measure the fault detection effectiveness of a test suite using programs with simulated faults (namely mutants). However, mutation testing is time consuming and computationally expensive because of the normal use of a large amount of mutants. Thus, reducing the mutants is of great significance. To address this problem, various mutant reduction techniques have been proposed. Among them, the identification of redundant mutants aims at removing mutants whose test results can be inferred by other mutants. This article proposes a redundant mutant identification technique based on selective symbolic execution called ReMuSSE for weak mutation testing. Redundant mutants could be revealed by identifying those with similar program execution state changes within a program block involving mutated statements. An empirical study was conducted using 13 C programs from different application domains with varying sizes. The empirical results showed that ReMuSSE could identify up to 31.4% redundant mutants and consequentially save up to 35.2% time cost of weak mutation testing. The results demonstrated that ReMuSSE could effectively identify redundant mutants and thus could significantly improve the efficiency of weak mutation testing. [ABSTRACT FROM AUTHOR]

This special issue of Software Tools for Technology Transfer comprises extended versions of selected papers from the 26th edition of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020). The focus of this conference series is tools and algorithms for the rigorous analysis of software and hardware systems, and the papers in this special cover the spectrum of current work in this field. [ABSTRACT FROM AUTHOR]

Symbolic execution is a powerful technique for automating software testing to detect many types of errors such as memory errors and assertion violations. However, it encounters the problem of path explosion, and by using only assertions, it still lacks the capability of going deep into checking the functional correctness of a path based on corresponding formal specifications. To address these problems, we propose a specification-based incremental testing method with symbolic execution, called SIT-SE, providing a much more rigorous way to automatically check the functional correctness of all the discovered program paths, by introducing theorems (instead of assertions) for path correctness and branch sequence coverage algorithm for guiding a moderate path exploration. Compared with Hoare logic for proving the correctness of an entire program, a theorem in the SIT-SE is made for verifying the correctness of a program path. The proposed method carefully treats the relationship between a path condition and the specification in a theorem to restrict the monotonous path exploration, whereas traditional concolic testing methods roughly use one test data to determine the path correctness by assertions during long path searching. We use a classic case to demonstrate how the method works and conduct an experiment to evaluate the performance of both the proposed method and the commonly used well-known concolic testing tool KLEE. The experimental results show that our method SIT-SE is effective and outperforms KLEE in detecting faulty paths based on specifications. [ABSTRACT FROM AUTHOR]

Due to the immutable nature of the blockchain,smart contracts that have been deployed on the blockchain cannot be changed . In order to improve the security of the contract and prevent the smart contract from integer overflow, short address attacks, pseudo-random, etc, it is necessary that perform vulnerability detection on the contract before the contract have been deployed. This paper analyzed and researched the symbolic execution of the integer overflow vulnerability of the smart contract, and the investigation found that the detection speed of existing symbolic execution methods was slow. Then this paper proposed an improved symbolic execution method for solving constraints from the bottom, which combined depth first and breadth first path selection to improve code coverage of symbolic execution. The experimental results show that the improved symbolic execution has a detection accuracy rate of 84% in the selected 100 smart contracts containing overflow vulnerabilities, and the average detection efficiency has increased by 20% . The detection efficiency in medium-scale smart contracts has increased significantly, and the detection results have a higher accuracy high. [ABSTRACT FROM AUTHOR]

Symbolic execution is one of the most important testing techniques to ensure the quality of software systems that need to be dependable and reliable. This technique systematically explores the program of the subject system which is represented by an Inter-procedural Control Flow Graph (ICFG). An ICFG is a graph that combines Control Flow Graphs (CFGs) of the program procedures by connecting each CFG with its call nodes. The existence of unreachable CFGs and infinite loops increases the complexity and runtime of a program, while they have no effect on testing the program. In this paper, we present an approach to convert the ICFG of a program to the corresponding finite automaton, called ICFG-automaton. Then, we construct a quasi-ordering hypergroup on the set of states of the ICFG-automaton and prove that the inner irreducibility in hypergroups is equivalent to the connectivity in CFGs. Moreover, we show that if every sub-automaton of an ICFG-automaton is a sub-hypergroup, then the program has an infinite loop. These results identify the parts of a program that should be modified to decrease the complexity of the testing activity. [ABSTRACT FROM AUTHOR]

Symbiotic is a bug-finding and verification tool that integrates light-weight static analyses and instrumentation with program slicing and symbolic execution. The techniques are suitably combined according to a given goal. The paper describes a particular configuration competing in Test-Comp 2019. We also provide a brief analysis of Symbiotic 's results achieved in the competition. As our tool uses a fork of the open-source symbolic executor Klee, we focus on comparison with mainstream Klee that also participated in the competition this year. [ABSTRACT FROM AUTHOR]

In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KERNELC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KERNELC in the semantic framework, we enrich the symbolic execution facilities recently provided by with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented our technique in the automated tool KINDSPEC 2.1, which generates logical axioms that express pre- and post-condition assertions which define the precise input/output behavior of the C routines. Thanks to the integrated support for symbolic execution and deductive verification provided by , some synthesized axioms that cannot be guaranteed to be correct by construction due to abstraction can finally be verified in our setting with little effort. [ABSTRACT FROM AUTHOR]

We present an improved version of the memory safety verification approach implemented in Symbiotic 5, the winner of the MemSafety category at the Competition on Software Verification (SV-COMP) 2018. The approach can verify programs for standard errors in memory usage like invalid pointer dereference or memory leaking. It is based on instrumentation, static pointer analysis extended to consider memory deallocations, static program slicing, and symbolic execution. The improved version brings higher precision of the extended pointer analysis and further optimizations in instrumentation. It is implemented in the current version of Symbiotic, which contains also some improvements in program slicing and symbolic execution. We explain the approach in theory, describe implementation of selected components, and provide experimental results showing the impact of particular components. [ABSTRACT FROM AUTHOR]

The Symbolic Execution Debugger (SED), is an extension of the debug platform for interactive debuggers based on symbolic execution. The SED comes with a static symbolic execution engine for sequential programs, but any third-party symbolic execution engine can be integrated into the SED. An interactive debugger based on symbolic execution allows one like a traditional debugger to locate defects in the source code. The difference is that all feasible execution paths are explored at once, and thus there is no need to know input values resulting in an execution that exhibits the failure. In addition, such a debugger can be used in code reviews and to guide and present results of an analysis based on symbolic execution such as, in our case, correctness proofs. Experimental evaluations proved that the SED increases the effectiveness of code reviews and proof understanding tasks. [ABSTRACT FROM AUTHOR]

The format string vulnerability is a kind of software vulnerability which has high risk and wide impact. Currently, there are many limitations of vulnerability detection method, such as high degree of artificial dependence, high false positive rate, single detection model and failing to consider the characteristics of the format string vulnerability fully. To solve above problems, this paper analyzed the format string vulnerability. Based on symbolic execution, the paper designed and produced a way to detect formatted string vulnerability and generate test cases automatically. This method detected the existence of the format string vulnerability in Linux binary program automatically and determined whether it could lead to harm, which allowed attackers to read or write arbitrary memory. Meanwhile it generated stable and effective test cases. [ABSTRACT FROM AUTHOR]

Many security and software testing applications require checking whether certain properties of a program hold for any possible usage scenario. For instance, a tool for identifying software vulnerabilities may need to rule out the existence of any backdoor to bypass a program's authentication. One approach would be to test the program using different, possibly random inputs. As the backdoor may only be hit for very specific program workloads, automated exploration of the space of possible inputs is of the essence. Symbolic execution provides an elegant solution to the problem, by systematically exploring many possible execution paths at the same time without necessarily requiring concrete inputs. Rather than taking on fully specified input values, the technique abstractly represents them as symbols, resorting to constraint solvers to construct actual instances that would cause property violations. Symbolic execution has been incubated in dozens of tools developed over the past four decades, leading to major practical breakthroughs in a number of prominent software reliability applications. The goal of this survey is to provide an overview of the main ideas, challenges, and solutions developed in the area, distilling them for a broad audience. [ABSTRACT FROM AUTHOR]

To take advantage of multi-core systems, programmers are replacing sequential software with parallel software. Software engineers often avoid writing their parallel software from scratch and prefer refactoring their legacy application, either manually or with the help of a refactoring tool. In either case, it is extremely challenging to produce correct parallel code, taking into account all synchronization issues. Furthermore, the complexity of parallel code makes its verification extremely difficult. We introduce a method for the verification of parallel code after refactoring. Our method, which is based on symbolic interpretation, leverages the original sequential code that in most cases was already tested and/or verified, and checks whether it is equivalent to the code after refactoring. The advantage of this method is that it can generically find any problem in the parallel code that does not exist in the original sequential code. As a result, it can help create higher quality and safer parallel code. [ABSTRACT FROM AUTHOR]

Fault localisation, i.e. the identification of program locations that cause errors, takes significant effort and cost. We describe a fast model-based fault localisation algorithm that, given a test suite, uses symbolic execution methods to fully automatically identify a small subset of program locations where genuine program repairs exist. Our algorithm iterates over failing test cases and collects locations where an assignment change can repair exhibited faulty behaviour. Our main contribution is an improved search through the test suite, reducing the effort for the symbolic execution of the models and leading to speed-ups of more than two orders of magnitude over the previously published implementation by Griesmayer et al. We implemented our algorithm for C programs, using the KLEE symbolic execution engine, and demonstrate its effectiveness on the Siemens TCAS variants. Its performance is in line with recent alternative model-based fault localisation techniques, but narrows the location set further without rejecting any genuine repair locations where faults can be fixed by changing a single assignment. We also show how our tool can be used in an educational context to improve self-guided learning and accelerate assessment. We apply our algorithm to a large selection of actual student coursework submissions, providing precise localisation within a sub-second response time. We show this using small test suites, already provided in the coursework management system, and on expanded test suites, demonstrating the scalability of our approach. We also show compliance with test suites does not reliably grade a class of "almost-correct" submissions, which our tool highlights, as being close to the correct answer. Finally, we show an extension to our tool that extends our fast localisation results to a selection of student submissions that contain two faults. [ABSTRACT FROM AUTHOR]

Abstract: Currently, one of the most efficient ways to detect software security flaws is taint analysis. It can be based on static code analysis, and it helps detect bugs that lead to vulnerabilities, such as code injection or leaks of private data. Two approaches to the implementation of tainted data propagation over the program intermediate representation are proposed and compared. One of them is based on dataflow analysis (IFDS), and the other is based on symbolic execution. In this paper, the implementation of both approaches in the framework of the existing static analyzer infrastructure for detecting bugs in C# programs are described. These approaches are compared from the viewpoint of the scope of application, quality of results, performance, and resource requirements. Since both approaches use a common infrastructure for accessing information about the program and are implemented by the same team of developers, the results of the comparison are more significant and accurate than usual, and they can be used to select the best option in the context of the specific program and task. Our experiments show that it is possible to achieve the same completeness regardless of the chosen approach. The IFDS-based implementation has higher performance comparing with the symbolic execution for detectors with a small amount of tainted data sources. In the case of multiple detectors and a large number of sources, the scalability of the IFDS approach is worse than the scalability of the symbolic execution. [ABSTRACT FROM AUTHOR]

Constructing binary control flow graph is the base of analysing the binary security. The static method is efficient, while facing the precision shortage; dynamic analysis with the advantage of precision ,however is limited to its poor speed. This paper base on the characteristics of both static and dynamic method, put forward the combined method of binary control flow graph construct, with the base of control flow graph static constructed, using partial symbolic execution analysis and backward slicing analysis to compute the targets of indirect jumps, and then analyses the reachability of nodes and edges. Merging the unreachable nodes and edges. The experimental result shows that combined method with the similar efficiency of static analysis, far faster than dynamic method. It has a better precision compare with static method. [ABSTRACT FROM AUTHOR]

The Atlas Transformation Language (ATL) is currently one of the most used model transformation languages and has become a de facto standard in model-driven engineering for implementing model transformations. At the same time, it is understood by the community that enhancing methods for exhaustively verifying such transformations allows for a more widespread adoption of model-driven engineering in industry. A variety of proposals for the verification of ATL transformations have arisen in the past few years. However, the majority of these techniques are either based on non-exhaustive testing or on proof methods that require human assistance and/or are not complete. In this paper, we describe our method for statically verifying the declarative subset of ATL model transformations. This verification is performed by translating the transformation (including features like filters, OCL expressions, and lazy rules) into our model transformation language DSLTrans. As we handle only the declarative portion of ATL, and DSLTrans is Turing-incomplete, this reduction in expressivity allows us to use a symbolic-execution approach to generate representations of all possible input models to the transformation. We then verify pre-/post-condition contracts on these representations, which in turn verifies the transformation itself. The technique we present in this paper is exhaustive for the subset of declarative ATL model transformations. This means that if the prover indicates a contract holds on a transformation, then the contract’s pre-/post-condition pair will be true for any input model for that transformation. We demonstrate and explore the applicability of our technique by studying several relatively large and complex ATL model transformations, including a model transformation developed in collaboration with our industrial partner. As well, we present our ‘slicing’ technique. This technique selects only those rules in the DSLTrans transformation needed for contract proof, thereby reducing proving time. [ABSTRACT FROM AUTHOR]

Providing efficient theorem proving support for general ASM rules that update proper functions, use sequential and parallel composition, nondeterministic choice and recursion is difficult, since it is not easy to find a predicate logic formula that describes the transition relation of an ASM rule. One important obstacle to achieving this goal is that executing rules may result in a clash, that aborts the ASM run. This paper contributes three results towards this goal. First, it shows that it is possible to compute a first-order formula for each rule that implies clash-freedom when provable. The derived formula is not a precise characterization, but is provable for many ASMs that are used in practice. Second, we give axioms that describe the transition relation for clash-free ASM rules as formulas of predicate logic that can be used to verify pre/post-condition assertions using automated theorem provers. Third, we show that the relational encoding can be used to justify a calculus for clash-free ASM rules based on symbolic execution. Such a calculus is useful for interactive theorem provers such as our tool KIV. [ABSTRACT FROM AUTHOR]

In the process of safety testing in large-scale programs, Concolic tests often faced problems such as path explosion and lack of constraint solving ability. In order to alleviate these problems, this paper proposed a directed Concolic testing method for source code. Aiming at the danger code area prone to produce defects, the paths which could reach the critical code areas and the essential symbolic variables could be inferred based on backtracking control-flow and data-flow analysis. These information limited the dynamic testing only to cover the danger code area. The empirical results show that by ignoring a-nalysis of the unconcerned paths and symbolic variables, The method significantly improves the test efficiency and the provability of finding defects. [ABSTRACT FROM AUTHOR]

Concolic testing is a software testing technique that simultaneously combines concrete execution of a program (given specific input, along specific paths) with symbolic execution (generating new test inputs that explore other paths, which gives better path coverage than random test case generation). So far, concolic testing has been applied, mainly at the level of bytecode or assembly code, to programs written in imperative languages that manipulate primitive data types such as integers and arrays. In this article, we demonstrate its application to a functional programming language core, the functional subset of Core Erlang, that supports pattern matching, structured recursive data types such as lists, recursion and higher-order functions. We present CutEr, a tool implementing this testing technique, and describe its architecture, the challenges that it needs to address, its current limitations, and report some experiences from its use. [ABSTRACT FROM AUTHOR]

Interpolation has been successfully applied in formal methods for model checking and test-case generation for sequential programs. Security protocols, however, exhibit idiosyncrasies that make them unsuitable for the direct application of interpolation. We address this problem and present an interpolation-based method for security protocol verification. Our method starts from a protocol specification and combines Craig interpolation, symbolic execution and the standard Dolev-Yao intruder model to search for possible attacks on the protocol. Interpolants are generated as a response to search failure in order to prune possible useless traces and speed up the exploration. We illustrate our method by means of concrete examples and discuss the results obtained by using a prototype implementation. [ABSTRACT FROM AUTHOR]

We propose a language-independent symbolic execution framework. The approach is parameterised by a language definition, which consists of a signature for the syntax and execution infrastructure of the language, a model interpreting the signature, and rewrite rules for the language's operational semantics. Then, symbolic execution amounts to computing symbolic paths using a derivative operation. We prove that the symbolic execution thus defined has the properties naturally expected from it, meaning that the feasible symbolic executions of a program and the concrete executions of the same program mutually simulate each other. We also show how a coinduction-based extension of symbolic execution can be used for the deductive verification of programs. We show how the proposed symbolic-execution approach, and the coinductive verification technique based on it, can be seamlessly implemented in language definition frameworks based on rewriting such as the K framework. A prototype implementation of our approach has been developed in K . We illustrate it on the symbolic analysis and deductive verification of nontrivial programs. [ABSTRACT FROM AUTHOR]

Device drivers constitute an important part o£ an operation system (OS). The reliability of device drivers is critical to the security and reliability of OSs. We propose a property guided symbolic execution based framework for the bug detection of Linux device drivers. To analyze multiple properties simultaneously, we propose a multiple properties guided symbolic execution method. Based on the LLVM and KLEE，the framework and the property guided method are implemented. The results of the preliminary experiments on real world Linux drivers demonstrate the effectiveness and efficiency of the proposal. [ABSTRACT FROM AUTHOR]

The use of formal models to describe early versions of the structure and the behavior of a system has become common practice in industry. UML and OCL are the de-facto specification languages for these tasks. They allow for capturing system properties and module behavior in an abstract but still formal fashion. At the same time, this enables designers to detect errors or inconsistencies in the initial phases of the design flow—even if the implementation has not already started. Corresponding tools for verification of formal models got established in the recent past. However, verification results are usually not reused in later design steps anymore. In fact, similar verification tasks are applied again, e.g., after the implementation has been completed. This is a waste of computational and human effort. In this paper, we address this problem by proposing a method which checks a given implementation of a system against its corresponding formal method. This allows for transferring verification results already obtained from the formal model to the implementation and, eventually, motivates a new design flow which addresses verification across abstraction levels. This paper describes the applied techniques as well as their orchestration. Afterwards, the applicability of the proposed methodology is demonstrated by means of examples as well as a case study from an industrial context. [ABSTRACT FROM AUTHOR]

We present Crowbar, a deductive verification tool for the Active Object language ABS. Crowbar implements novel specification approaches specifically for distributed systems. For user interaction, counterexamples are presented as executable programs. Crowbar has a modular structure to explore further approaches, and was applied in the largest Active Objects verification study. [ABSTRACT FROM AUTHOR]

Software plagiarism, an act of illegally copying others’ code, has become a serious concern for honest software companies and the open source community. Considerable research efforts have been dedicated to searching the evidence of software plagiarism. In this paper, we continue this line of research and propose LoPD, a deviation-based program equivalence checking approach, which is an ideal fit for the whole-program plagiarism detection. Instead of directly comparing the similarity between two programs, LoPD searches for any dissimilarity between two programs by finding an input that will cause these two programs to behave differently, either with different output states or with semantically different execution paths. As long as we can find one dissimilarity, the programs are semantically different; but if we cannot find any dissimilarity, it is more likely a plagiarism case. We leverage dynamic symbolic execution to capture the semantics of execution paths and to find path deviations. Compared to the existing detection approaches, LoPD's formal program semantics-based method is more resilient to automatic obfuscation schemes. Our evaluation results indicate that LoPD is effective in detecting whole-program plagiarism. Furthermore, we demonstrate that LoPD can be applied to partial software plagiarism detection as well. The encouraging experiment results show that LoPD is an appealing complement to existing software plagiarism detection approaches. [ABSTRACT FROM PUBLISHER]

Existing static deadlock detectors suffer from either lack of precise interprocedural path- and context-sensitive analysis or lack of scalability. In addition, they only take a few of synchronous events into account and suffer from the lack of a united method to handle different synchronization events. To address these problems, we first present a static interprocedural analysis algorithm, named mixed procedure inlining and summary-based analysis (MPISBA), to produce feasible execution traces in C/C++ programs. The functions which call function pointers or virtual functions are considered as inlining functions to figure out callees in different context. Path-sensitive symbolic execution is also used by MPISBA to track synchronization events in different program paths guarded by path conditions. In order to do interprocedural context-sensitive analysis and avoid function re-analysis, the proposed algorithm generates a summary for each function and applies the summary at the function's call sites. Based on feasible execution traces in program, a translation algorithm called generic synchronization event translation is proposed to translate different synchronization events into unified Petri nets. A prototype detector named MagicDetector is implemented for these procedures. A suite of open-source and large-scale softwares are used to validate MagicDetector, and comparisons are made among JDAE, Magiclock, DADCP and MagicDetector. Experimental results demonstrate that MagicDetector scales well to programs with 2M lines of codes and is more precise than previous detectors, finding more real deadlocks and reporting less false positives. [ABSTRACT FROM AUTHOR]

Studies have shown that driver vulnerability is one of the main causes of Linux security issues ，which can lead to privilege escalation，denial of service and other high-risk situations. Considering the difficulty of driver vulnerability detection without real devices，this paper proposes symbolic execution of Linux drivers and implements the symbolic device driver environment (SDDE ) which can detect bugs in Linux device driver. The SDDE provides symbolic kernel services and symbolic devices, making symbolic execution of Linux driver and runtime driver vulnerability detection possible. The SDDE works without real hardware, and has high coverage, high performance and good scalability. The SDDE is applied to 6 Linux drivers，and we found six real bugs，three of which are confirmed by Linux developers. [ABSTRACT FROM AUTHOR]

We propose a language-independent symbolic execution framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language definition is generated, with the same syntax as the original one, but whose semantical rules are transformed in order to rewrite over logical formulas denoting possibly infinite sets of program states. Then, the symbolic execution of concrete programs is, by definition, the execution of the same programs with the symbolic semantics. We prove that the symbolic execution thus defined has the properties naturally expected from it (with respect to concrete program execution). A prototype implementation of our approach was developed in the K framework. We demonstrate the tool׳s genericity by instantiating it on several languages, and illustrate it on the reachability analysis and model checking of several programs. [ABSTRACT FROM AUTHOR]

Security protocols are notoriously difficult to get right, and most go through several iterations before their hidden security vulnerabilities, which are hard to detect, are triggered. To help protocol designers and developers efficiently find non-trivial bugs, we introduce SYMCONF, a practical conformance testing tool that generates high-coverage test input packets using a conformance test suite and symbolic execution. Our approach can be viewed as the combination of conformance testing and symbolic execution: 1) it first selects symbolic inputs from an existing conformance test suite; 2) it then symbolically executes a network protocol implementation with the symbolic inputs; and 3) it finally generates high-coverage test input packets using a conformance test suite. We demonstrate the feasibility of this methodology by applying SYMCONF to the generation of a stream of high quality test input packets for multiple implementations of two network protocols, the Kerberos Telnet protocol and Dynamic Host Configuration Protocol (DHCP), and discovering non-trivial security bugs in the protocols. [ABSTRACT FROM AUTHOR]

Symbolic execution is a technique enabling the automatic generation of test inputs that exercise a set of execution paths within a code unit to be tested. If the paths cover a sufficient part of the code under test, the test data offer a representative view of the actual behaviour of this code. This notably enables detecting errors and correcting faults. Relational databases are ubiquitous in software, but symbolic execution of code units that manipulate them remains a non-trivial problem, particularly because of the complex structure of such databases and the complex behaviour of SQL statements. Finding errors in such code units is yet critical, as it can avoid corrupting important data. In this work, we define a symbolic execution translating database manipulation code directly into constraints and integrate it with a more traditional symbolic execution of normal program code. The database tables are represented by relational symbols and the SQL statements by relational constraints over these symbols. An algorithm based on these principles is presented for the symbolic execution of simple Java methods that implement transactional use cases by reading and writing in a relational database, the latter subject to data integrity constraints. The algorithm is integrated in a test generation tool and experimented over sample code. The target language for the constraints produced by the tool is the SMT-Lib standard and the used solver is Microsoft Z3. The results show that the proposed approach enables generating meaningful test data, including valid database content, in reasonable time. In particular, the Z3 solver is shown to be more scalable than the Alloy solver, used in our previous work, for solving relational constraints. [ABSTRACT FROM AUTHOR]

It has been proved that Linux driver bugs are the major bug source of the whole system, which can lead to serious security problems. A tool called symbolic driver environment (SDE) is designed to detect Linux driver bugs, which consists of the system model, the interactions between driver and kernel, and the interactions between driver and device. Using SDE, we detect two real Linux drivers, and find Two bugs. The results prove that the tool is feasible, and the speed is 90% faster and the coverage is 20% larger compared with an existing tool called SymDrive. [ABSTRACT FROM AUTHOR]

Data races are one of the main causes of concurrency problems in multithreaded programs.Whether all data races are bad, or some are harmful and others are harmless, is still the subject of vigorous scientific debate [Narayanasamy et al. 2007; Boehm 2012]. What is clear, however, is that today's code has many data races [Kasikci et al. 2012; Jin et al. 2012; Erickson et al. 2010], and fixing data races without introducing bugs is time consuming [Godefroid and Nagappan 2008]. Therefore, it is important to efficiently identify data races in code and understand their consequences to prioritize their resolution. We present Portend+, a tool that not only detects races but also automatically classifies them based on their potential consequences: Could they lead to crashes or hangs? Could their effects be visible outside the program? Do they appear to be harmless? How do their effects change under weak memory models? Our proposed technique achieves high accuracy by efficiently analyzing multiple paths and multiple thread schedules in combination, and by performing symbolic comparison between program outputs. We ran Portend+ on seven real-world applications: it detected 93 true data races and correctly classified 92 of them, with no human effort. Six of them were harmful races. Portend+'s classification accuracy is up to 89% higher than that of existing tools, and it produces easy-to-understand evidence of the consequences of "harmful" races, thus both proving their harmfulness and making debugging easier. We envision Portend+ being used for testing and debugging, as well as for automatically triaging bug reports. [ABSTRACT FROM AUTHOR]

Software crash reproduction is the necessary first step for debugging. Unfortunately, crash reproduction is often labor intensive. To automate crash reproduction, many techniques have been proposed including record-replay and post-failure-process approaches. Record-replay approaches can reliably replay recorded crashes, but they incur substantial performance overhead to program executions. Alternatively, post-failure-process approaches analyse crashes only after they have occurred. Therefore they do not incur performance overhead. However, existing post-failure-process approaches still cannot reproduce many crashes in practice because of scalability issues and the object creation challenge. This paper proposes an automatic crash reproduction framework using collected crash stack traces. The proposed approach combines an efficient backward symbolic execution and a novel method sequence composition approach to generate unit test cases that can reproduce the original crashes without incurring additional runtime overhead. Our evaluation study shows that our approach successfully exploited 31 (59.6 percent) of 52 crashes in three open source projects. Among these exploitable crashes, 22 (42.3 percent) are useful reproductions of the original crashes that reveal the crash triggering bugs. A comparison study also demonstrates that our approach can effectively outperform existing crash reproduction approaches. [ABSTRACT FROM PUBLISHER]

We present a symbolic execution-based technique for cross-checking programs accelerated using SIMD or OpenCL against an unaccelerated version, as well as a technique for detecting data races in OpenCL programs. Our techniques are implemented in KLEE-CL, a tool based on the symbolic execution engine KLEE that supports symbolic reasoning on the equivalence between expressions involving both integer and floating-point operations. While the current generation of constraint solvers provide effective support for integer arithmetic, the situation is different for floating-point arithmetic, due to the complexity inherent in such computations. The key insight behind our approach is that floating-point values are only reliably equal if they are essentially built by the same operations. This allows us to use an algorithm based on symbolic expression matching augmented with canonicalisation rules to determine path equivalence. Under symbolic execution, we have to verify equivalence along every feasible control-flow path. We reduce the branching factor of this process by aggressively merging conditionals, if-converting branches into select operations via an aggressive phi-node folding transformation. To support the Intel Streaming SIMD Extension (SSE) instruction set, we lower SSE instructions to equivalent generic vector operations, which in turn are interpreted in terms of primitive integer and floating-point operations. To support OpenCL programs, we symbolically model the OpenCL environment using an OpenCL runtime library targeted to symbolic execution. We detect data races by keeping track of all memory accesses using a memory log, and reporting a race whenever we detect that two accesses conflict. By representing the memory log symbolically, we are also able to detect races associated with symbolically-indexed accesses of memory objects. We used KLEE-CL to prove the bounded equivalence between scalar and data-parallel versions of floating-point programs and find a number of issues in a variety of open source projects that use SSE and OpenCL, including mismatches between implementations, memory errors, race conditions and a compiler bug. [ABSTRACT FROM PUBLISHER]

The objective of this paper is to present the symbolic execution of programs and its extension, generalized symbolic execution, to indicate the necessary improvements to symbolic execution so that it becomes a practical approach for program verification. Program analysis allows determining levels of software correctness or compliance with the user requirements. There are two approaches for program verification, analytic and dynamic, and, between them, symbolic execution exits which statically analyzes the program source code, and dynamically simulates the execution of executable instructions of programs by means of symbolic input data. In this paper, concepts of program verification, the original proposal of symbolic execution along with their advantages and disadvantages, and the main features of generalized symbolic execution are described. Finally, the main open research areas related to symbolic execution are summarized. [ABSTRACT FROM AUTHOR]

This paper presents a new method, capable of automatically generating attacks on binary programs from software crashes. We analyze software crashes with a symbolic failure model by performing concolic executions following the failure directed paths, using a whole system environment model and concrete address mapped symbolic memory in S^2 E. We propose a new selective symbolic input method and lazy evaluation on pseudo symbolic variables to handle symbolic pointers and speed up the process. This is an end-to-end approach able to create exploits from crash inputs or existing exploits for various applications, including most of the existing benchmark programs, and several large scale applications, such as a word processor (Microsoft office word), a media player (mpalyer), an archiver (unrar), or a pdf reader (foxit). We can deal with vulnerability types including stack and heap overflows, format string, and the use of uninitialized variables. Notably, these applications have become software fuzz testing targets, but still require a manual process with security knowledge to produce mitigation-hardened exploits. Using this method to generate exploits is an automated process for software failures without source code. The proposed method is simpler, more general, faster, and can be scaled to larger programs than existing systems. We produce the exploits within one minute for most of the benchmark programs, including mplayer. We also transform existing exploits of Microsoft office word into new exploits within four minutes. The best speedup is 7,211 times faster than the initial attempt. For heap overflow vulnerability, we can automatically exploit the unlink() macro of glibc, which formerly requires sophisticated hacking efforts. [ABSTRACT FROM PUBLISHER]

Classical symbolic execution in software testing has difficulty in environment interaction. To address the problem, this paper proposed symbolic execution with mixed concrete-symbolic input. Firstly it defined the consistency model of program execution to analyze systematically approximation between symbolic execution and concrete execution. Secondly it put forward the method for switching back and forth between symbolic execution and concrete execution and the heuristic strategy of maintaining consistency. Finally, by distinguishing solvable constraint from complex constraint and using concrete and symbolic values to simplify complex constraint, it designed and realized mixed path constraint solution algorithm. The experiment represents the feasibility and effectiveness of the method in the processing environment interaction. As well as, the method is able to improve classical symbolic execution. [ABSTRACT FROM AUTHOR]

Modern web applications often suffer from command injection attacks. Even when equipped with sanitization code, many systems can be penetrated due to software bugs. It is desirable to automatically discover such vulnerabilities, given the bytecode of a web application. One approach would be symbolically executing the target system and constructing constraints for matching path conditions and attack patterns. Solving these constraints yields an attack signature, based on which, the attack process can be replayed. Constraint solving is the key to symbolic execution. For web applications, string constraints receive most of the attention because web applications are essentially text processing programs. We present simple linear string equation (SISE), a decidable fragment of the general string constraint system. SISE models a collection of regular replacement operations (such as the greedy, reluctant, declarative, and finite replacement), which are frequently used by text processing programs. Various automata techniques are proposed for simulating procedural semantics such as left-most matching. By composing atomic transducers of a SISE, we show that a recursive algorithm can be used to compute the solution pool, which contains the value range of each variable in concrete solutions. Then a concrete variable solution can be synthesized from a solution pool. To accelerate solver performance, a symbolic representation of finite state transducer is developed. This allows the constraint solver to support a 16-bit Unicode alphabet in practice. The algorithm is implemented in a Java constraint solver called SUSHI. We compare the applicability and performance of SUSHI with Kaluza, a bounded string solver. [ABSTRACT FROM AUTHOR]