bincaml

lightweight binary exploration verification project implemented in ocaml.

status: very early stages work-in progress.

Cloning

The examples exist in a submodule, to clone these:

git clone --recurse-submodules https://github.com/agle/bincaml.git --shallow-submodules

If you have already cloned you can fetch the submodule with:

git submodule update --init --depth 1

If you are developing with SSH git access, update the examples remote to make uplaoding examples easier

cd examples && git remote set-url origin git@github.com:UQ-PAC/bincaml-test.git

Setup

Supports Linux (at least amd64) and MacOS (arm64) with OCaml 5.4.1. Windows is explicitly not supported outside of WSL.

• enable frame pointers on opam switch for performance recording

• enable flambda for compiler optimisation (for release build only)

• ensure pac opam repository is installed

• Tests require smt solver CVC5 installed.

opam switch create bincaml ocaml-variants.5.4.1+options ocaml-option-flambda ocaml-option-fp
opam repository add pac https://github.com/uq-pac/opam-repository.git
opam install --deps-only --with-doc --with-test .
dune build

On MacOS ensure your environment allows linking against homebrew, e.g. in .bashrc

export LIBRARY_PATH=$LIBRARY_PATH:/opt/homebrew/lib/

Example

bincaml analyses il files produced by basil. scripts (in addition to cli) are used to drive the tool, for example:

; test.s
(load-il "examples/cntlm-simp-output.il")
(dump-il "before.il")
(run-transforms "cf-expressions" "intra-dead-store-elim")
(dump-il "after.il")

$ dune exec bincaml script test.s
$ diff before.il after.il | head
50d49
<       var R30_begin_p9main_4198208:bv64 := $R30:bv64;
55d53
<       var var1_4198208_bv64:bv64 := 0x0:bv64;
65,66c63
<       var var1_4198220_bv64:bv64 := 0x0:bv64;
<       $R29:bv64 := bvadd($R31:bv64, 0x0:bv64);
---
>       $R29:bv64 := $R31:bv64;
68,69d64