First commit, passes a bunch of the Kocher test cases

Author: cdisselkoen

.gitignore

@@ -0,0 +1,4 @@
+.vscode
+__pycache__
+venv
+*~

driver.py

@@ -0,0 +1,155 @@
+from specvex import SimEngineSpecVEX, SpecState
+from oob import OOBState
+from spectre import SpectreState
+
+import angr
+import claripy
+import logging
+import monkeyhex
+
+logging.getLogger('angr.engines').setLevel(logging.INFO)
+#logging.getLogger('angr.engines.vex.expressions').setLevel(logging.INFO)
+#logging.getLogger('angr.engines.unicorn').setLevel(logging.INFO)
+#logging.getLogger('angr.engines.hook').setLevel(logging.INFO)
+logging.getLogger('angr.state_plugins.symbolic_memory').setLevel(logging.DEBUG)
+logging.getLogger('specvex').setLevel(logging.DEBUG)
+logging.getLogger('boundstracking').setLevel(logging.DEBUG)
+
+def fauxware():
+    proj = angr.Project('../angr-binaries/tests/x86_64/fauxware')
+    state = proj.factory.entry_state()
+    return (proj, state)
+
+def kocher(s):
+    """
+    Pass a string like "01" or "12" to get an angr project and state for that
+    Kocher test case.
+    """
+    proj = angr.Project('spectector-clang/'+s+'.o')
+    arg = claripy.BVS("x", 64)  # unconstrained
+    funcaddr = proj.loader.find_symbol("victim_function_v"+s).rebased_addr
+    state = proj.factory.call_state(funcaddr, arg)
+    state.globals['arg'] = arg
+    return (proj, state)
+
+def kocher11(s):
+    """
+    Pass one of 'gcc', 'ker', of 'sub' to get an angr project and state for
+    the Kocher test case '11gcc', '11ker', or '11sub' respectively.
+    """
+    proj = angr.Project('spectector-clang/11'+s+'.o')
+    arg = claripy.BVS("x", 64)  # unconstrained
+    funcaddr = proj.loader.find_symbol("victim_function_v11").rebased_addr
+    state = proj.factory.call_state(funcaddr, arg)
+    state.globals['arg'] = arg
+    return (proj, state)
+
+def blatantOOB():
+    proj = angr.Project('blatantOOB.o')
+    arg = claripy.BVS("x", 64)  # unconstrained
+    funcaddr = proj.loader.find_symbol("victim_function_v01").rebased_addr
+    state = proj.factory.call_state(funcaddr, arg)
+    state.globals['arg'] = arg
+    return (proj, state)
+
+def armBoundsChecks(proj,state):
+    state.register_plugin('oob', OOBState(proj))
+    assert len(state.oob.inbounds_intervals) > 0
+    state.oob.arm(state)
+    assert state.oob.armed()
+
+def armSpectreChecks(proj,state):
+    state.register_plugin('oob', OOBState(proj))
+    state.register_plugin('spectre', SpectreState())
+    state.spectre.arm(state)
+    assert state.spectre.armed()
+
+def makeSpeculative(proj, state):
+    proj.engines.register_plugin('specvex', SimEngineSpecVEX(1000))
+    proj.engines.order = ['specvex' if x=='vex' else x for x in proj.engines.order]  # replace 'vex' with 'specvex'
+    if proj.engines.has_plugin('vex'): proj.engines.release_plugin('vex')
+
+    #state.options.discard(angr.options.LAZY_SOLVES)  # turns out LAZY_SOLVES is not on by default
+    state.register_plugin('spec', SpecState())
+    assert state.spec.ins_executed == 0
+
+def runState(proj, state):
+    simgr = proj.factory.simgr(state, save_unsat=True)
+    if state.has_plugin('oob'):
+        simgr.use_technique(OOBViolationFilter())
+    if state.has_plugin('spectre'):
+        simgr.use_technique(SpectreViolationFilter())
+    simgr.run()
+    return simgr
+
+def showbbVEX(proj, bbaddr):
+    proj.factory.block(bbaddr).vex.pp()
+
+def showbbASM(proj, bbaddr):
+    proj.factory.block(bbaddr).capstone.pp()
+
+class OOBViolationFilter(angr.exploration_techniques.ExplorationTechnique):
+  def __init__(self):
+    super().__init__()
+
+  def filter(self, simgr, state, **kwargs):
+    if state.oob.violation: return 'oob_violation'
+    return simgr.filter(state, **kwargs)
+
+class SpectreViolationFilter(angr.exploration_techniques.ExplorationTechnique):
+  def __init__(self):
+    super().__init__()
+
+  def filter(self, simgr, state, **kwargs):
+    if state.spectre.violation: return 'spectre_violation'
+    return simgr.filter(state, **kwargs)
+
+def runSpec(s):
+    proj,state = kocher(s)
+    armSpectreChecks(proj,state)
+    makeSpeculative(proj,state)
+    return runState(proj,state)
+
+def runNotSpec(s):
+    proj,state = kocher(s)
+    armSpectreChecks(proj,state)
+    return runState(proj,state)
+
+def run11Spec(s):
+    proj,state = kocher11(s)
+    armSpectreChecks(proj,state)
+    makeSpeculative(proj,state)
+    return runState(proj,state)
+
+def run11NotSpec(s):
+    proj,state = kocher11(s)
+    armSpectreChecks(proj,state)
+    return runState(proj,state)
+
+def runallSpec():
+    return unionDicts(
+      {s:runSpec(s) for s in ['01','02','03','04','05','06','07','08','09','10','12','13','14','15']},
+      {('11'+s):run11Spec(s) for s in ['gcc','ker','sub']})
+
+def runallNotSpec():
+    return unionDicts(
+      {s:runNotSpec(s) for s in ['01','02','03','04','05','06','07','08','09','10','12','13','14','15']},
+      {('11'+s):run11NotSpec(s) for s in ['gcc','ker','sub']})
+
+def alltests():
+    notspec = runallNotSpec()
+    spec = runallSpec()
+    def violationDetected(simgr):
+        return 'spectre_violation' in simgr.stashes and len(simgr.spectre_violation) > 0
+    def testResult(s):
+        return ("FAIL: detected a violation without speculative execution" if violationDetected(notspec[s])
+            else "FAIL: no violation detected" if not violationDetected(spec[s])
+            else "PASS")
+    return {k:testResult(k) for k in spec.keys()}
+
+def unionDicts(dicta, dictb):
+    return {**dicta, **dictb}  # requires Python 3.5+
+
+if __name__ == '__main__':
+    from pprint import pprint
+    pprint(alltests())

