Initial commitHEADmaster

1 files changed, 114 insertions, 0 deletions

diff --git a/prove.py b/prove.py
new file mode 100644
index 0000000..efff6da
--- /dev/null
+++ b/prove.py
@@ -0,0 +1,114 @@
+#!/usr/bin/env python3
+
+import sys
+import time
+import datetime
+import subprocess
+import multiprocessing
+import angr
+from claripy import *
+from claripy.backends.backend_z3 import claripy_solver_to_smt2
+
+proj = angr.Project(sys.argv[1])
+state = proj.factory.full_init_state()
+
+symbols = {
+    'fadd': { 'out': 4, 'f1': 4, 'f2': 4 },
+    'fsub': { 'out': 4, 'f1': 4, 'f2': 4 },
+    'fmul': { 'out': 4, 'f1': 4, 'f2': 4 },
+    'fmul2': { 'out': 8, 'f1': 8, 'f2': 8 },
+    'fmul_scalar': { 'out': 4, 'f1': 4, 'f2': 1 },
+    'fsqr': { 'out': 4, 'f1': 4 },
+    'fsqr2': { 'out': 8, 'f1': 8 },
+    'cswap2': { 'bit': 1, 'p1': 8, 'p2': 8 }
+}
+
+before = { }
+after = { }
+
+for symbol in symbols.items():
+    for var in symbol[1].items():
+        name = var[0] + '_' + symbol[0]
+        xaddr = proj.loader.find_symbol(name).rebased_addr
+        before[name] = [BVS('in_%s%u' % (name, i), 64) for i in range(var[1])]
+        for i in range(var[1]):
+            state.mem[xaddr + 8 * i].uint64_t = before[name][i]
+
+simgr = proj.factory.simgr(state)
+simgr.run()
+
+exits = simgr.deadended
+if len(simgr.errored) != 0:
+    print(simgr.errored)
+assert len(exits) == 1
+assert len(simgr.errored) == 0
+
+for symbol in symbols.items():
+    for var in symbol[1].items():
+        name = var[0] + '_' + symbol[0]
+        xaddr = proj.loader.find_symbol(name).rebased_addr
+        after[name] = []
+        for i in range(var[1]):
+            resolved = exits[0].mem[xaddr + 8 * i].uint64_t.resolved
+            after[name].append(resolved)
+
+def test_unsat(name, *constraints):
+    print("[?] Checking %s..." % name)
+    start = time.monotonic()
+    s = Solver()
+    for c in constraints:
+        s.add(c)
+    unsat = subprocess.run(
+        ["boolector", "--sat-engine-n-threads=%d" % multiprocessing.cpu_count(), "-SE", "cms", "-m", "-x", "-e", "--smt2"],
+        input=claripy_solver_to_smt2(s).encode()
+    ).returncode == 20
+    end = time.monotonic()
+    print("%s %s, elapsed: %s" % ("[+] Verified" if unsat else "[-] Falsified", name, str(datetime.timedelta(seconds=(end-start)))))
+    return unsat
+
+# Return a 512-bit number so that even multiplications won't overflow
+def combine_limbs(l):
+    return ZeroExt(512 - 256, Concat(l[3], l[2], l[1], l[0]))
+
+p = 2**255 - 19
+
+test_unsat("fadd",
+    (combine_limbs(before["f1_fadd"]) + combine_limbs(before["f2_fadd"])) % p != combine_limbs(after["out_fadd"])
+)
+test_unsat("fsub",
+    (3 * p + combine_limbs(before["f1_fsub"]) - combine_limbs(before["f2_fsub"])) % p != combine_limbs(after["out_fsub"])
+)
+test_unsat("fmul",
+    (combine_limbs(before["f1_fmul"]) * combine_limbs(before["f2_fmul"])) % p != combine_limbs(after["out_fmul"])
+)
+test_unsat("fmul2",
+    Or(
+        (combine_limbs(before["f1_fmul2"]) * combine_limbs(before["f2_fmul2"])) % p != combine_limbs(after["out_fmul2"]),
+        (combine_limbs(before["f1_fmul2"][4:]) * combine_limbs(before["f2_fmul2"][4:])) % p != combine_limbs(after["out_fmul2"][4:])
+    )
+)
+test_unsat("fmul_scalar",
+    (combine_limbs(before["f1_fmul_scalar"]) * ZeroExt(512 - 64, before["f2_fmul_scalar"][0])) % p != combine_limbs(after["out_fmul_scalar"]),
+    ULE(before["f2_fmul_scalar"][0], 2**17)
+)
+test_unsat("fsqr",
+    (combine_limbs(before["f1_fsqr"]) * combine_limbs(before["f1_fsqr"])) % p != combine_limbs(after["out_fsqr"])
+)
+test_unsat("fsqr2",
+    Or(
+        (combine_limbs(before["f1_fsqr2"]) * combine_limbs(before["f1_fsqr2"])) % p != combine_limbs(after["out_fsqr2"]),
+        (combine_limbs(before["f1_fsqr2"][4:]) * combine_limbs(before["f1_fsqr2"][4:])) % p != combine_limbs(after["out_fsqr2"][4:])
+    )
+)
+test_unsat("cswap2",
+    If(before["bit_cswap2"][0] == 0,
+        Or(
+            Concat(*before["p1_cswap2"]) != Concat(*after["p1_cswap2"]),
+            Concat(*before["p2_cswap2"]) != Concat(*after["p2_cswap2"])
+        ),
+        Or(
+            Concat(*before["p1_cswap2"]) != Concat(*after["p2_cswap2"]),
+            Concat(*before["p2_cswap2"]) != Concat(*after["p1_cswap2"])
+        )
+    )
+)