{ "cells": [ { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": false, "run_control": { "read_only": false }, "slideshow": { "slide_type": "slide" } }, "source": [ "# Symbolic Fuzzing\n", "\n", "One of the problems with traditional methods of fuzzing is that they fail to penetrate deeply into the program. Quite often the execution of a specific branch of execution may happen only with very specific inputs, which could represent an extremely small fraction of the input space. The traditional fuzzing methods relies on chance to produce inputs they need. However, relying on randomness to generate values that we want is a bad idea when the space to be explored is huge. For example, a function that accepts a string, even if one only considers the first $10$ characters, already has $2^{80}$ possible inputs. If one is looking for a specific string, random generation of values will take a few thousand years even in one of the super computers.\n", "\n", "Symbolic execution is a way out of this problem. A program is a computation that can be treated as a system of equations that obtains the output values from the given inputs. Executing the program symbolically -- that is, solving these mathematically -- along with any specified objective such as covering a particular branch or obtaining a particular output will get us inputs that can accomplish this task. Unfortunately, symbolic execution can rapidly become unwieldy as the paths through the program increases. A practical alternative is called *Concolic* execution, which combines symbolic and concrete execution, with concrete execution guiding symbolic execution through a path through the program.\n", "\n", "In this chapter, we investigate how **concolic execution** can be implemented, and how it can be used to obtain interesting values for fuzzing." ] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": false, "run_control": { "read_only": false }, "slideshow": { "slide_type": "subslide" } }, "source": [ "**Prerequisites**\n", "\n", "* You should have read the [chapter on coverage](Coverage.ipynb).\n", "* Some knowledge of inheritance in Python is required.\n", "* A familiarity with the [chapter on search based fuzzing](SearchBasedFuzzer.ipynb) would be useful.\n", "* A familiarity with the basic idea of [SMT solvers](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) would be useful." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Using symbolic variables to obtain path conditions for coverage" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "In the chapter on [parsing and recombining inputs](SearchBasedFuzzer.ipynb), we saw how difficult it was to generate inputs for `process_vehicle()` -- a simple function that accepts a string. The solution given there was to rely on preexisting sample inputs. However, this solution is inadequate as it assumes the existence of sample inputs. What if there are no sample inputs at hand?\n", "\n", "For a simpler example, let us consider the following function. Can we generate inputs to cover all the paths?" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def check_triangle(a, b, c):\n", " if a == b:\n", " if a == c:\n", " if b == c:\n", " return \"Equilateral\"\n", " else:\n", " return \"Isosceles\"\n", " else:\n", " return \"Isosceles\"\n", " else:\n", " if b != c:\n", " if a == c:\n", " return \"Isosceles\"\n", " else:\n", " return \"Scalene\"\n", " else:\n", " return \"Isosceles\"" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### The control flow graph" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The control flow graph of this function can be represented as follows:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "import fuzzingbook_utils" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "from ControlFlow import PyCFG, CFGNode, to_graph, gen_cfg" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "import inspect" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "from graphviz import Source, Graph" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "Source(to_graph(gen_cfg(inspect.getsource(check_triangle))))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The possible execution paths traced by the program can be represented as follows, with the numbers indicating the specific line numbers executed." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "paths = {\n", " '': ([1, 2, 3, 4, 5], 'Equilateral'),\n", " '': ([1, 2, 3, 4, 7], 'Isosceles'),\n", " '': ([1, 2, 3, 9], 'Isosceles'),\n", " '': ([1, 2, 11, 12, 13], 'Isosceles'),\n", " '': ([1, 2, 11, 12, 15], 'Scalene'),\n", " '': ([1, 2, 11, 17], 'Isosceles'),\n", "}" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Consider the ``. To trace this path, we need to execute the following statements in order." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "```python\n", "1: check_triangle(a, b, c)\n", "2: if (a == b) -> True\n", "3: if (a == c) -> True\n", "4: if (b == c) -> True\n", "5: return 'Equilateral'\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "That is, any execution that traces this path has to start with values for `a`, `b`, and `c` that obeys the constraints in line numbers `2: (a == b)` evaluates to `True`, `3: (a == c)` evaluates to `True`, and `4: (b == c)` evaluates to `True`. Can we generate inputs such that these constraints are satisfied?" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "One of the ways to solve such constraints is to use an [SMT solver](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories) such as [z3](http://theory.stanford.edu/~nikolaj/programmingz3.html). Here is how one would go about solving the set of equations using *z3*." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "import z3" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "First, we declare a set of variables as symbolic integers using *z3*.\n", "\n", "*A symbolic variable can be thought of as a sort of placeholder for the real variable, sort of like the `x` in solving for `x` in Algebra. We identify what conditions the variable is supposed to obey, and finally produce a value that obeys all*" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "a, b, c = z3.Int('a'), z3.Int('b'), z3.Int('c')" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We can now ask *z3* to solve the set of equations for us as follows." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "z3.solve(a == b, a == c, b == c)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Here we find the first problem in our program. Our program seems to not check whether the sides are greater than zero. Assume for now that we do not have that restriction. Does our program correctly follow the path described?\n", "\n", "We can use the `Coverage` from the [chapter on coverage](Coverage.ipynb) as a tracer to visualize that information as below." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "from Coverage import Coverage" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We modify the tracer to report *all* traced events." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class Tracer(Coverage):\n", " def traceit(self, frame, event, args):\n", " if event != 'return':\n", " f = inspect.getframeinfo(frame)\n", " self._trace.append((f.function, f.lineno))\n", " return self.traceit" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "First, we recover the trace." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " assert check_triangle(0, 0, 0) == 'Equilateral'\n", "cov._trace" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "To plot the path taken, we need to extract edges from the coverage.\n", "We define a procedure `cov_to_arcs()` to translate our coverage to a list of edges." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def cov_to_arcs(cov):\n", " t = [i for f, i in cov._trace]\n", " return list(zip(t, t[1:]))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "cov_to_arcs(cov)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We can now determine the path taken." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### The CFG with path taken" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "check_triangle_src = inspect.getsource(check_triangle).strip()" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "Source(to_graph(gen_cfg(check_triangle_src), arcs=cov_to_arcs(cov)))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "As you can see, the path taken is ``." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Similarly, for solving `` we need to simply invert the condition at :" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "a, b, c = z3.Ints('a b c')" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "z3.solve(a == b, a == c, z3.Not(b == c))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The symbolic execution suggests that there is no solution. A moment's reflection will convince us that it is indeed true. Let us proceed with the other paths. The `` can be obtained by inverting the condition at ``." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "a, b, c = z3.Ints('a b c')" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "z3.solve(a == b, z3.Not(a == c))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " assert check_triangle(1, 1, 0) == 'Isosceles'\n", "[i for fn, i in cov._trace if fn == 'check_triangle']" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "How about path <4>?" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "a, b, c = z3.Ints('a b c')" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "z3.solve(z3.Not(a == b), b != c, a == c)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "As we mentioned earlier, our program does not account for sides with zero or negative length. We can modify our program to check for zero and negative input. However, do we always have to make sure that every function has to account for all possible inputs? It is possible that the `check_triangle` is not directly exposed to the user, and it is called from another function that already guarantees that the inputs would be positive.\n", "\n", "We can easily add such a precondition here." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "pre_condition = z3.And(a > 0, b > 0, c > 0)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "z3.solve(pre_condition, z3.Not(a == b), b != c, a == c)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " assert check_triangle(1, 2, 1) == 'Isosceles'\n", "[i for fn, i in cov._trace if fn == 'check_triangle']" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "paths['']" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Continuing to path <5>:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "a, b, c = z3.Ints('a b c')" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "z3.solve(pre_condition, z3.Not(a == b), b != c, z3.Not(a == c))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "And indeed it is a *Scalene* triangle." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " assert check_triangle(3, 1, 2) == 'Scalene'\n", "[i for fn, i in cov._trace if fn == 'check_triangle']" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "paths['']" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Finally, for `` the procedure is similar." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "z3.solve(pre_condition, z3.Not(a == b), z3.Not(b != c))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " assert check_triangle(2, 1, 1) == 'Isosceles'\n", "[i for fn, i in cov._trace if fn == 'check_triangle']" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "paths['']" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "What if we wanted another solution? We can simply ask the solver to solve again, and not give us the same values." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "seen = [z3.And(a == 2, b == 1, c == 1)]" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "z3.solve(pre_condition, z3.Not(z3.Or(seen)), z3.Not(a == b), z3.Not(b != c))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "seen.append(z3.And(a == 1, b == 2, c == 2))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "z3.solve(pre_condition, z3.Not(z3.Or(seen)), z3.Not(a == b), z3.Not(b != c))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "That is, using simple symbolic computation, we were able to easily see that (1) some of the paths are not reachable, and (2) some of the conditions were insufficient -- we needed preconditions. What about the total coverage obtained?" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### Visualizing the coverage obtained" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Visualizing the statement coverage can be accomplished as below." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class Tracer(Tracer):\n", " def show_coverage(self, fn):\n", " src = fn if isinstance(fn, str) else inspect.getsource(fn)\n", " covered = set([lineno for method, lineno in self._trace])\n", " for i, s in enumerate(src.split('\\n')):\n", " print('%s %2d: %s' % ('#' if i + 1 in covered else ' ', i + 1, s))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We run all the inputs obtained under the coverage tracer." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " assert check_triangle(0, 0, 0) == 'Equilateral'\n", " assert check_triangle(1, 1, 0) == 'Isosceles'\n", " assert check_triangle(1, 2, 1) == 'Isosceles'\n", " assert check_triangle(3, 1, 2) == 'Scalene'\n", " assert check_triangle(2, 1, 1) == 'Isosceles'" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "cov.show_coverage(check_triangle)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "The coverage is as expected. The generated values does seem to cover all code that can be covered." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### Function summaries" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Now, consider this equation for determining absolute value." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def abs_value(x):\n", " if x < 0:\n", " v = -x\n", " else:\n", " v = x\n", " return v" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "Source(to_graph(gen_cfg(inspect.getsource(abs_value))))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "What can we say about the value of `v` at `line: 5`? Let us trace and see. First, we have variable `x` at `line: 1`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "x = z3.Int('x')" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "At `line: 2`, we face a bifurcation in the possible paths. Hence, we produce two paths with corresponding constraints." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "l2_F = x < 0\n", "l2_T = z3.Not(x < 0)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "For `line: 3`, we only need to consider the `If` path. However, we have an assignment. So we use a new variable here." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "v_0 = z3.Int('v_0')\n", "l3 = z3.And(l2_F, v_0 == -x)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Similarly, for `line: 5`, we have an assignment. (Can we reuse the variable `v_0` from before?)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "v_1 = z3.Int('v_1')\n", "l5 = z3.And(l2_T, v_1 == x)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "When we come to `line: 6`, we see that we have *two* input streams. We have a choice. We can either keep each path separate as we did previously." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "v = z3.Int('v')\n", "for s in [z3.And(l3, v == v_0), z3.And(l5, v == v_1)]:\n", " z3.solve(x != 0, s)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Or, we can combine them together and produce a single predicate at `line: 6`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "v = z3.Int('v')\n", "l6 = z3.Or(z3.And(l3, v == v_0), z3.And(l5, v == v_1))\n", "z3.solve(l6)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "**Note.** Mering two incoming streams of execution can be non-trivial, especially when the execution paths are traversed multiple times (E.g. loops and recursion). For those interested, lookup [inferring loop invariants](https://www.st.cs.uni-saarland.de/publications/details/galeotti-hvc-2014/)." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We can get this to produce any number of solutions for `abs()` as below." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "s = z3.Solver()\n", "s.add(l6)\n", "for i in range(5):\n", " if s.check() == z3.sat:\n", " m = s.model()\n", " x_val = m[x]\n", " print(m)\n", " else:\n", " print('no solution')\n", " break\n", " s.add(z3.Not(x == x_val))\n", "s" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "The solver is not particularly random. So we need to help it a bit to produce values on the negative range." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "s.add(x < 0)\n", "for i in range(5):\n", " if s.check() == z3.sat:\n", " m = s.model()\n", " x_val = m[x]\n", " print(m)\n", " else:\n", " print('no solution')\n", " break\n", " s.add(z3.Not(x == x_val))\n", "\n", "s" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "Note that the single expression produced at `line: 6` is essentially a summary for `abs_value()`. " ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "abs_value_summary = l6\n", "abs_value_summary" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The *z3* solver can be used to simplify the predicates where possible." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "z3.simplify(l6)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "One can use this summary rather than trace into `abs_value()` when `abs_value()` is used elsewhere. For that, we need to convert this summary into a form that is usable in other places." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "import ast\n", "import astunparse" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### prefix_vars\n", "The method `prefix_vars()` modifies the variables in an expression such that the variables are prefixed with a given value." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def prefix_vars(astnode, prefix):\n", " if isinstance(astnode, ast.BoolOp):\n", " return ast.BoolOp(astnode.op,\n", " [prefix_vars(i, prefix) for i in astnode.values], [])\n", " elif isinstance(astnode, ast.BinOp):\n", " return ast.BinOp(\n", " prefix_vars(astnode.left, prefix), astnode.op,\n", " prefix_vars(astnode.right, prefix))\n", " elif isinstance(astnode, ast.UnaryOp):\n", " return ast.UnaryOp(astnode.op, prefix_vars(astnode.operand, prefix))\n", " elif isinstance(astnode, ast.Call):\n", " return ast.Call(prefix_vars(astnode.func, prefix),\n", " [prefix_vars(i, prefix) for i in astnode.args],\n", " astnode.keywords)\n", " elif isinstance(astnode, ast.Compare):\n", " return ast.Compare(\n", " prefix_vars(astnode.left, prefix), astnode.ops,\n", " [prefix_vars(i, prefix) for i in astnode.comparators])\n", " elif isinstance(astnode, ast.Name):\n", " if astnode.id in {'And', 'Or', 'Not'}:\n", " return ast.Name('z3.%s' % (astnode.id), astnode.ctx)\n", " else:\n", " return ast.Name('%s_%s' % (prefix, astnode.id), astnode.ctx)\n", " elif isinstance(astnode, ast.Return):\n", " return ast.Return(prefix_vars(astnode.value, env))\n", " else:\n", " return astnode" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "The function `to_src()` allows us to *unparse* an expression." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def to_src(astnode):\n", " return astunparse.unparse(astnode).strip()" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def get_expression(src):\n", " return ast.parse(src).body[0].value" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Now, we can combine both pieces to produce a prefixed expression as below." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "abs_value_summary_ast = get_expression(str(abs_value_summary))\n", "to_src(prefix_vars(abs_value_summary_ast, 'x1'))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### names" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We need the names of variables used in an expression to declare the to declare them. The method `names()` extracts variables used." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def names(astnode):\n", " lst = []\n", " if isinstance(astnode, ast.BoolOp):\n", " for i in astnode.values:\n", " lst.extend(names(i))\n", " elif isinstance(astnode, ast.BinOp):\n", " lst.extend(names(astnode.left))\n", " lst.extend(names(astnode.right))\n", " elif isinstance(astnode, ast.UnaryOp):\n", " lst.extend(names(astnode.operand))\n", " elif isinstance(astnode, ast.Call):\n", " for i in astnode.args:\n", " lst.extend(names(i))\n", " elif isinstance(astnode, ast.Compare):\n", " lst.extend(names(astnode.left))\n", " for i in astnode.comparators:\n", " lst.extend(names(i))\n", " elif isinstance(astnode, ast.Name):\n", " lst.append(astnode.id)\n", " elif isinstance(astnode, ast.Expr):\n", " lst.extend(names(astnode.value))\n", " elif isinstance(astnode, (ast.Num, ast.Str, ast.Tuple, ast.NameConstant)):\n", " pass\n", " elif isinstance(astnode, ast.Assign):\n", " for t in astnode.targets:\n", " lst.extend(names(t))\n", " lst.extend(names(astnode.value))\n", " elif isinstance(astnode, ast.Module):\n", " for b in astnode.body:\n", " lst.extend(names(b))\n", " else:\n", " raise Exception(str(astnode))\n", " return list(set(lst))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "With this, we can now extract the variables used in an expression." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "v = ast.parse('fn(x+z,y>(a+b)) == c')\n", "names(v)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "abs_value_vars = names(ast.parse(str(abs_value_summary)))\n", "abs_value_vars" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Registering functions for later use." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "function_summaries = {}\n", "function_summaries['abs_value'] = {\n", " 'predicate': str(abs_value_summary),\n", " 'vars': abs_value_vars}" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def define_vars(fn_vars, sym_fn='z3.Int'):\n", " sym_var_dec = ', '.join(fn_vars)\n", " sym_var_def = ', '.join([\"%s('%s')\" % (sym_fn, i) for i in fn_vars])\n", " return \"%s = %s\" % (sym_var_dec, sym_var_def)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def gen_fn_summary(prefix, fn, sym_fn='z3.Int'):\n", " fn_name = fn.__name__\n", " summary = function_summaries[fn_name]\n", " summary_ast = ast.parse(summary['predicate']).body[0].value\n", " fn_vars = [\"%s_%s\" % (prefix, s) for s in summary['vars']]\n", " declarations = define_vars(fn_vars, sym_fn)\n", " return declarations, to_src(prefix_vars(summary_ast, prefix))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "gen_fn_summary('a', abs_value)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "gen_fn_summary('b', abs_value)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "How do we use our function summaries? Here is a function `abs_max()` that uses `abs_value()`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def abs_max(a, b):\n", " a1 = abs_value(a)\n", " b1 = abs_value(b)\n", " if a1 > b1:\n", " c = a1\n", " else:\n", " c = b1\n", " return c" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "To trace this function symbolically, we first define the two variables `a` and `b`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "a = z3.Int('a')\n", "b = z3.Int('b')" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The `line: 2` contains definition for `a1`, which we define as a symbolic variable." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "a1 = z3.Int('a1')" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We also need to call `abs_value()`, which is accomplished as follows. Since this is the first call to `abs_value()`, we use `abs1` as the prefix." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "d, v = gen_fn_summary('abs1', abs_value)\n", "v" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We also need to equate the resulting value (`_v`) to the symbolic variable `a1` we defined earlier." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "l2_src = \"l2 = z3.And(a == abs1_x, a1 == abs1_v, %s)\" % v\n", "l2_src" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Applying both declaration and the assignment." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "exec(d)\n", "exec(l2_src)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "l2" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We need to do the same for `line: 3`, but with `abs2` as the prefix." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "b1 = z3.Int('b1')\n", "d, v = gen_fn_summary('abs2', abs_value)\n", "l3_src = \"l3_ = z3.And(b == abs2_x, b1 == abs2_v, %s)\" % v\n", "exec(d)\n", "exec(l3_src)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "l3_" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "To get the true set of predicates at `line: 3`, we need to add the predicates from `line: 2`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "l3 = z3.And(l2, l3_)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "l3" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "This equation can be simplified a bit using z3." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "z3.simplify(l3)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "Coming to `line: 4`, we have a condition." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "l4_cond = a1 > b1\n", "l4 = z3.And(l3, l4_cond)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "For `line: 5`, we define the symbolic variable `c_0` assuming we took the *IF* branch." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "c_0 = z3.Int('c_0')\n", "l5 = z3.And(l4, c_0 == a1)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "For `line: 6`, the *ELSE* branch was taken. So we invert that condition." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "l6 = z3.And(l3, z3.Not(l4_cond))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "For `line: 7`, we define `c_1`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "c_1 = z3.Int('c_1')\n", "l7 = z3.And(l6, c_1 == b1)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "s1 = z3.Solver()\n", "s1.add(l5)\n", "s1.check()" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "m1 = s1.model()\n", "sorted([(d, m1[d]) for d in m1.decls() if not d.name(\n", ").startswith('abs')], key=lambda x: x[0].name())" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "s2 = z3.Solver()\n", "s2.add(l7)\n", "s2.check()" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "m2 = s2.model()\n", "sorted([(d, m2[d]) for d in m2.decls() if not d.name(\n", ").startswith('abs')], key=lambda x: x[0].name())" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "What we really want to do is to automate this process, because doing this by hand is tedious and error prone. Essentially, we want the ability to extract *all paths* in the program, and symbolically execute each path, which will generate the inputs required to cover all reachable portions of the program." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Symbolic Execution" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "We define a simple *symbolic fuzzer* that can generate input values *symbolically* with the following assumptions:\n", "\n", "* There are no loops in the program\n", "* The function is self contained.\n", "* No recursion.\n", "* No reassignments for variables.\n", "\n", "The key idea is as follows: We traverse through the control flow graph from the entry point, and generate all possible paths to a given depth. Then we collect constraints that we encountered along the path, and generate inputs that will traverse the program up to that point." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "We build our fuzzer based on the class `Fuzzer`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "from Fuzzer import Fuzzer" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### SimpleSymbolicFuzzer" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We start by extracting the control flow graph of the function passed. We also provide a hook for child classes to do their processing." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class SimpleSymbolicFuzzer(Fuzzer):\n", " def __init__(self, fn, **kwargs):\n", " self.fn = fn\n", " self.fn_src = inspect.getsource(fn)\n", " self.fn_args = list(inspect.signature(fn).parameters)\n", " self.py_cfg = PyCFG()\n", " self.py_cfg.gen_cfg(self.fn_src)\n", " self.fnenter, self.fnexit = self.py_cfg.functions[fn.__name__]\n", " self.paths = None\n", " self.last_path = None\n", " self.removed_solutions = []\n", " self.z3 = z3.Solver()\n", " self.options(kwargs)\n", " self.process()\n", "\n", " def process(self):\n", " pass" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "We need a few variables to control how much we are willing to traverse." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "`MAX_DEPTH` is the depth to which one should attempt to trace the execution." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "MAX_DEPTH = 100" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "`MAX_TRIES` is the maximum number of attempts we will try to produce a value before giving up." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "MAX_TRIES = 100" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "`MAX_ITER` is the number of iterations we will attempt." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "MAX_ITER = 100" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The `options()` method sets these parameters in the fuzzing class." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class SimpleSymbolicFuzzer(SimpleSymbolicFuzzer):\n", " def options(self, kwargs):\n", " self.max_depth = kwargs.get('max_depth', MAX_DEPTH)\n", " self.max_tries = kwargs.get('max_tries', MAX_TRIES)\n", " self.max_iter = kwargs.get('max_iter', MAX_ITER)\n", " self.symbolic_fn = kwargs.get('symbolic_fn', 'z3.Int')\n", " self._options = kwargs" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The initialization generates a control flow graph and hooks it to `fnenter` and `fnexit`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "symfz_ct = SimpleSymbolicFuzzer(check_triangle)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "symfz_ct.fnenter, symfz_ct.fnexit" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### get_all_paths\n", "We can use the procedure `get_all_paths()` starting from `fnenter` to recursively retrieve all paths in the function.\n", "\n", "In the CFG, in the case of if-then-else branches, the first node is the `If` branch, while the second node is the `Else` branch. Hence, we keep track of the order of definition in `idx`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class SimpleSymbolicFuzzer(SimpleSymbolicFuzzer):\n", " def get_all_paths(self, fenter, depth=0):\n", " if depth > self.max_depth:\n", " raise Exception('Maximum depth exceeded')\n", " if not fenter.children:\n", " return [[(0, fenter)]]\n", "\n", " fnpaths = []\n", " for idx, child in enumerate(fenter.children):\n", " child_paths = self.get_all_paths(child, depth + 1)\n", " for path in child_paths:\n", " fnpaths.append([(idx, fenter)] + path)\n", " return fnpaths" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "This can be used as follows." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "symfz_ct = SimpleSymbolicFuzzer(check_triangle)\n", "paths = symfz_ct.get_all_paths(symfz_ct.fnenter)\n", "print(len(paths))\n", "paths[1]" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We hook `get_all_paths()` to initialization as below." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class SimpleSymbolicFuzzer(SimpleSymbolicFuzzer):\n", " def process(self):\n", " self.paths = self.get_all_paths(self.fnenter)\n", " self.last_path = len(self.paths)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### extract_constraints\n", "\n", "For any given path, we define a function `extract_constraints()` to extract the constraints in `z3` format. Given that the order of the child shows which branch was taken, we need to shift" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class SimpleSymbolicFuzzer(SimpleSymbolicFuzzer):\n", " def extract_constraints(self, path):\n", " predicates = []\n", " for (idx, elt) in path:\n", " if isinstance(elt.ast_node, ast.AnnAssign):\n", " if elt.ast_node.target.id in {'_if', '_while'}:\n", " s = to_src(elt.ast_node.annotation)\n", " predicates.append((\"%s\" if idx == 0 else \"z3.Not%s\") % s)\n", " elif isinstance(elt.ast_node, ast.Assign):\n", " predicates.append(to_src(elt.ast_node))\n", " else:\n", " pass\n", " return predicates" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "symfz_ct = SimpleSymbolicFuzzer(check_triangle)\n", "paths = symfz_ct.get_all_paths(symfz_ct.fnenter)\n", "constraints = symfz_ct.extract_constraints(paths[1])\n", "constraints" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The method `used_vars()` extracts the symbolic variables to be defined from an expression." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def used_vars(predicates):\n", " return list(set([n for p in predicates for n in names(get_expression(p))]))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "used_vars(constraints)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "symfz_ct.extract_constraints(paths[0])" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### Fuzzing with our simple fuzzer" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "To actually generate solutions, we define `fuzz()`. For that, we need to first extract all paths. Then choose a particular path, and extract the constraints in that path, which is then solved using *z3*." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "from contextlib import contextmanager" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "First we create a checkpoint for our current solver so that we can check a predicate, and rollback if necessary." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "@contextmanager\n", "def checkpoint(z3solver):\n", " z3solver.push()\n", " yield z3solver\n", " z3solver.pop()" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "The `use_path()` function extracts constraints for a single function, applies it to our current solver (under a checkpoint), and returns the results if some solutions can be found.\n", "\n", "If solutions were found, we also make sure that we never reuse those solutions." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class SimpleSymbolicFuzzer(SimpleSymbolicFuzzer):\n", " def solve_path_constraint(self, path):\n", " # re-initializing does not seem problematic.\n", " # a = z3.Int('a').get_id() remains the same.\n", " constraints = self.extract_constraints(path)\n", " exec(define_vars(used_vars(constraints), self.symbolic_fn))\n", "\n", " solutions = {}\n", " with checkpoint(self.z3):\n", " st = 'self.z3.add(%s)' % ', '.join(constraints)\n", " eval(st)\n", " if self.z3.check() != z3.sat:\n", " return {}\n", " m = self.z3.model()\n", " solutions = {d.name(): m[d] for d in m.decls()}\n", " my_args = {k: solutions.get(k, None) for k in self.fn_args}\n", " predicate = 'z3.And(%s)' % ','.join(\n", " [\"%s == %s\" % (k, v) for k, v in my_args.items()])\n", " eval('self.z3.add(z3.Not(%s))' % predicate)\n", " return my_args" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "We define `get_path()` that retrieves the current path and updates the path used." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class SimpleSymbolicFuzzer(SimpleSymbolicFuzzer):\n", " def get_next_path(self):\n", " self.last_path -= 1\n", " if self.last_path == -1:\n", " self.last_path = len(self.paths) - 1\n", " return self.paths[self.last_path]" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The `fuzz()` method simply solves each path in order." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class SimpleSymbolicFuzzer(SimpleSymbolicFuzzer):\n", " def fuzz(self):\n", " for i in range(self.max_tries):\n", " res = self.solve_path_constraint(self.get_next_path())\n", " if res:\n", " return res\n", " return {}" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The fuzzer can be used as follows." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "a, b, c = None, None, None\n", "symfz_ct = SimpleSymbolicFuzzer(check_triangle)\n", "for i in range(1, 10):\n", " r = symfz_ct.fuzz()\n", " v = check_triangle(r['a'].as_long(), r['b'].as_long(), r['c'].as_long())\n", " print(r, \"result:\", v)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### Problems with the Simple Fuzzer" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "As we mentioned earlier, the `SimpleSymbolicFuzzer` cannot yet deal with variable reassignments. Further, it also fails to account for any loops. For example, consider the following program." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def gcd(a, b):\n", " if a < b:\n", " c = a\n", " a = b\n", " b = c\n", "\n", " while b != 0:\n", " c = a\n", " a = b\n", " b = c % b\n", " return a" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "Source(to_graph(gen_cfg(inspect.getsource(gcd))))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "from ExpectError import ExpectError" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "with ExpectError():\n", " symfz_gcd = SimpleSymbolicFuzzer(gcd)\n", " for i in range(1, 100):\n", " r = symfz_gcd.fuzz()\n", " v = gcd(r['a'].as_long(), r['b'].as_long())\n", " print(r, v)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### Advanced Symbolic Fuzzer" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We next define `AdvancedSymbolicFuzzer` that can deal with reassignments and *unrolling of loops*." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class AdvancedSymbolicFuzzer(SimpleSymbolicFuzzer):\n", " def options(self, kwargs):\n", " super().options(kwargs)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Once we allow reassignments and loop unrolling, we have to deal with what to call the new variables generated. This is what we will tackle next." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### rename_variables" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We want to rename all variables present in an expression such that the variables are annotated with their usage count. This makes it possible to determine variable reassignments. To do that, we define the `rename_variables()` function that, when given an `env` that contains the current usage index of different variables, renames the variables in the passed in AST node with the annotations.\n", "\n", "That is, if the expression is `env[v] == 1`, `v` is renamed to `_v_1`" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def rename_variables(astnode, env):\n", " if isinstance(astnode, ast.BoolOp):\n", " fn = 'z3.And' if isinstance(astnode.op, ast.And) else 'z3.Or'\n", " return ast.Call(\n", " ast.Name(fn, None),\n", " [rename_variables(i, env) for i in astnode.values], [])\n", " elif isinstance(astnode, ast.BinOp):\n", " return ast.BinOp(\n", " rename_variables(astnode.left, env), astnode.op,\n", " rename_variables(astnode.right, env))\n", " elif isinstance(astnode, ast.UnaryOp):\n", " if isinstance(astnode.op, ast.Not):\n", " return ast.Call(\n", " ast.Name('z3.Not', None),\n", " [rename_variables(astnode.operand, env)], [])\n", " else:\n", " return ast.UnaryOp(astnode.op,\n", " rename_variables(astnode.operand, env))\n", " elif isinstance(astnode, ast.Call):\n", " return ast.Call(astnode.func,\n", " [rename_variables(i, env) for i in astnode.args],\n", " astnode.keywords)\n", " elif isinstance(astnode, ast.Compare):\n", " return ast.Compare(\n", " rename_variables(astnode.left, env), astnode.ops,\n", " [rename_variables(i, env) for i in astnode.comparators])\n", " elif isinstance(astnode, ast.Name):\n", " if astnode.id not in env:\n", " env[astnode.id] = 0\n", " num = env[astnode.id]\n", " return ast.Name('_%s_%d' % (astnode.id, num), astnode.ctx)\n", " elif isinstance(astnode, ast.Return):\n", " return ast.Return(rename_variables(astnode.value, env))\n", " else:\n", " return astnode" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "To verify that it works ans intended, we start with an environment." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "env = {'x': 1}" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "ba = get_expression('x == 1 and y == 2')\n", "type(ba)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "assert to_src(rename_variables(ba, env)) == 'z3.And((_x_1 == 1), (_y_0 == 2))'" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "bo = get_expression('x == 1 or y == 2')\n", "type(bo.op)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "assert to_src(rename_variables(bo, env)) == 'z3.Or((_x_1 == 1), (_y_0 == 2))'" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "b = get_expression('x + y')\n", "type(b)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "assert to_src(rename_variables(b, env)) == '(_x_1 + _y_0)'" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "u = get_expression('-y')\n", "type(u)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "assert to_src(rename_variables(u, env)) == '(- _y_0)'" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "un = get_expression('not y')\n", "type(un.op)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "assert to_src(rename_variables(un, env)) == 'z3.Not(_y_0)'" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "c = get_expression('x == y')\n", "type(c)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "assert to_src(rename_variables(c, env)) == '(_x_1 == _y_0)'" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "f = get_expression('fn(x,y)')\n", "type(f)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "assert to_src(rename_variables(f, env)) == 'fn(_x_1, _y_0)'" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "env" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Next, we want to process the CFG, and correctly transform the paths." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### PNode" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "For keeping track of assignments in the CFG, We define a data structure `PNode` that stores the current CFG node." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class PNode:\n", " def __init__(self, idx, cfgnode, parent=None, order=0):\n", " self.idx, self.cfgnode, self.parent, self.order = idx, cfgnode, parent, order\n", "\n", " def __repr__(self):\n", " return \"PNode:%d[%s order:%d]\" % (self.idx, str(self.cfgnode),\n", " self.order)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Defining a new `PNode` is done as follows." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "cfg = PyCFG()\n", "cfg.gen_cfg(inspect.getsource(gcd))\n", "fnenter, fnexit = cfg.functions['gcd']" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "PNode(0, fnenter)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "##### copy\n", "The `copy()` method generates a copy for the child's keep, indicating which path was taken (with `order` of the child)." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class PNode(PNode):\n", " def copy(self, order):\n", " p = PNode(self.idx, self.cfgnode, self.parent, order)\n", " assert p.order == order\n", " return p" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Using the copy operation." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "PNode(0, fnenter).copy(1)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "##### explore" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "A problem we had with our `SimpleSymbolicFuzzer` is that it explored a path to completion before attempting another. However, this is non-optimal. One may want to explore the graph in a more step-wise manner, expanding every possible execution one step at a time.\n", "\n", "Hence, we define `explore()` which explores the children of a node if any, one step at a time. If done exhaustively, this will generate all paths from a starting node until no more children are left. We made `PNode` to a container class so that this iteration can be driven from outside, and stopped if say a maximum iteration is complete, or certain paths need to be prioritized." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class PNode(PNode):\n", " def explore(self):\n", " return [\n", " PNode(self.idx + 1, n, self.copy(i))\n", " for (i, n) in enumerate(self.cfgnode.children)\n", " ]" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We can use `explore()` as follows." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "PNode(0, fnenter).explore()" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "PNode(0, fnenter).explore()[0].explore()" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "##### get_path_to_root" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The method `get_path_to_root()` recursively goes up through child->parent chain retrieving the complete chain to the topmost parent." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "code_folding": [], "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class PNode(PNode):\n", " def get_path_to_root(self):\n", " path = []\n", " n = self\n", " while n:\n", " path.append(n)\n", " n = n.parent\n", " return list(reversed(path))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "p = PNode(0, fnenter)\n", "[s.get_path_to_root() for s in p.explore()[0].explore()[0].explore()[0].explore()]" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The string representation of the node is in `z3` solvable form." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class PNode(PNode):\n", " def __str__(self):\n", " path = self.get_path_to_root()\n", " ssa_path = to_single_assignment_predicates(path)\n", " return ', '.join([to_src(p) for p in ssa_path])" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "However, before using it, we need to define the `rename_variables()`. But first, we define `names()`." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "###### to_single_assignment_predicates" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We need to rename used variables. Any variable `v = xxx` should be renamed to `_v_0` and any later assignment such as `v = v + 1` should be transformed to `_v_1 = _v_0 + 1` and later conditionals such as `v == x` should be transformed to `(_v_1 == _x_0)`. The method `to_single_assignment_predicates()` does this for a given path." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def to_single_assignment_predicates(path):\n", " env = {}\n", " new_path = []\n", " for i, node in enumerate(path):\n", " ast_node = node.cfgnode.ast_node\n", " new_node = None\n", " if isinstance(ast_node, ast.AnnAssign) and ast_node.target.id in {\n", " 'exit'}:\n", " new_node = None\n", " elif isinstance(ast_node, ast.AnnAssign) and ast_node.target.id in {'enter'}:\n", " args = [\n", " ast.parse(\n", " \"%s == _%s_0\" %\n", " (a.id, a.id)).body[0].value for a in ast_node.annotation.args]\n", " new_node = ast.Call(ast.Name('z3.And', None), args, [])\n", " elif isinstance(ast_node, ast.AnnAssign) and ast_node.target.id in {'_if', '_while'}:\n", " new_node = rename_variables(ast_node.annotation, env)\n", " if node.order != 0:\n", " assert node.order == 1\n", " new_node = ast.Call(ast.Name('z3.Not', None), [new_node], [])\n", " elif isinstance(ast_node, ast.Assign):\n", " assigned = ast_node.targets[0].id\n", " val = [rename_variables(ast_node.value, env)]\n", " env[assigned] = 0 if assigned not in env else env[assigned] + 1\n", " target = ast.Name('_%s_%d' %\n", " (ast_node.targets[0].id, env[assigned]), None)\n", " new_node = ast.Expr(ast.Compare(target, [ast.Eq()], val))\n", " elif isinstance(ast_node, (ast.Return, ast.Pass)):\n", " new_node = None\n", " else:\n", " s = \"NI %s %s\" % (type(ast_node), ast_node.target.id)\n", " raise Exception(s)\n", " new_path.append(new_node)\n", " return new_path" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "p = PNode(0, fnenter)\n", "path = p.explore()[0].explore()[0].explore()[0].get_path_to_root()\n", "spath = to_single_assignment_predicates(path)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "[to_src(s) for s in spath]" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "assert set(q for s in spath for q in names(s)) == {\n", " '_a_0', '_a_1', '_b_0', '_c_0', 'a', 'b'}" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "##### can_be_satisfied\n", "\n", "One of the ways in which the *concolic* execution simplifies *symbolic* execution is in the treatment of loops. Rather than trying to determine an invariant for a loop, we simply *unroll* the loops a number of times until we hit the `MAX_DEPTH` limit. However, not all loops will need to be unrolled until `MAX_DEPTH` is reached. Some of them may exit before. Hence, it is necessary to check whether the given set of constraints can be satisfied before continuing to explore further. " ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class AdvancedSymbolicFuzzer(AdvancedSymbolicFuzzer):\n", " def can_be_satisfied(self, p):\n", " s2 = self.extract_constraints(p.get_path_to_root())\n", " s = z3.Solver()\n", " exec(define_vars(used_vars(s2), self.symbolic_fn), globals(), locals())\n", " exec(\"s.add(z3.And(%s))\" % ','.join(s2), globals(), locals())\n", " return s.check() == z3.sat" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### extract_constraints\n", "\n", "The `extract_constraints()` generates the `z3` constraints from a path. The main work is done by `to_single_assignment_predicates()`. The `extract_constraints()` then converts the AST to source." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class AdvancedSymbolicFuzzer(AdvancedSymbolicFuzzer):\n", " def extract_constraints(self, path):\n", " return [to_src(p) for p in to_single_assignment_predicates(path) if p]" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### get_all_paths" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Get all paths one can generate from function enter node (`fenter`) subject to max_depth limit." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class AdvancedSymbolicFuzzer(AdvancedSymbolicFuzzer):\n", " def get_all_paths(self, fenter):\n", " path_lst = [PNode(0, fenter)]\n", " completed = []\n", " for i in range(self.max_iter):\n", " new_paths = [PNode(0, fenter)]\n", " for path in path_lst:\n", " # explore each path once\n", " if path.cfgnode.children:\n", " np = path.explore()\n", " for p in np:\n", " if path.idx > self.max_depth:\n", " break\n", " if self.can_be_satisfied(p):\n", " new_paths.append(p)\n", " else:\n", " pass\n", " else:\n", " completed.append(path)\n", " path_lst = new_paths\n", " return completed + path_lst" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "We can now obtain all paths using our advanced symbolic fuzzer as follows." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "asymfz_gcd = AdvancedSymbolicFuzzer(\n", " gcd, max_iter=10, max_tries=10, max_depth=10)\n", "paths = asymfz_gcd.get_all_paths(asymfz_gcd.fnenter)\n", "print(len(paths))\n", "paths[37].get_path_to_root()" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "We can also list the predicates in each path." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "for s in to_single_assignment_predicates(paths[37].get_path_to_root()):\n", " if s is not None:\n", " print(to_src(s))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "constraints = asymfz_gcd.extract_constraints(paths[37].get_path_to_root())" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "constraints" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "used_vars(constraints)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### Fuzzing with our advanced fuzzer" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class AdvancedSymbolicFuzzer(AdvancedSymbolicFuzzer):\n", " def get_next_path(self):\n", " self.last_path -= 1\n", " if self.last_path == -1:\n", " self.last_path = len(self.paths) - 1\n", " return self.paths[self.last_path].get_path_to_root()" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "asymfz_gcd = AdvancedSymbolicFuzzer(\n", " gcd, max_tries=10, max_iter=10, max_depth=10)\n", "data = []\n", "for i in range(10):\n", " r = asymfz_gcd.fuzz()\n", " data.append((r['a'].as_long(), r['b'].as_long()))\n", " v = gcd(*data[-1])\n", " print(r, \"result:\", repr(v))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "What is our coverage?" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " for a, b in data:\n", " gcd(a, b)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "cov.show_coverage(gcd)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "Source(to_graph(gen_cfg(inspect.getsource(gcd)), arcs=cov_to_arcs(cov)))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "How do we make use of our fuzzer in practice? We explore a small case study of a program to solve the roots of a quadratic equation." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### Example: roots\n", "Here is the famous equation for finding the roots of quadratic equations." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def roots(a, b, c):\n", " d = b * b - 4 * a * c\n", " ax = 0.5 * d\n", " bx = 0\n", " while (ax - bx) > 0.1:\n", " bx = 0.5 * (ax + d / ax)\n", " ax = bx\n", " s = bx\n", "\n", " a2 = 2 * a\n", " ba2 = b / a2\n", " return -ba2 + s / a2, -ba2 - s / a2" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "Does the program look correct? Let us investigate if the program is reasonable. But before that, we need a helper\n", "function `sym_to_float()` to convert symbolic values to floating point." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def sym_to_float(v):\n", " if v is None:\n", " return math.inf\n", " return v.numerator_as_long() / v.denominator_as_long()" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Now we are ready to fuzz." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "asymfz_roots = AdvancedSymbolicFuzzer(\n", " roots,\n", " max_tries=10,\n", " max_iter=10,\n", " max_depth=10,\n", " symbolic_fn='z3.Real')\n", "with ExpectError():\n", " for i in range(100):\n", " r = asymfz_roots.fuzz()\n", " d = [sym_to_float(r[i]) for i in ['a', 'b', 'c']]\n", " v = roots(*d)\n", " print(d, v)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "We have a `ZeroDivisionError`. Can we eliminate it?" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "##### roots - take 2" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def roots2(a, b, c):\n", " d = b * b - 4 * a * c\n", "\n", " xa = 0.5 * d\n", " xb = 0\n", " while (xa - xb) > 0.1:\n", " xb = 0.5 * (xa + d / xa)\n", " xa = xb\n", " s = xb\n", "\n", " if a == 0:\n", " return -c / b\n", "\n", " a2 = 2 * a\n", " ba2 = b / a2\n", " return -ba2 + s / a2, -ba2 - s / a2" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "asymfz_roots = AdvancedSymbolicFuzzer(\n", " roots2,\n", " max_tries=10,\n", " max_iter=10,\n", " max_depth=10,\n", " symbolic_fn='z3.Real')\n", "with ExpectError():\n", " for i in range(1000):\n", " r = asymfz_roots.fuzz()\n", " d = [sym_to_float(r[i]) for i in ['a', 'b', 'c']]\n", " v = roots2(*d)\n", " #print(d, v)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "Apparently, our fix was incomplete. Let us try again." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "##### roots - take 3" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "import math" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def roots3(a, b, c):\n", " d = b * b - 4 * a * c\n", "\n", " xa = 0.5 * d\n", " xb = 0\n", " while (xa - xb) > 0.1:\n", " xb = 0.5 * (xa + d / xa)\n", " xa = xb\n", " s = xb\n", "\n", " if a == 0:\n", " if b == 0:\n", " return math.inf\n", " return -c / b\n", "\n", " a2 = 2 * a\n", " ba2 = b / a2\n", " return -ba2 + s / a2, -ba2 - s / a2" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "asymfz_roots = AdvancedSymbolicFuzzer(\n", " roots3,\n", " max_tries=10,\n", " max_iter=10,\n", " max_depth=10,\n", " symbolic_fn='z3.Real')\n", "# with ExpectError():\n", "for i in range(10):\n", " r = asymfz_roots.fuzz()\n", " print(r)\n", " d = [sym_to_float(r[i]) for i in ['a', 'b', 'c']]\n", " v = roots3(*d)\n", " print(d, v)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### Problems with our advanced fuzzer" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "There is an evident error in this program. We are not checking for negative roots. However, the symbolic execution does not seem to have detected it." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Why are we not able to detect the problem of negative roots? Because we stop execution at a predetermined depth without throwing an error. That is, our symbolic execution is wide but shallow.\n", "\n", "Is there a way to make it go deep? One solution is to go for the *Concolic Execution*." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "### Concolic Execution" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "In *concolic execution*, we rely on a seed input to guide our symbolic execution. We collect the line numbers that our seed input traces, and feed it to the symbolic execution such that in the `explore` step, only the child node that correspond to the seed input execution path is chosen. This allows us to collect the complete set of constraints along a *representative path*. Once we have it, we can choose any particular predicate and invert it to explore the program execution paths near the representative path." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We modify our original `Tracer` to provide *all* line numbers that the program traversed." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### ConcolicFuzzer" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "class Tracer(Tracer):\n", " def offsets_from_entry(self, fn):\n", " zero = self._trace[0][1] - 1\n", " return [l-zero for (f,l) in self._trace if f == fn]" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " roots3(1, 1, 1)" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "cov.offsets_from_entry('roots3')" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The `ConcolicFuzzer` first extracts the program trace on a seed input." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class ConcolicFuzzer(AdvancedSymbolicFuzzer):\n", " def __init__(self, fn, fnargs, **kwargs):\n", " with Tracer() as cov:\n", " fn(*fnargs)\n", " self.lines = cov.offsets_from_entry(fn.__name__)\n", " self.current_line = 0\n", " super().__init__(fn, **kwargs)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "##### get_all_paths\n", "The method `get_all_paths()` now tries to follow the seed execution path." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "class ConcolicFuzzer(ConcolicFuzzer):\n", " def get_all_paths(self, fenter):\n", " assert fenter.ast_node.lineno == self.lines[self.current_line]\n", " self.current_line += 1\n", " last_node = PNode(0, fenter)\n", " while last_node and self.current_line < len(self.lines):\n", " if last_node.cfgnode.children:\n", " np = last_node.explore()\n", " for p in np:\n", " if self.lines[self.current_line] == p.cfgnode.ast_node.lineno:\n", " self.current_line += 1\n", " last_node = p\n", " break\n", " else:\n", " last_node = None\n", " break\n", " else:\n", " break\n", " assert len(self.lines) == self.current_line\n", " return [last_node]\n", "\n", " def solve_path_constraint(self, path):\n", " # re-initializing does not seem problematic.\n", " # a = z3.Int('a').get_id() remains the same.\n", " constraints = self.extract_constraints(path)\n", " exec(define_vars(used_vars(constraints), self.symbolic_fn))\n", "\n", " solutions = {}\n", " with checkpoint(self.z3):\n", " eval('self.z3.add(%s)' % ', '.join(constraints))\n", " if self.z3.check() != z3.sat:\n", " return {}\n", " m = self.z3.model()\n", " solutions = {d.name(): m[d] for d in m.decls()}\n", " my_args = {k: solutions.get(k, None) for k in self.fn_args}\n", " predicate = 'z3.And(%s)' % ','.join(\n", " [\"%s == %s\" % (k, v) for k, v in my_args.items()])\n", " eval('self.z3.add(z3.Not(%s))' % predicate)\n", " return my_args" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### Fuzzing with our concolic fuzzer" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "acfz_roots = ConcolicFuzzer(\n", " roots3,\n", " fnargs=[1, 1, 1],\n", " max_tries=10,\n", " max_iter=10,\n", " max_depth=10,\n", " symbolic_fn='z3.Real')" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "acfz_roots.paths[0].get_path_to_root()" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "print([i.cfgnode.ast_node.lineno for i in acfz_roots.paths[0].get_path_to_root()])\n", "print(acfz_roots.lines)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We extract the constraints as usual." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "constraints = acfz_roots.extract_constraints(\n", " acfz_roots.paths[0].get_path_to_root())" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "constraints" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The used vars are first as symbolic." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "exec(define_vars(used_vars(constraints), 'z3.Real'))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "We can now solve our constraints. However, before that, here is a question for you.\n", "\n", "Should it result in exactly the same arguments?" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "eval('z3.solve(%s)' % ','.join(constraints))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "acfz_roots.fuzz()" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Did they take the same path?" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " roots(1, 1, 1)\n", "Source(to_graph(gen_cfg(inspect.getsource(roots)), arcs=cov_to_arcs(cov)))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " roots(1, 1 / 8, 1)\n", "Source(to_graph(gen_cfg(inspect.getsource(roots)), arcs=cov_to_arcs(cov)))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Remember our constraints" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "constraints" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### Exploring nearby paths\n", "\n", "We can explore nearby paths by negating some of the predicates." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "new_constraints = constraints[0:4] + ['z3.Not(%s)' % constraints[4]]" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "new_constraints" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "eval('z3.solve(%s)' % ','.join(new_constraints))" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "with Tracer() as cov:\n", " roots3(1, 0, -11 / 20)\n", "Source(to_graph(gen_cfg(inspect.getsource(roots3)), arcs=cov_to_arcs(cov)))" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "\\todo{Function summaries and variable renaming}" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Our symbolic fuzzer is reasonable for single functions that use `Int` or `Real` values. However, real world applications often contain multiple recursive method calls, which will not be handled by our implementation. Nor are real applications restricted to using just numbers.\n", "\n", "We will examine an implementation that can handle practical programs next." ] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": true, "run_control": { "read_only": false }, "slideshow": { "slide_type": "slide" } }, "source": [ "## Concolic Execution with PyExZ3" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ " **Requires the PyExZ3 pip package from [here](https://github.com/uds-se/PyExZ3).**\n", " \n", "[PyExZ3](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/dse.pdf) is a concolic evaluator of programs that takes a different strategy from what we did here. Similar to our dynamic taint approach, the PyExZ3 wraps the Python data structures so that they are symbolic equivalents. These data structures are then traced through program execution, and constraints are collected at the end." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "```python\n", "import PyExZ3.pyloader\n", "import symbolic.symbolic_types as st\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "```python\n", "generatedInputs, returnVals, path = PyExZ3.pyloader.exploreFunction(check_triangle)\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "We can get *PyExZ3* to print a flow graph of the conditions it examined." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "```python\n", "Source(path.toDot())\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "As in our implementation, *PyExZ3* also takes a `max_iters` argument." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "```python\n", "generatedInputs, returnVals, path = PyExZ3.pyloader.exploreFunction(gcd, max_iters=5)\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "```python\n", "Source(path.toDot())\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "This is useful in functions such as `factorial()`." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def factorial(n):\n", " if n <= 1:\n", " return 1\n", " return n * factorial(n - 1)" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "```python\n", "generatedInputs, returnVals, path = PyExZ3.pyloader.exploreFunction(factorial, max_iters=10)\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Our implementation did not yet implement symbolic execution through function calls. *PyExZ3* does handle symbolic execution across function boundaries." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "skip" } }, "outputs": [], "source": [ "import math" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def discriminant(a, b, c):\n", " return b * b - 4 * a * c" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def my_roots(a, b, c):\n", " if a == 0:\n", " if b == 0:\n", " return math.inf\n", " return -c / b\n", " d = discriminant(a, b, c)\n", " a2 = 2 * a\n", " ba2 = b / a2\n", " if d == 0:\n", " return -ba2\n", " s = math.sqrt(d)\n", " return -ba2 + s / a2, -ba2 - s / a2" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Remember what we mentioned about our implementation being unable to determine the error of the previous `roots()`? Would *PyExZ3* find it?" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "```python\n", "generatedInputs, returnVals, path = PyExZ3.pyloader.exploreFunction(my_roots)\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Unfortunately, it does not seem to detect it. The culprit is the `math.sqrt()` call. *PyExZ3* does not know how it behaves. Hence, it makes the returned variable unconstrained. It can be seen when we try to trace the function directly." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "```python\n", "with ExpectError():\n", " generatedInputs, returnVals, path = PyExZ3.pyloader.exploreFunction(math.sqrt)\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "The problem here is that *PyExZ3* does not know about *math.sqrt*. Can we help it?" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def sqrt(d):\n", " if d < 0:\n", " assert False\n", " xa = 0.5 * d\n", " xb = 0\n", " while (xa - xb) > 0.1:\n", " xb = 0.5 * (xa + d / xa)\n", " xa = xb\n", " s = xb\n", " return s" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def discriminant(a, b, c):\n", " return b * b - 4 * a * c" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def my_roots(a, b, c):\n", " if a == 0:\n", " if b == 0:\n", " return math.inf\n", " return -c / b\n", " d = discriminant(a, b, c)\n", " a2 = 2 * a\n", " ba2 = b / a2\n", " if d == 0:\n", " return -ba2\n", " s = sqrt(d)\n", " return -ba2 + s / a2, -ba2 - s / a2" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "With this, *PyExZ3* is ready to find all the problematic areas." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "```python\n", "with ExpectError():\n", " generatedInputs, returnVals, path = PyExZ3.pyloader.exploreFunction(my_roots, max_iters=1000)\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "#### roots - take 4" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def sqrt(d):\n", " if d < 0:\n", " assert False\n", " xa = 0.5 * d\n", " xb = 0\n", " while (xa - xb) > 0.1:\n", " xb = 0.5 * (xa + d / xa)\n", " xa = xb\n", " s = xb\n", " return s" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [ "def discriminant(a, b, c):\n", " return b * b - 4 * a * c" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "subslide" } }, "outputs": [], "source": [ "def roots4(a, b, c):\n", " if a == 0:\n", " if b == 0:\n", " return math.inf\n", " return -c / b\n", " d = discriminant(a, b, c)\n", " a2 = 2 * a\n", " ba2 = b / a2\n", " if d == 0:\n", " return -ba2\n", " elif d < 0:\n", " s = sqrt(-d)\n", " return (-ba2, s / a2), (-ba2, -s / a2)\n", " else:\n", " s = sqrt(d)\n", " return -ba2 + s / a2, -ba2 - s / a2" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "subslide" } }, "source": [ "And that indeed seems to be accepted by *PyExZ3*." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "```python\n", "generatedInputs, returnVals, path = PyExZ3.pyloader.exploreFunction(roots4, max_iters=1000)\n", "```" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Using Concolic Execution in Fuzzing" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "fragment" } }, "source": [ "Similar to dynamic taint analysis, one can consider *concolic execution* as a better oracle for fuzzing. For dynamic taints, we simply check whether taints reached any of the marked sinks on fuzzing, which helps us to not rely only on program crashes to detect that a program has vulnerabilities. Similarly, *concolic execution* needs to be driven by grammar based deep fuzzing, and the end result can be checked for specific properties such as information leak.\\todo{Expand}." ] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": true, "run_control": { "read_only": false }, "slideshow": { "slide_type": "slide" } }, "source": [ "## Lessons Learned\n", "\n", "* One can use symbolic execution to augment the inputs that explore all characteristics of a program.\n", "* Symbolic execution can be broad but shallow.\n", "* Concolic execution provides an acceptable middle ground, and uses a seed execution for guiding the symbolic exploration." ] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": false, "run_control": { "read_only": false }, "slideshow": { "slide_type": "slide" } }, "source": [ "## Next Steps\n", "\n", "* [Search based fuzzing](SearchBasedFuzzer.ipynb) can often be an acceptable middle ground when random fuzzing does not provide sufficient results, but symbolic fuzzing is too heavyweight." ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "slide" } }, "source": [ "## Background\n", "\n", "Symbolic execution of programs was originally described by King~\\cite{king1976symbolic} in 1976. It is used extensively in vulnerability analysis of software, especially binary programs. Some of the well known symbolic execution tools include KLEE~\\cite{KLEE}, Angr~\\cite{wang2017angr, stephens2016driller}, and SAGE~\\cite{godefroid2012sage}. The most well known symbolic execution environment for Python is CHEF~\\cite{bucur2014prototyping} which does symbolic execution by modifying the interpreter. PeerCheck~\\cite{PeerCheck} and PEF~\\cite{PEF} are two concolic execution engines." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "slideshow": { "slide_type": "fragment" } }, "outputs": [], "source": [] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": true, "run_control": { "read_only": false }, "slideshow": { "slide_type": "slide" } }, "source": [ "## Exercises" ] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": false, "run_control": { "read_only": false }, "slideshow": { "slide_type": "subslide" }, "solution": "hidden", "solution2": "hidden", "solution2_first": true, "solution_first": true }, "source": [ "### Exercise 1: _Extending Symbolic Fuzzer to use function summaries_\n", "\n", "We showed in the first section how function summaries may be produced. Can you extend the `AdvancedSymbolicFuzzer` to use function summaries when needed?" ] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": false, "run_control": { "read_only": false }, "slideshow": { "slide_type": "skip" }, "solution": "hidden", "solution2": "hidden" }, "source": [ "**Solution.** _None yet available._" ] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": false, "run_control": { "read_only": false }, "slideshow": { "slide_type": "subslide" }, "solution2": "hidden", "solution2_first": true }, "source": [ "### Exercise 2: _Inferring variable types for Concolic Fuzzer_\n", "\n", "Our `ConcolicFuzzer` assumes that all its variables are of the same category. However, most real world programs take inputs with different data types, and different data types are used during execution. Given that Python is a dynamic language, how do we know what to declare our variables as? One way (the simplest) is to rely on the types returned by the concrete execution. Can you modify our `ConcolicFuzzer` so that it uses the right variable types?" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "skip" }, "solution2": "hidden" }, "source": [ "**Solution.** _None yet available._" ] }, { "cell_type": "markdown", "metadata": { "button": false, "new_sheet": false, "run_control": { "read_only": false }, "slideshow": { "slide_type": "subslide" }, "solution2": "hidden", "solution2_first": true }, "source": [ "### Exercise 3: _Extending Concolic Fuzzer to trace through function calls_\n", "\n", "Unlike SymbolicFuzzers, a ConcolicFuzzer does not need function summaries. In fact, it needs to step through individual steps of functions it can get access to (For external functions such as `math.sqrt`, one still has to rely on function summaries). Can you extend the `ConcolicFuzzer` to trace across function boundaries?" ] }, { "cell_type": "markdown", "metadata": { "slideshow": { "slide_type": "skip" }, "solution2": "hidden" }, "source": [ "**Solution.** _None yet available._" ] } ], "metadata": { "ipub": { "bibliography": "fuzzingbook.bib", "toc": true }, "kernelspec": { "display_name": "Python 3", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.6.8" }, "toc": { "base_numbering": 1, "nav_menu": {}, "number_sections": true, "sideBar": true, "skip_h1_title": true, "title_cell": "", "title_sidebar": "Contents", "toc_cell": false, "toc_position": {}, "toc_section_display": true, "toc_window_display": true }, "toc-autonumbering": false, "varInspector": { "cols": { "lenName": 16, "lenType": 16, "lenVar": 40 }, "kernels_config": { "python": { "delete_cmd_postfix": "", "delete_cmd_prefix": "del ", "library": "var_list.py", "varRefreshCmd": "print(var_dic_list())" }, "r": { "delete_cmd_postfix": ") ", "delete_cmd_prefix": "rm(", "library": "var_list.r", "varRefreshCmd": "cat(var_dic_list()) " } }, "types_to_exclude": [ "module", "function", "builtin_function_or_method", "instance", "_Feature" ], "window_display": false } }, "nbformat": 4, "nbformat_minor": 2 }