oob.py

@@ -0,0 +1,123 @@
+import angr
+import claripy
+
+import logging
+l = logging.getLogger(name=__name__)
+
+class OOBState(angr.SimStatePlugin):
+    """
+    State tracking for crudely marking what is determined 'in-bounds'.
+    If you 'arm' it, it reports any potential memory read/write to any area not marked 'in-bounds'.
+
+    This 'in-bounds' determination is not used by the Spectre checker (which
+    relies on uninitialized memory for the initial 'secret' determination, then a
+    form of taint tracking), but it is used by the OOB concretization strategy below
+    (which both OOB and Spectre checking rely on). However, the Spectre checker doesn't
+    need/want the OOB state to be 'armed'.
+    """
+
+    def __init__(self, proj=None, inbounds_intervals=None, armed=False):
+        """
+        Either 'proj' or 'inbounds_intervals' must not be None. Initial inbounds intervals
+        will be taken from 'proj', or else from the explicit 'inbounds_intervals' if 'proj' is None.
+        """
+        super().__init__()
+        if proj is None:
+            self.inbounds_intervals = inbounds_intervals
+        else:
+            self.inbounds_intervals = [(obj.min_addr, obj.max_addr) for obj in proj.loader.all_objects]
+              # this is an overapproximation of what is in-bounds: everything that is mapped is in-bounds.
+              # the analysis then tells us if we can leak the value of things that are "not mapped".
+              # of course, we separately need to account for when more memory is allocated, for instance
+              # malloc() or when the stack is expanded (??)
+        self._armed = armed
+        self.violation = None
+
+    @angr.SimStatePlugin.memo
+    def copy(self, memo):
+        return OOBState(inbounds_intervals=self.inbounds_intervals, armed=self._armed)
+
+    def arm(self, state):
+        """
+        Setup hooks and breakpoints to perform bounds tracking.
+        Also set up concretization to ensure addresses are always made to be OOB when possible.
+        """
+        state.inspect.b('mem_read',  when=angr.BP_AFTER, condition=_read_is_oob, action=detected_oob_read)
+        state.inspect.b('mem_write', when=angr.BP_AFTER, condition=_write_is_oob, action=detected_oob_write)
+
+        state.memory.read_strategies.insert(0, OOBStrategy())
+        state.memory.write_strategies.insert(0, OOBStrategy())
+
+        state.options.add(angr.options.SYMBOLIC_WRITE_ADDRESSES)
+
+        self._armed = True
+
+    def armed(self):
+        """
+        Has arm() been called?
+        """
+        return self._armed
+
+# Call during a breakpoint callback on 'mem_read'
+def _read_is_oob(state):
+    addr = state.inspect.mem_read_address
+    length = state.inspect.mem_read_length
+    return _is_oob(state, addr, length)
+
+# Call during a breakpoint callback on 'mem_write'
+def _write_is_oob(state):
+    addr = state.inspect.mem_write_address
+    length = state.inspect.mem_write_length
+    return _is_oob(state, addr, length)
+
+def _is_oob(state, addr, length):
+    l.debug("checking if {} is oob".format(addr))
+    inbounds_intervals = state.oob.inbounds_intervals + [get_stack_interval(state)]
+    oob_constraints = [claripy.Or(addr < mn, addr+length > mx) for (mn,mx) in inbounds_intervals]
+    if state.solver.satisfiable(extra_constraints=oob_constraints): return True  # there is a solution to current constraints such that the access is OOB
+    #l.debug("inbounds: {} >= {} and {} <= {}".format(addr, hexprint(mn), addr+length, hexprint(mx)))  # when you also take into account all the current constraints
+    return False  # operation must be inbounds
+
+def get_stack_interval(state):
+    sp = state.regs.rsp
+    end_of_stack = 0x7fffffffffffffff  # this is an assumption, but I think a good one for ELF programs
+    return (sp, end_of_stack)
+
+# print a claripy AST as-is, or if it's a Python int, print in hex
+def hexprint(val):
+    if isinstance(val, claripy.Base): return "{}".format(val)
+    else: return "0x{:02X}".format(val)
+
+def detected_oob_read(state):
+    print("\n!!!!!!!! OUT-OF-BOUNDS READ !!!!!!!!\n  Address {}\n  Value {}\n  x={}\n  constraints were {}\n".format(
+        state.inspect.mem_read_address, state.inspect.mem_read_expr, state.globals['arg'], state.solver.constraints))
+    state.oob.violation = (state.inspect.mem_read_address, state.inspect.mem_read_expr)
+
+def detected_oob_write(state):
+    print("\n!!!!!!!! OUT-OF-BOUNDS WRITE !!!!!!!!\n  Address {}\n  Value {}\n  x={}\n  constraints were {}\n".format(
+        state.inspect.mem_write_address, state.inspect.mem_write_expr, state.globals['arg'], state.solver.constraints))
+    state.oob.violation = (state.inspect.mem_write_address, state.inspect.mem_write_expr)
+
+class OOBStrategy(angr.concretization_strategies.SimConcretizationStrategy):
+    """
+    Concretization strategy which attempts to resolve every address to
+    somewhere *outside* of bounds (as determined by the OOBState state
+    plugin). See notes on superclass (and other subclasses) for more info on
+    what's happening here.
+    """
+
+    def __init__(self, **kwargs):
+        super().__init__(**kwargs)
+
+    def _concretize(self, memory, addr):
+        """
+        Attempts to resolve the address to a value *outside* all of the in-bounds
+        intervals if possible.
+        Else, defers to fallback strategies.
+        """
+        try:
+            constraints = [memory.state.solver.Or(addr < mn, addr >= mx) for (mn, mx) in memory.state.oob.inbounds_intervals]
+            return [ self._any(memory, addr, extra_constraints=constraints) ]
+        except angr.errors.SimUnsatError:
+            # no solution
+            return None

