pycbat MVP

Dockerfile.min

@@ -0,0 +1,37 @@
+FROM ubuntu:20.04
+# Multi-stage docker build
+# Copying over only needed compiled objects from development docker to get CBAT to run
+# https://docs.docker.com/build/building/multi-stage/
+
+WORKDIR /root/
+# Bap cli binary
+COPY --from=cbat:latest /home/opam/.opam/4.14/bin/bap /home/opam/.opam/4.14/bin/bap 
+ENV PATH="$PATH:/home/opam/.opam/4.14/bin"
+
+# Plugins 
+COPY --from=cbat:latest /home/opam/.opam/4.14/lib/bap/*.plugin /home/opam/.opam/4.14/lib/bap/
+# Removing some unneeded larger plugins mostly related to primus
+RUN rm /home/opam/.opam/4.14/lib/bap/primus* \
+    /home/opam/.opam/4.14/lib/bap/beagle.plugin \
+    /home/opam/.opam/4.14/lib/bap/run.plugin \
+    /home/opam/.opam/4.14/lib/bap/constant_tracker.plugin
+# Do we need this? /home/opam/.opam/4.14/lib/bap/frontc_parser.plugin \
+
+COPY --from=cbat:latest /home/opam/.opam/4.14/lib/bap/primus_lisp.plugin /home/opam/.opam/4.14/lib/bap/
+
+# Some primus semantics
+COPY --from=cbat:latest /home/opam/.opam/4.14/share/bap/primus/  /home/opam/.opam/4.14/share/bap/primus/
+
+# Get Z3 library
+COPY --from=cbat:latest /home/opam/.opam/4.14/lib/stublibs/libz3.so /home/opam/.opam/4.14/lib/stublibs/libz3.so
+
+# Objdump and Objdump dependencies
+COPY --from=cbat:latest /usr/bin/objdump /usr/bin/objdump
+COPY --from=cbat:latest /lib/x86_64-linux-gnu/libopcodes-2.34-multiarch.so /lib/x86_64-linux-gnu/libopcodes-2.34-multiarch.so
+COPY --from=cbat:latest /lib/x86_64-linux-gnu/libbfd-2.34-multiarch.so /lib/x86_64-linux-gnu/libbfd-2.34-multiarch.so
+COPY --from=cbat:latest /lib/x86_64-linux-gnu/libctf-multiarch.so.0 /lib/x86_64-linux-gnu/libctf-multiarch.so.0
+
+# Removing unneeded bytecode .cma from plugins 
+COPY --from=cbat:latest  /usr/bin/zip  /usr/bin/zip
+RUN  for file in /home/opam/.opam/4.14/lib/bap/*.plugin; do zip --delete $file "*.cma"; done
+RUN rm /usr/bin/zip

wp/pycbat/.gitignore

@@ -0,0 +1,2 @@
+__pycache__
+.pytest_cache

wp/pycbat/README.md

@@ -0,0 +1,23 @@
+# CBAT Python Bindings
+
+<https://github.com/draperlaboratory/cbat_tools>
+
+
+Installation
+```
+docker pull philzook58/cbat_min
+python3 -m pip install -e .
+```
+
+Usage:
+
+```python
+import z3
+import cbat
+
+rax = z3.BitVec("RAX", 64)
+postcond = rax == 4
+# Check that rax is always 4 at end of function "fact" in binary file myfactorial.o
+cbat.run_wp("./myfactorial.o", func="fact", postcond=postcond)
+```
+

wp/pycbat/pyproject.toml

@@ -0,0 +1,21 @@
+[build-system]
+requires = ["hatchling"]
+build-backend = "hatchling.build"
+
+[project]
+name = "cbat"
+version = "0.0.1"
+authors = [
+  { name="Philip Zucker", email="[email protected]" },
+]
+description = "Comparative Binary Analysis Tool"
+readme = "README.md"
+requires-python = ">=3.7"
+classifiers = [
+    "Programming Language :: Python :: 3",
+    "License :: OSI Approved :: MIT License",
+    "Operating System :: OS Independent",
+]
+
+[project.urls]
+"Homepage" = "https://github.com/draperlaboratory/cbat_tools"

wp/pycbat/requirements.txt

@@ -0,0 +1,3 @@
+z3
+docker
+

wp/pycbat/src/cbat/__init__.py

@@ -0,0 +1,50 @@
+import subprocess
+import z3
+
+
+def run_wp(filename, filename2=None,  func="main", invariants=[], debug=False, precond=None, postcond=None, docker_image=None, **kwargs):
+    cmd = ["bap", "wp", "--no-cache",
+           "--show", "precond-smtlib", "--func", func]
+    if precond != None:
+        cmd.append("--precond")
+        cmd.append("(assert " + precond.sexpr() + ")")
+    if postcond != None:
+        cmd.append("--postcond")
+        cmd.append("(assert " + postcond.sexpr() + ")")
+    # TODO: Fill out invariants
+
+    # forward kwargs. Typo unfriendly
+    # TODO: fill out other allowed flags
+    flags = ["check-invalid-derefs", "check-null-derefs"]
+    assert all(k in flags for k in kwargs.keys()), kwargs
+    cmd += [f"--{k}" for k,
+            v in kwargs.items() if v == True and k in flags]
+
+    cmd.append(filename)
+    if filename2 != None:
+        cmd.append(filename2)
+
+    if docker_image != None:
+        flags = ["-v", f"{filename}:{filename}"]
+        if filename2 != None:
+            flags += ["-v", f"{filename2}:{filename2}"]
+        cmd = ["docker", "run"] + flags + [docker_image] + cmd
+    res = subprocess.run(cmd, check=False, capture_output=True)
+    if debug:
+        print(res.stderr)
+    smt = res.stdout.decode().split("Z3 :")
+    if len(smt) != 2:
+        print("SMT formula extraction failed", smt)
+        print(res.stderr)
+        assert False
+    smtlib = smt[1]
+    s = z3.Solver()
+    s.from_string(smtlib)
+    if debug:
+        print(s)
+    res = s.check()
+    if res == z3.unsat:
+        return (z3.unsat, s)
+    elif res == z3.sat:
+        # raise?
+        return (z3.sat, s)

wp/pycbat/src/cbat/helpers.py

@@ -0,0 +1,118 @@
+import z3
+import angr
+from . import run_wp
+
+
+class TypedView():
+    def __init__(self, value: z3.BitVecRef, typ: angr.sim_type.SimType, le=True, mem=None):
+        self.mem = mem
+        self.value = value
+        self.typ = typ
+        self.le = True
+
+    def deref(self):
+        assert self.mem != None
+        bytes = range(self.typ.size // 8)
+        if self.le:
+            bytes = reversed(bytes)
+        value = z3.Concat([self.mem[self.value + n] for n in bytes])
+        return TypedView(value, self.typ.pts_to, le=self.le, mem=self.mem)
+
+    def __getitem__(self, field):
+        start = self.typ.offsets[field]
+        end = start + self.typ.fields[field].size
+        value = z3.Extract(end-1, start, self.value)
+        return TypedView(value, self.typ.fields[field], mem=self.mem, le=self.le)
+
+    def __add__(self, b):
+        if isinstance(b, int):
+            return TypedView(self.value + b, self.typ, mem=self.mem, le=self.le)
+        elif isinstance(b, TypedView):
+            assert b.typ == self.typ and self.mem == b.mem and self.le == b.le
+            return TypedView(self.value + b.value, self.typ, mem=self.mem, le=self.le)
+        assert False, "Unexpected addition type"
+
+    def __eq__(self, b):
+        assert self.typ == b.typ
+        return self.value == b.value
+
+    def __repr__(self):
+        return f"({repr(self.typ)}){repr(self.value)}"
+
+
+def make_mem(name):
+    return z3.Array(name, z3.BitVecSort(64), z3.BitVecSort(8))
+
+
+class PropertyBuilder():
+    def __init__(self, binary=None, binary2=None, func=None, headers=None):
+        self.binary = binary
+        self.binary2 = binary2
+        self.func = func
+        if binary != None:
+            self.load_binary(binary)
+        if headers != None:
+            self.load_headers(headers)
+        self.posts = []
+
+        self.mem = make_mem("mem")
+        self.init_mem = make_mem("init_mem")
+        self.mem0 = make_mem("mem0")
+        self.init_mem0 = make_mem("init_mem0")
+
+    def load_binary(self, filename):
+        self.proj = angr.Project(filename, load_debug_info=True)
+        self.cc = self.proj.factory.cc()
+
+    def load_headers(self, header_str):
+        (defns, types) = angr.types.parse_file(header_str)
+        angr.types.register_types(types)
+        self.defns = defns
+
+    def cast(self, value, typ, prefix="", suffix=""):
+        mem = make_mem(prefix+"mem"+suffix)
+        le = self.proj.arch.memory_endness == 'Iend_LE'
+        value = z3.Extract(typ.size - 1, 0, value)
+        return TypedView(value, typ, le=le, mem=mem)
+
+    def fun_args(self, prefix="", suffix=""):
+        assert self.func != None
+        funsig = self.defns[self.func]
+        funsig = funsig.with_arch(self.proj.arch)
+        # stack args not supported yet
+        assert len(funsig.args) <= len(self.cc.ARG_REGS)
+        return [self.cast(z3.BitVec(prefix + reg.upper() + suffix, 64), typ, prefix=prefix, suffix=suffix) for typ, reg in zip(funsig.args, self.cc.ARG_REGS)]
+
+    def init_fun_args(self):
+        return self.fun_args(prefix="init_")
+
+    def init_fun_args_mod(self):
+        return self.fun_args(prefix="init_", suffix="_mod")
+
+    def fun_args_mod(self):
+        return self.fun_args(suffix="_mod")
+
+    def init_fun_args_orig(self):
+        return self.fun_args(prefix="init_", suffix="_orig")
+
+    def fun_args_orig(self):
+        return self.fun_args(suffix="_orig")
+
+    def ret_val(self, suffix=""):
+        assert self.func != None
+        funsig = self.defns[self.func]
+        funsig = funsig.with_arch(self.proj.arch)
+        reg = self.cc.RETURN_VAL.reg_name
+        return self.cast(z3.BitVec(reg.upper() + suffix, 64), funsig.returnty)
+
+    def ret_val_orig(self):
+        return self.ret_val(suffix="_orig")
+
+    def ret_val_mod(self):
+        return self.ret_val(suffix="_mod")
+
+    def add_post(self, post):
+        self.posts.append(post)
+
+    def run_wp(self):
+        return run_wp(self.binary, func=self.func, filename2=self.binary2, postcond=z3.And(self.posts))

wp/pycbat/tests/resources/Makefile

@@ -0,0 +1,4 @@
+
+test6: test6_1.c test6_2.c
+	gcc -O1 -c test6_1.c -o test6_1.o
+	gcc -O1 -c test6_2.c -o test6_2.o

wp/pycbat/tests/resources/test4.c

@@ -0,0 +1,6 @@
+int foo(int x, char y)
+{
+    int bar;
+    bar = x;
+    return 3 + bar;
+}

wp/pycbat/tests/resources/test5.c

@@ -0,0 +1,12 @@
+typedef struct mystruct
+{
+    int f1;
+    char f2;
+} mystruct;
+
+int foo(mystruct *x, char y)
+{
+    int bar;
+    bar = x->f1;
+    return 3 + bar;
+}

wp/pycbat/tests/resources/test6_1.c

@@ -0,0 +1,4 @@
+int foo(int x)
+{
+    return x + 3;
+}

wp/pycbat/tests/resources/test6_2.c

@@ -0,0 +1,4 @@
+int foo(int x)
+{
+    return x + 4;
+}