1. Installation

This section explains the necessary steps to install and build BINSEC tool and BINSEC/Codex tool extension on a Linux System.

1.1. Prerequisites

The usual development tools (i.e. make, gcc, g++, …) as well as some C libraries are required:

• Debian 10 / Ubuntu 20.04:

  sudo apt-get install build-essential git autoconf m4 unzip python-dev libzmq3-dev libgmp-dev llvm-dev cmake protobuf-compiler z3
  

• Ubuntu 18.04:

  sudo apt-get install build-essential git autoconf m4 unzip python-dev libzmq3-dev libgmp-dev llvm-7-dev cmake protobuf-compiler z3
  

Furthermore, the OCaml package manager OPAM is required:

• Either install it from the system’s package manager …:

  • Debian 10 / Ubuntu 20.04: sudo apt-get install opam

• … or get a binary release from GitHub:

  wget https://github.com/ocaml/opam/releases/download/2.0.8/opam-2.0.8-x86_64-linux
  sudo install -v -m755 -o root -g root opam-2.0.8-x86_64-linux /usr/local/bin/opam
  

Finally, OPAM has to be initialized in the current user account:

opam init

If inside chroot, it may be necessary to add option --disable-sandboxing.

If behind a proxy, it may be necessary to add a line proxy= <proxy_url>:<proxy_port> (e.g. proxy= proxy.cs.hs-rm.de:8080) to file ~/.curlrc.

This will create a directory named .opam in your home directory and ask for permission to modify your ~/.profile. If you allow it to do so, the opam environment will be initialized each time you log into the system. Otherwise, it may be necessary to enter:

eval $(opam env)

each time you want to use opam.

1.2. Downloading the source code

The original source code is available from the BINSEC developer’s Github project:

git clone https://github.com/binsec/binsec.git

The BINSEC/Codex extension source code is also available from the BINSEC developer’s Github project (also includes BINSEC):

git clone https://github.com/binsec/rtas2021_artifact

To enable local development though, we are using our own forks of BINSEC and BINSEC/Codex on GitLAB respectively:

git clone git@gitlab.cs.hs-rm.de:trexor/extern/binsec.git
git clone git@gitlab.cs.hs-rm.de:trexor/projects/rtas2021_artifact.git

After this, you should have a local directories named binsec and/or rtas2021_artifact containing all necessary code.

1.3. Building BINSEC/Codex

BINSEC and BINSEC/Codex can be built either with the traditional autotools, or directly by OPAM. In the steps shown below, opam is preferred, because of its ability to resolve and install all ocaml dependencies on the fly.

• BINSEC

cd to the just checked-out binsec Directory and enter:

opam install --unlock-base ./binsec.opam llvm=7.0.0

Where

• --unlock-base allows opam to change the ocaml version

• llvm=7.0.0 forces a specific version of llvm, e.g. Debian 10 only ships version 7

This may take a while: Several packages will be installed in the process. Eventually, the binsec binary should exist in the hidden opam directory ~/.opam/default/bin/binsec, and should be available in the executable path.

• BINSEC/Codex

  The Codex extension is based upon libase library, that should also be installed from the local directory. Installation of libase should be executed only once, so the opam package manager remains the source code path.

cd to the checked-out rtas2021_artifact Directory and enter:

opam install libase/libase.opam
opam install --unlock-base binsec/binsec.opam

Again, unlock-base allows opam to change the ocaml version.

The BINSEC and BINSEC/Codex installation can be tested as follows:

binsec --help

2. First Steps

2.1. Translating Code to DBA

BINSEC uses DBA (Dynamic Bitvector Automata) as a intermediate representation. To translate some opcode of a specific ISA into a DBA program, BINSEC can be invoked with the option disasm:

$ binsec disasm -isa x86 -disasm-decode 0416

[disasm:result] 04 16 / add al, 0x16
               0: res8<8> := (22<8> + eax<32>{0,7});
               1: OF<1> :=
                   ((eax<32>{7} = 0<1>) & (eax<32>{7} != res8<8>{7}));
               2: SF<1> := (res8<8> <s 0<8>);
               3: ZF<1> := (res8<8> = 0<8>);
               4: AF<1> := (6<5> + (extu eax<32>{0,3} 5)){4};
               5: PF<1> :=                     !
                   ((((((((res8<8>{0} ^ res8<8>{1}) ^ res8<8>{2}) ^
                         res8<8>{3}) ^ res8<8>{4}) ^ res8<8>{5}) ^
                      res8<8>{6}) ^ res8<8>{7}));
               6: CF<1> := (22<9> + (extu eax<32>{0,7} 9)){8};
               7: eax<32>{0, 7} := res8<8>;
               8: goto (00000002, 0)

