This repository serves as a mirror for the source code of Codex. Codex is two things:

• Codex semantics Library: An OCaml library to write static analysers based on abstract interpretation;
• Sound static analysers based on this library. Two are currently available:
  • BINSEC/Codex : An analyzer for machine code using BINSEC as a front-end.
  • Frama-C/Codex : An analyzer for C using Frama-C as its front-end.

Codex has notably been used for automated verification of security properties of a whole embedded kernels directly from its binary executable [RTAS’21], to verify the absence of spatial memory corruption in challenging code manipulating data structure libraries [VMCAI’22]. The structure of the analysis is based on the relational composition of expressions, and we are in the early stages of establishing its theoretical foundations, as detailed in [POPL’23].

[RTAS’21]

No Crash, No Exploit: Automated Verification of Embedded Kernels. O. Nicole, M. Lemerre, S. Bardin, X. Rival (Best paper)

[VMCAI’22]

Lightweight Shape Analysis based on Physical Types, O. Nicole, M. Lemerre, X. Rival

[POPL’23]

SSA Translation Is an Abstract Interpretation, M. Lemerre (Distinguished paper).

The repository example contains the results of a simple program (computing the absolute value of an integer) in both C and machine code analysis. The results of the analysis can be presented as a standalone html file, that you can find for the C analysis here. The binary analysis example (here) analyses the machine code version of same file, but is also given a type specification (which can be found here) that restricts the possible values at the start of the program to be in some interval.

Codex is capable of handling much more than these simple examples! We will soon provide tutorials to help you perform your own analyses, but you can already try Codex by replacing these examples by your own code.

This is our first beta release, not intended to be a plug-and-play static analysis tool. The theory is sound and the tool has been used in several important case studies, but please be aware of the current lack of comprehensive documentation or polished user interface. Codex is rapidly evolving and the interface of some internal components and command line options may also change in the future. If you are require assistance, feel free to reach out (matthieu dot lemerre at cea dot fr).

We have now entered a phase where the primary objective is to enhance the tool’s usability beyond our internal team, so anticipate forthcoming improvements in user-friendliness and updates to the documentation.

Additionally, with this release, we aim to initiate the exportation of abstract interpretation components that may prove beneficial to other static analysis developers. We welcome feedback to aid us in refining and enhancing the tool.

The simplest way to try Binsec/Codex and Frama-C/Codex is to download the compiled version. It should work on any platform supporting the execution of x86-64bit linux executables (including WSL).

Codex should build without any issues on macOS, both x86 and ARM; however, macOS builds are not part of our continuous integration, and thus feature parity with Linux is not guaranteed.

(note that framac_codex.exe is a stripped version of Frama-C, with no plugins and support for compiler builtins removed)

1. Install opam, OCaml’s package manager.

   $ apt install unzip bubblewrap git build-essential # opam dependencies
   $ bash -c "sh <(curl -fsSL https://opam.ocaml.org/install.sh)"
   $ opam init --bare
       

   I recommend answering y to all questions opam asks.

2. Install Codex’s external dependencies

   $ apt install bc libgmp-dev liblmdb-dev \
       pkg-config autoconf graphviz libexpat1-dev zlib1g-dev libcairo2-dev \
       libexpat1-dev libgtk-3-dev libgtksourceview-3.0-dev libgnomecanvas2-dev \
       cmake time z3 gcc-multilib libev-dev libssl-dev \
       npm curl
       

3. Create a new opam switch with OCaml 4.14.2 for codex

   $ opam switch create codex ocaml-base-compiler.4.14.2
   $ eval $(opam env --switch=codex)
       

4. If you simply want to use codex, simply run

   $ opam install .
       

   which will install all dependencies and the packages. You can now use Codex using the following commands

   $ frama-c -codex # Frama-C/Codex, use -codex-h to display CLI options
   $ binsec_codex # Binsec/Codex, use -codex-h to display CLI options
       

   However, if you also want to be able to change the code, you should instead run

   $ opam install . --with-test --deps-only # install dependencies
   $ dune build # Build codex, re-run after any change
       

   You can then run Codex with

   $ dune exec -- frama-c -codex # Frama-C/Codex, use -codex-h to display CLI options
   $ dune exec -- binsec_codex # Binsec/Codex, use -codex-h to display CLI options
       

   (Or, run dune install and then access them directly with frama-c -codex).

Nix users can obtain a fully-fledged development environment with

$ nix develop ./devenv --impure

You can test that frama_c_codex is working by typing:

frama_c_codex -no-plugin-autoload -machdep x86_32 -codex test.c -codex-use-type-domain -codex-type-file frama-c/test.types  -codex-html-dump output.html

This should output an output.html with the results of the analysis, that you can inspect using your browser.

You can build the docker image with

$ docker build -t codex -f devenv/Dockerfile.debian .

(replace with Dockerfile.alpine for the alpine version).

You can then run the docker image with

$ docker run -it --rm --name codex_debian codex:debian

Additionally, one can use docker to build the binaries and them extract them out of the docker image (using docker copy) and use them locally.

We describe the structure of the library top-down:

binsec

The BINSEC/Codex plugin, doing binary code analysis using BINSEC as a frontend.

frama_c

The Frama-C/Codex plugin, doing C code analysis using Frama-C as a frontend.

codex

The main library, used to implement static analyses.

codex.fixpoint

Fixpoint engines (for forward flow-sensitive analyses).

codex.domains

Memory and numerical domains of Codex.

codex.types

Code used by the type-based abstract domains , e.g. parser or types

codex.single_value_abstraction

Non-relational abstraction of scalar values (e.g. interval, congruence, tristate/bitwise abstraction, etc.) including transfer functions.

codex.lattices

Lattices used in single_value_abstraction.

codex.terms

Symbolic expressions; this corresponds to the SSA expressions described in the “SSA Translation Is an Abstract Interpretation” POPL 2023 paper.

codex.smtbackend

Translating the SSA/Symbolic terms into a SMT formula for symbolic model-checking.

codex.operator

Definitions of basic operators (boolean operators like &&, arithmetic operators like +, etc.), syntax and semantics and their implementation in the concrete. The main module is Operator.Sig. Operator.Function_symbol allows building terms containing Codex expressions.

codex.codex_log

Logging facilities.

codex.codex_config

Compile-time configuration options.

utils

a collection of reusable datastructures and algorithms suitable to abstract interpretation, such as maps, sets etc. We are in the process of outsourcing some of them to make them more easily reusable.

ext

is a collection of code taken from other projects, and the place where we install the patched version of Frama-C.