specmem.py

@@ -0,0 +1,3 @@
+import angr
+
+import collections

specstate.py

@@ -0,0 +1,14 @@
+#include <string.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+unsigned int array1_size = 16;
+uint8_t array1[16] = { 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16 };
+uint8_t array2[256 * 512];
+uint8_t temp = 0; /* Used so compiler won't optimize out victim_function() */
+
+void victim_function_v01(size_t x) {
+     if (x < array1_size) {
+          temp &= array2[array1[x] * 512];
+     }
+}

spectector-clang/01.c

@@ -0,0 +1,15 @@
+#include <string.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+unsigned int array1_size = 16;
+uint8_t array1[16] = { 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16 };
+uint8_t array2[256 * 512];
+uint8_t temp = 0; /* Used so compiler won't optimize out victim_function() */
+
+void leakByteLocalFunction(uint8_t k) { temp &= array2[(k)* 512]; }
+void victim_function_v02(size_t x) {
+     if (x < array1_size) {
+       leakByteLocalFunction(array1[x]);
+     }
+}

spectector-clang/01.o

@@ -0,0 +1,14 @@
+#include <string.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+unsigned int array1_size = 16;
+uint8_t array1[16] = { 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16 };
+uint8_t array2[256 * 512];
+uint8_t temp = 0; /* Used so compiler won't optimize out victim_function() */
+
+__declspec(noinline) void leakByteNoinlineFunction(uint8_t k) { temp &= array2[(k)* 512]; }
+void victim_function_v03(size_t x) {
+     if (x < array1_size)
+          leakByteNoinlineFunction(array1[x]);
+}