In this example the x86 opcode 0416 is decoded to add al, 0x16 and then translated to DBA. With the option -isa the ISA can be set to x86, arm32 or riscv. Additionally the output can be saved into a file out.dba with the parameter -disasm-o-dba.

Note

There should be some basic explanation here as to the meaning of the above DBA code, plus a link to some documentation about DBA.

To disassemble a binary file the parameter -file can be set like this:

$ gcc -m32 main.c
$ binsec disasm -isa x86 -disasm-o-dba out.dba -file a.out

Note

This works for x86, however if try this for arm32, i get:

[disasm:info] Running disassembly
[disasm:result] Entry points:
[disasm:info] Starting from default entry point 000003f4
[disasm:info] Using section until 633
[disasm:result] Linear disassembly from 000003f4 to 00000633
/bin/sh: 1: unisim-armsec: not found
[arm:error] Probable parse error at line 1, column 0
Lexeme was:
Entry was:
Getting basic infos only ...

2.2. educRTOS verification

rtas2021_artifact repository contains the educrtos source code directory for the small OS kernel that will be used to demonstrate the verification tool.

For the compilation process the 32-Bit support is required. Therefore the following package should be installed:

sudo apt-get install gcc-multilib

2.2.1. Verification using nix-shell

The Artifact verification procedure makes use of the nix-shell command which is part of NixOS, a Linux distribution on its own right. It is possible to install nix-shell in, e.g. a Debian or Ubuntu system as is explained here:

sh <(curl -L https://nixos.org/nix/install) --daemon

Note

This is a rather invasive process, installing several packages on the system, regardless of whether or not the system may already have them. The web site also has information on how to undo things and remove Nix completely.

After this, the artifact verification can be run from the root directory of the artifact:

nix-shell
make <target>

Where <target> is one of rq0, rq3, rq3_noprint or rq4and5_<n>:

• rq0: Soundness check: Show that analysis fails to verify APE and ARTE when the kernel is vulnerable or buggy.

• rq3: Genericity: Show that method applies on different kernels, hardware architectures and toolchains.

• rq3_noprint: Like rq3, but less output and thus faster

• rq4and5_<n>: Automation ans scalability: show that APE and ARTE in OS kernels can be proven fully automatically and that the method scales to large numbers of tasks (<n> = number of tasks)

2.2.2. Verification not using nix-shell

In the source code directory there is a config.mk file that contains the necessary compilation options like compiler, scheduler and so on. The unused options should be commented out or alternativelly set up from the command line. For example the usage of Round-Robin scheduler could be defined with following:

export SCHEDULER=ROUND_ROBIN_SCHEDULING

After that the compilation is initiated with simple make command:

make clean && make system_${ntasks}tasks.exe

Where $ntasks defines a number of tasks and supports only one of the followings: 1, 2, 5, 10, 50, 100, 500, 1000, 2000, 5000, 10000, 100000

If this results in an error saying “not enough room for program headers”, edit file user_task.ld, adding the following lines:

PHDRS
{
  text PT_LOAD ;
}

Also, add : text to the end of the SECTIONS statement in the same file, like so;

SECTIONS
{
      .....
} : text

Note

This change has been tested in the nix-shell environment. It does not seem to break anything, so it should be safe to apply generally.

The verification process should be executed from the root directory. The chosen compilation options should also be taken into account while verifying.

binsec -config educrtos/binsec.ini $exe -codex-x86-types $scheduling $shape_arg -codex-nb-tasks $ntasks $dyn_thread_arg -codex-debug_level $debug_level

• $exe: executable e.g. educrtos/system_10tasks.exe

• $scheduling: scheduling parameter

  • rr: Round-Robin scheduler (SCHEDULER=ROUND_ROBIN_SCHEDULING)

  • fp: Fixed-Priority scheduler (SCHEDULER=FP_SCHEDULING)

  • edf: Earliest-Deadline-First scheduler (SCHEDULER=EDF_SCHEDULING)

• $shape_arg: TODO: -codex-no-use-shape or empty

• $ntasks: number of tasks (same that was used during compilation process)

• $dyn_thread_arg: usage of dynamic tasks

  • empty: (DYNAMIC_TASK_CREATION=yes)

  • -codex-no-dyn-threads: (DYNAMIC_TASK_CREATEN=no)

• $debug_level: debug level (from 0 up to 3 can be chosen)

After verification process the following control-flow-graphs are automatically generated: handler_cpu0.dot, init_conrete_cpu0.dot, init_cpu0.dot. These dot files can be converted into post-script files with the dot tool:

dot -Tps <name>.dot -o <name>.ps

After conversion the post-script files can be seen by any post-script viewer like evince.

Note

So now that we have these nice diagrams, what can we see from them? Generally, some more information on how to read the binsec output is required here.