We propose a symbolic execution method for programs that can draw random samples. In contrast to existing work, our method can verify randomized programs with unknown inputs and can prove probabilistic properties that universally quantify over all possible inputs. Our technique augments standard symbolic execution with a new class of \emph{probabilistic symbolic variables}, which represent the results of random draws, and computes symbolic expressions representing the probability of taking individual paths. We implement our method on top of the \textsc{KLEE} symbolic execution engine alongside multiple optimizations and use it to prove properties about probabilities and expected values for a range of challenging case studies written in C++, including Freivalds' algorithm, randomized quicksort, and a randomized property-testing algorithm for monotonicity. We evaluate our method against \textsc{Psi}, an exact probabilistic symbolic inference engine, and \textsc{Storm}, a probabilistic model checker, and show that our method significantly outperforms both tools.
Symbolic execution is a powerful technique for program analysis. However, it has many limitations in practical applicability: the path explosion problem encumbers scalability, the need for language-specific implementation, the inability to handle complex dependencies, and the limited expressiveness of theories supported by underlying satisfiability checkers. Often, relationships between variables of interest are not expressible directly as purely symbolic constraints. To this end, we present a new approach -- neuro-symbolic execution -- which learns an approximation of the relationship as a ne…
We present a generalisation of King's symbolic execution technique called compact symbolic execution. It proceeds in two steps. First, we analyse cyclic paths in the control flow graph of a given program, independently from the rest of the program. Our goal is to compute a so called template for each such a cyclic path. A template is a declarative parametric description of all possible program states, which may leave the analysed cyclic path after any number of iterations along it. In the second step, we execute the program symbolically with the templates in hand. The result is a compact symbo…
We present an automatic analysis technique for checking data races on OpenCL kernels. Our method defines symbolic execution techniques based on separation logic with suitable abstractions to automatically detect non-benign racy behaviours on kernel
Symbolic execution is a classical program analysis technique used to show that programs satisfy or violate given specifications. In this work we generalize symbolic execution to support program analysis for relational specifications in the form of relational properties - these are properties about two runs of two programs on related inputs, or about two executions of a single program on related inputs. Relational properties are useful to formalize notions in security and privacy, and to reason about program optimizations. We design a relational symbolic execution engine, named RelSym which sup…
We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external behaviour. We prove the symbolic semantics to be sound and complete. This yields a bounded technique by imposing bounds on the depth of recursion and callbacks. We provide an implementation of our te…
We introduce a novel technique for finding real errors in programs. The technique is based on a synergy of three well-known methods: metacompilation, slicing, and symbolic execution. More precisely, we instrument a given program with a code that tracks runs of state machines representing various kinds of errors. Next we slice the program to reduce its size without affecting runs of state machines. And then we symbolically execute the sliced program. Depending on the kind of symbolic execution, the technique can be applied as a stand-alone bug finding technique, or to weed out some false positi…
Message passing is the standard paradigm of programming in high-performance computing. However, verifying Message Passing Interface (MPI) programs is challenging, due to the complex program features (such as non-determinism and non-blocking operations). In this work, we present MPI symbolic verifier (MPI-SV), the first symbolic execution based tool for automatically verifying MPI programs with non-blocking operations. MPI-SV combines symbolic execution and model checking in a synergistic way to tackle the challenges in MPI program verification. The synergy improves the scalability and enlarges…
Symbolic execution has always been plagued by the inability to handle programs that require highly structured inputs. Most often, the symbolic execution engine gets overwhelmed by the sheer number of infeasible paths and fails to explore enough feasible paths to gain any respectable coverage. In this paper, we propose a system, InVaSion, that attempts to solve this problem for forking-based symbolic execution engines. We propose an input specification language (ISL) that is based on a finite-state automaton but includes guarded transitions, a set of registers and a set of commands to update th…
We present a new approach to automated reasoning about higher-order programs by extending symbolic execution to use behavioral contracts as symbolic values, enabling symbolic approximation of higher-order behavior. Our approach is based on the idea of an abstract reduction semantics that gives an operational semantics to programs with both concrete and symbolic components. Symbolic components are approximated by their contract and our semantics gives an operational interpretation of contracts-as-values. The result is a executable semantics that soundly predicts program behavior, including cont…
Symbolic execution is a successful and very popular technique used in software verification and testing. A key limitation of symbolic execution is in dealing with code containing loops. The problem is that even a single loop can generate a huge number of different symbolic execution paths, corresponding to different number of loop iterations and taking various paths through the loop. We introduce a technique which, given a start location above some loops and a target location anywhere below these loops, returns a feasible path between these two locations, if such a path exists. The technique i…
Symbolic execution is a program analysis technique commonly utilized to determine whether programs violate properties and, in case violations are found, to generate inputs that can trigger them. Used in the context of security properties such as noninterference, symbolic execution is precise when looking for counterexample pairs of traces when insecure information flows are found, however it is sound only up to a bound thus it does not allow to prove the correctness of programs with executions beyond the given bound. By contrast, abstract interpretation-based static analysis guarantees soundne…
We present a new approach to automated reasoning about higher-order programs by endowing symbolic execution with a notion of higher-order, symbolic values. Our approach is sound and relatively complete with respect to a first-order solver for base type values. Therefore, it can form the basis of automated verification and bug-finding tools for higher-order programs. To validate our approach, we use it to develop and evaluate a system for verifying and refuting behavioral software contracts of components in a functional language, which we call soft contract verification. In doing so, we discove…
Existing support for regular expressions in automated test generation or verification tools is lacking. Common aspects of regular expression engines found in mainstream programming languages, such as backreferences or greedy matching, are commonly ignored or imprecisely approximated, leading to poor test coverage or failed proofs. In this paper, we present the first complete strategy to faithfully reason about regular expressions in the context of symbolic execution, focusing on the operators found in JavaScript. We model regular expression operations using string constraints and classical reg…
Seoul National University（首尔大学）；FriendliAI；Samsung Research（三星研究院）；University of California, Berkeley（加州大学伯克利分校）
Imperative programming allows users to implement their deep neural networks (DNNs) easily and has become an essential part of recent deep learning (DL) frameworks. Recently, several systems have been proposed to combine the usability of imperative programming with the optimized performance of symbolic graph execution. Such systems convert imperative Python DL programs to optimized symbolic graphs and execute them. However, they cannot fully support the usability of imperative programming. For example, if an imperative DL program contains a Python feature with no corresponding symbolic represen…
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 …
In previous work, we presented a symbolic execution method which starts with a concrete model of the program but progressively abstracts away details only when these are known to be irrelevant using interpolation. In this paper, we extend the technique to handle unbounded loops. The central idea is to progressively discover the strongest invariants through a process of loop unrolling. The key feature of this technique, called the minimax algorithm, is intelligent backtracking which directs the search for the next invariant. We then present an analysis of the main differences between our symbol…
In this thesis, we introduce the idea of combining symbolic execution with dynamic analysis for reverse engineering. Differently from DSE, we devise an approach where the reverse engineer can use a debugger to drive and inspect a concrete execution engine of the application code and then, when needed, transfer the execution into a symbolic executor in order to automatically identify the input values required to reach a target point in the code. After that, the user can also transfer back the correct input values found with symbolic execution in order to continue the debugging. The synchronizat…
Differential privacy is a de facto standard in data privacy with applications in the private and public sectors. Most of the techniques that achieve differential privacy are based on a judicious use of randomness. However, reasoning about randomized programs is difficult and error prone. For this reason, several techniques have been recently proposed to support designer in proving programs differentially private or in finding violations to it. In this work we propose a technique based on symbolic execution for reasoning about differential privacy. Symbolic execution is a classic technique used…
We present Gillian, a language-independent framework for the development of compositional symbolic analysis tools. Gillian supports three flavours of analysis: whole-program symbolic testing, full verification, and bi-abduction. It comes with fully parametric meta-theoretical results and a modular implementation, designed to minimise the instantiation effort required of the user. We evaluate Gillian by instantiating it to JavaScript and C, and perform its analyses on a set of data-structure libraries, obtaining results that indicate that Gillian is robust enough to reason about real-world prog…
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…
Dynamically typed languages, like Erlang, allow developers to quickly write programs without explicitly providing any type information on expressions or function definitions. However, this feature makes those languages less reliable than statically typed languages, where many runtime errors can be detected at compile time. In this paper, we present a preliminary work on a tool that, by using the well-known techniques of metaprogramming and symbolic execution, can be used to perform bounded verification of Erlang programs. In particular, by using Constraint Logic Programming, we develop an inte…
Parametric Worst-case execution time (WCET) analysis of a sequential program produces a formula that represents the worst-case execution time of the program, where parameters of the formula are user-defined parameters of the program (as loop bounds, values of inputs or internal variables, etc). In this paper we propose a novel methodology to compute the parametric WCET of a program. Unlike other algorithms in the literature, our method is not based on Integer Linear Programming (ILP). Instead, we follow an approach based on the notion of symbolic computation of WCET formulae. After explaining …
In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to recursive predicates, iterated separating conjunctions do not prescribe a structure on the locations they range over, and so do not restrict how to traverse and modify these locations. This flexibility is important for the verification of random-access data structures such as arrays and data structures that can be traversed in multiple ways such as graphs. Despite its usefulness, no automatic program verifier nativel…
We study the problem of learning worst-case-safe parameters for programs that use neural networks as well as symbolic, human-written code. Such neurosymbolic programs arise in many safety-critical domains. However, because they can use nondifferentiable operations, it is hard to learn their parameters using existing gradient-based approaches to safe learning. Our approach to this problem, Differentiable Symbolic Execution (DSE), samples control flow paths in a program, symbolically constructs worst-case "safety losses" along these paths, and backpropagates the gradients of these losses through…
Fuzzy logic programming is a growing declarative paradigm aiming to integrate fuzzy logic into logic programming. One of the most difficult tasks when specifying a fuzzy logic program is determining the right weights for each rule, as well as the most appropriate fuzzy connectives and operators. In this paper, we introduce a symbolic extension of fuzzy logic programs in which some of these parameters can be left unknown, so that the user can easily see the impact of their possible values. Furthermore, given a number of test cases, the most appropriate values for these parameters can be automat…
The rapid evolution of deep neural networks is demanding deep learning (DL) frameworks not only to satisfy the requirement of quickly executing large computations, but also to support straightforward programming models for quickly implementing and experimenting with complex network structures. However, existing frameworks fail to excel in both departments simultaneously, leading to diverged efforts for optimizing performance and improving usability. This paper presents JANUS, a system that combines the advantages from both sides by transparently converting an imperative DL program written in P…
University of California Los Angeles（加利福尼亚大学洛杉矶分校）；University of Southern California（南加利福尼亚大学）；Portland State University（波特兰州立大学）
As the number of deep learning frameworks increase and certain ones gain popularity, it spurs the discussion of what methodologies are employed by these frameworks and the reasoning behind them. The goal of this survey is to study how symbolic techniques are utilized in deep learning. To do this, we look at some of the most popular deep learning frameworks being used today, including TensorFlow, Keras, PyTorch, and MXNet. While these frameworks greatly differ from one another, many of them use symbolic techniques, whether it be symbolic execution, graphs, or programming. We focus this paper on…
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…
Message Passing Interfaces (MPI) plays an important role in parallel computing. Many parallel applications are implemented as MPI programs. The existing methods of bug detection for MPI programs have the shortage of providing both input and non-determinism coverage, leading to missed bugs. In this paper, we employ symbolic execution to ensure the input coverage, and propose an on-the-fly schedule algorithm to reduce the interleaving explorations for non-determinism coverage, while ensuring the soundness and completeness. We have implemented our approach as a tool, called MPISE, which can autom…
The timing characteristics of cache, a high-speed storage between the fast CPU and the slowmemory, may reveal sensitive information of a program, thus allowing an adversary to conduct side-channel attacks. Existing methods for detecting timing leaks either ignore cache all together or focus only on passive leaks generated by the program itself, without considering leaks that are made possible by concurrently running some other threads. In this work, we show that timing-leak-freedom is not a compositional property: a program that is not leaky when running alone may become leaky when interleaved…
In this work, we propose an automated method to identify semantic bugs in student programs, called ATAS, which builds upon the recent advances in both symbolic execution and active learning. Symbolic execution is a program analysis technique which can generate test cases through symbolic constraint solving. Our method makes use of a reference implementation of the task as its sole input. We compare our method with a symbolic execution-based baseline on 6 programming tasks retrieved from CodeForces comprising a total of 23K student submissions. We show an average improvement of over 2.5x over t…
We propose an automated technique for 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 K framework, we enrich the symbolic execution facilities recently provided by K with novel capabilities for assertion synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that explains the execution of a (modifier) C function by using other (observer) routines in the same program…