spectector-clang/02.c

@@ -0,0 +1,13 @@
+#include <string.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+unsigned int array1_size = 16;
+uint8_t array1[16] = { 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16 };
+uint8_t array2[256 * 512];
+uint8_t temp = 0; /* Used so compiler won't optimize out victim_function() */
+
+void victim_function_v04(size_t x) {
+  if (x < array1_size)
+    temp &= array2[array1[x << 1] * 512];
+}

spectector-clang/02.o

@@ -0,0 +1,27 @@
+#include <string.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+unsigned int array1_size = 16;
+uint8_t array1[16] = { 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16 };
+uint8_t array2[256 * 512];
+uint8_t temp = 0; /* Used so compiler won't optimize out victim_function() */
+
+// void victim_function_v05(size_t x) {
+//   int i;
+//   if (x < array1_size) {
+//     for (i = x - 1; i >= 0; i--)
+//       temp &= array2[array1[i] * 512];
+//   }
+// }
+
+// Patched version using signed integers (passing MIN_INT as argument
+// have problems due to an integer underflow in i=x-1). Spectector
+// X86->muAasm does not support unsigned arithmetic yet.
+void victim_function_v05(long x) {
+  int i;
+  if (x >=0 && x < array1_size) {
+    for (i = x - 1; i >= 0; i--)
+      temp &= array2[array1[i] * 512];
+  }
+}

spectector-clang/03.c

@@ -0,0 +1,16 @@
+#include <string.h>
+#include <stdlib.h>
+#include <stdint.h>
+
+unsigned int array1_size = 16;
+uint8_t array1[16] = { 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16 };
+uint8_t array2[256 * 512];
+uint8_t temp = 0; /* Used so compiler won't optimize out victim_function() */
+
+void victim_function_v05(size_t x) {
+  int i;
+  if (x < array1_size) {
+    for (i = x - 1; i >= 0; i--)
+      temp &= array2[array1[i] * 512];
+  }
+}