KO | EN

GitLite

Minimalist Open Source Repository Search Engine

gitlite — search

#typescript #ai-agents #developer-tools #cli #codex #claude-code #react #mcp #open-source #deepseek-harness #dsh-plugin #ai

Map2Check

★ 30 Open GitHub ↗

Map2Check: Finding Software Vulnerabilities

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

<h1>Map2Check</h1>
<h2>Finding Software Vulnerabilities using Symbolic Execution and Fuzzing</h3>

[![CI](https://github.com/hbgit/Map2Check/actions/workflows/ci.yml/badge.svg)](https://github.com/hbgit/Map2Check/actions/workflows/ci.yml)
[![OpenSSF Best Practices](https://www.bestpractices.dev/projects/3639/badge)](https://www.bestpractices.dev/projects/3639)
[![Gitter](https://badges.gitter.im/map2checkgit/community.svg)](https://gitter.im/map2checkgit/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge)

___

Map2Check is a bug hunting tool that automatically generates and checks safety properties in C programs and WebAssembly (WASM) binaries.
It tracks memory pointers and variable assignments to check user-specified assertions, overflow, and pointer safety.
The generation of the test cases is based on assertions (safety properties) from the code instructions, adopting the
[LLVM framework](http://llvm.org/) version 16, [LibFuzzer](https://llvm.org/docs/LibFuzzer.html), [KLEE](https://klee.github.io/) to generate input values to the test cases generated by Map2Check.

WASM verification works by lifting `.wasm` binaries to LLVM IR (via [WABT](https://github.com/WebAssembly/wabt)'s `wasm2c` + `clang-16`) and reusing the existing Map2Check instrumentation passes and the KLEE backend — see [Verifying WebAssembly (WASM) binaries](#verifying-webassembly-wasm-binaries).

Extra documentation is available at https://map2check.github.io

___

#### Requirements for using the tool

To use the Map2Check tool is necessary a Linux 64-bit OS system (Ubuntu 22.04 recommended). In the linux OS, you should install the requirements, typing the commands:
``` bash
$ sudo apt install python3 libc6-dev
```

Our binary tool is avaliable at https://github.com/hbgit/Map2Check/releases

#### Install Map2Check

In order to install Map2Check on your PC, you should download and save the map2check zip file on your disk from https://github.com/hbgit/Map2Check/releases.
After that, you should type the following command:

``` bash
$ unzip map2check-vx.y.2026-ii.jj.140ba2d2.zip
$ cd map2check-vx.y.2026-ii.jj.140ba2d2
```

Releases starting from **v8.0.0-Songbirds** include WebAssembly verification support (the `--wasm` option and the `lib/WasmRuntimeStubs.bc` runtime). Note that verifying `.wasm` inputs additionally requires WABT 1.0.41 and clang-16 installed on the host — see [Verifying WebAssembly (WASM) binaries](#verifying-webassembly-wasm-binaries). To generate a release layout yourself, build inside the Docker image and run `ninja install`: the self-contained distribution (binary, KLEE, instrumentation bitcode and WASM runtime) is produced in the `release/` directory.

#### Running the tool

Map2Check can be invoked through a standard command-line interface. Map2Check should be called
in the installation directory as follows:

``` bash
$ ./map2check --memtrack program.c
```

In this case, --memtrack is the option to check for memory errors. For help and others tool options:

``` bash
$ ./map2check --help
```

When you use a LLVM bytecode as input for the tool, be sure to add `-g` flag when generating the file, it is not required, but map2check will provide better info (like line numbers).

___

#### Verifying WebAssembly (WASM) binaries

##### Overview

Map2Check can verify third-party **`.wasm` binaries** (e.g. IoT/Edge modules) without access to their source code. Instead of implementing a dedicated WASM verification engine, Map2Check *lifts* the binary to LLVM IR and reuses its consolidated instrumentation passes and SMT-based backend:

```
.wasm ──▶ [1] Lifter: wasm2c (WABT) → C → clang-16 → LLVM IR
      ──▶ [2] Map2Check passes (WASM mode): linear-memory bounds checking,
              overflow and reachability instrumentation
      ──▶ [3] KLEE symbolic execution
      ──▶ [4] Result: TRUE / FALSE / UNKNOWN + witness
```

The analysis is **language-agnostic**: it instruments the elements common to every lifted module (the linear memory array and the `wasm_rt_*` runtime calls), so it works regardless of whether the `.wasm` was produced from C, Rust, Go, or AssemblyScript. Properties currently detected on WASM inputs:

| Property | Example CWEs | Status |
|:---|:---|:---|
| Linear-memory out-of-bounds access (bounds checking) | CWE-121/122/124/126/127 | ✅ Supported |
| Arithmetic overflow | CWE-190 | ✅ Supported |
| Reachability of target/error functions | — | ✅ Supported |
| Memory leak / use-after-free / double-free | CWE-401/416/415 | ❌ Future work¹ |

¹ In lifted WASM code the source language's allocator is compiled *inside* the linear memory, so `malloc`/`free` calls are not visible in the IR. Full memory tracking requires an export convention or allocator-detection heuristics — planned as future work.

##### Runtime requirements for `--wasm`

- **WABT ≥ 1.0.41** — `wasm2c` on `PATH` and the `wasm-rt.h` headers (searched at `/opt/wabt-1.0.41/include`, then `/opt/wabt/include`, then `/usr/include`). The `wabt` package from Ubuntu apt (1.0.27) is **too old**; install the [GitHub release](https://github.com/WebAssembly/wabt/releases/tag/1.0.41).
- **clang-16** at `/usr/bin/clang-16` (used to compile the lifted C to LLVM bitcode).

Both are pre-installed in the development Docker image ([Dockerfile.dev](/Dockerfile.dev)). Only `.wasm` (binary) files are accepted; for a `.wat` (text format) file, convert it first with `wat2wasm module.wat -o module.wasm` (also part of WABT).

##### Usage

```bash
$ ./map2check --wasm --memtrack --timeout 290 module.wasm
```

Relevant options:

- `--wasm` — enable the WASM pipeline (lifting + WASM-mode instrumentation). Implies memtrack mode.
- `--entry-function <name>` — override the entry function name (default: `main`). Map2Check automatically generates a `main()` wrapper that initializes the wasm2c runtime and calls the module's `w2c_*_start` entry point, so in most cases you do not need this flag.
- `--timeout <s>` — give KLEE enough time to explore the lifted IR. Lifted modules embed the whole WASI libc, so short timeouts (e.g. 110 s) tend to yield `UNKNOWN`; **290 s** is the value validated on the Juliet benchmarks.

##### End-to-end example

Inside the development container, create a C program with a heap buffer overflow, compile it to WASM with the wasi-sdk (pre-installed at `$WASI_SDK_PATH`), and verify the resulting binary:

```bash
$ cat > test_heap_overflow.c << 'EOF'
#include <stdlib.h>
int main() {
 int* p = (int*)malloc(10 * sizeof(int));
 if (!p) return -1;
 p[0] = 42;
 p[10] = 999; /* out-of-bounds write */
 free(p);
 return 0;
}
EOF

$ $WASI_SDK_PATH/bin/clang --target=wasm32-wasip1 \
    test_heap_overflow.c -o test_heap_overflow.wasm

$ ./map2check --wasm --memtrack --timeout 290 test_heap_overflow.wasm
# Expected result:
Adopting z3 solver...
Started Map2Check
WASM mode: lifting test_heap_overflow.wasm

...

----------------------------------------------------
Violated property:
	file map2check_property line 8 function main
	OVERFLOW

VERIFICATION FAILED
```

A safe program (e.g. writing to `p[9]` instead of `p[10]`) is not flagged. The pipeline was validated on a subset of the **Juliet Test Suite** compiled to WASM (CWE-121/122/124/126/127): all 15 seeded bugs were detected as `FALSE` with a 290 s timeout — see [test-comp2026/simulation/resultados_de_testes/juliet_wasm/wasm_results.csv](test-comp2026/simulation/resultados_de_testes/juliet_wasm/wasm_results.csv). The integration test scripts [tests/integration/test_wasm_pipeline.sh](tests/integration/test_wasm_pipeline.sh) and [tests/integration/test_wasm_entrypoint.sh](tests/integration/test_wasm_entrypoint.sh) reproduce this workflow automatically.

___

#### How to build Map2Check?

You can build Map2Check using our development Docker image ([Dockerfile.dev](/Dockerfile.dev)), which provides Ubuntu 22.04 with LLVM 16, KLEE 3.1, WABT 1.0.41 and wasi-sdk 33.0 pre-installed:

``` bash
$ git clone https://github.com/hbgit/Map2Check.git
$ cd Map2Check
# Build the development Docker image
$ docker build -t map2check-dev --no-cache -f Dockerfile.dev .
$ docker run -it --rm -v $(pwd):/workspace map2check-dev /bin/bash
```

Inside the container:

``` bash
$ mkdir build && cd build
$ cmake .. -G Ninja \
    -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm
$ ninja && ninja install
# binário em: release/bin/map2check (ou release/map2check)
```

The `Dockerfile.dev` image already builds and installs KLEE 3.1 (to `/opt/klee`) and provides LibFuzzer via LLVM 16's compiler-rt, so **do not** pass `-DSKIP_KLEE=ON` or `-DSKIP_LIB_FUZZER=ON` — those flags skip the `cmake/FindKlee.cmake` / `cmake/FindLibFuzzer.cmake` modules entirely, which are what copy the KLEE binaries and `libFuzzer.a` into `release/`. Only pass them `ON` if you deliberately want a build without KLEE/LibFuzzer support (e.g. `-DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON` for a minimal/CI build).

**Building with WASM support** requires **no additional CMake flag** — the `WasmLifter` frontend module is always compiled. The only extra build-time dependency is the WABT 1.0.41 header `wasm-rt.h`: when CMake finds it (searched at `/opt/wabt-1.0.41/include`, `/usr/include`, `/usr/local/include`), it compiles the KLEE-compatible wasm2c runtime `WasmRuntimeStubs.c` to bitcode and installs it as `release/lib/WasmRuntimeStubs.bc`, which is linked into the lifted module when `--wasm` is used. If `wasm-rt.h` is not found, CMake prints a warning and the build proceeds **without** WASM support (the recommended way to get a WASM-enabled build is the Docker image above, which ships WABT and the wasi-sdk out of the box).

Minor test:
``` bash
$ cd ../release/
$ ./map2check --memtrack svcomp_960521-1_false-valid-free.c
# Expected Result:
Adopting z3 solver... 
Started Map2Check
Compiling /workspace/release/../tests/regression_test/test_cases/sv-benchmarks/memsafety/960521-1-1.c

...

>>Memory list log

Line content   :   { free(a); free(b); } /* ditto */
  Address        : 0x55ba60a90700
  PointsTo       : 0x7f95f0003d54
  Is Free        : TRUE
  Is Dynamic     : FALSE
  Var Name       : b
  Line Number    : 29
  Function Scope : main

----------------------------------------------------
Violated property:
	file map2check_property line 29 function main
	FALSE-FREE: Operand of free must have zero pointer offset

VERIFICATION FAILED
```

Requires: **CMake ≥ 3.20**, **C++17**, **LLVM 16**, **Boost**.

More details at https://map2check.github.io/docker.html

#### How to run the tests

**Unit tests** (no KLEE/LibFuzzer required):

``` bash
$ mkdir build && cd build
$ cmake .. -G Ninja \
    -DLLVM_DIR=/usr/lib/llvm-16/lib/cmake/llvm \
    -DSKIP_LIB_FUZZER=ON -DSKIP_KLEE=ON -DENABLE_TEST=ON
$ ninja && ctest --output-on-failure
# Expected results:
Test project /workspace/build
    Start 1: HelloGTest
1/7 Test #1: HelloGTest .......................   Passed    0.00 sec
    Start 2: AllocationLogTest
2/7 Test #2: AllocationLogTest ................   Passed    0.00 sec
    Start 3: HeapLogTest
3/7 Test #3: HeapLogTest ......................   Passed    0.00 sec
    Start 4: ContainerReallocTest
4/7 Test #4: ContainerReallocTest .............   Passed    0.00 sec
    Start 5: BTreeTest
5/7 Test #5: BTreeTest ........................   Passed    0.06 sec
    Start 6: ContainerBTreeTest
6/7 Test #6: ContainerBTreeTest ...............   Passed    0.05 sec
    Start 7: MemTrackTest
7/7 Test #7: MemTrackTest .....................   Passed    0.00 sec

100% tests passed, 0 tests failed out of 7
```

**WASM integration tests** (require the Docker image, i.e. KLEE + WABT + wasi-sdk):

``` bash
$ ./tests/integration/test_wasm_pipeline.sh      # heap overflow detection + CLI flag
$ ./tests/integration/test_wasm_entrypoint.sh    # entry-point wrapper generation
```

These are also run on every push/PR by the `e2e-wasm` job in [.github/workflows/ci.yml](.github/workflows/ci.yml), which exercises the full `.wasm → LLVM IR → passes → KLEE` pipeline inside the published `map2check-dev` image.
___

#### Instructions for SV-COMP

Use the [map2check-wrapper.py](utils/map2check-wrapper.py) script in the Map2Check binary directory to verify each single test-case.

Usage:

``` bash
$ ./map2check-wrapper.py -p propertyFile.prp file.i
```

Map2Check accepts the property file and the verification task and provides as verification result:
TRUE + Witness, [FALSE|FALSE(p)] + Witness, or UNKNOWN.
FALSE(p), with p in {valid-free, valid-deref, valid-memtrack, valid-memcleanup}, means that the (partial)
property p is violated.
For each verification result the witness file (called witness.graphml) is generated Map2Check root-path folder.
There is timeout of 897 seconds set by this script, using "timeout" tool that is part of coreutils
on debian. If these constraints are violated, it should be treated as UNKNOWN result.

___

#### Authors

Maintainers:
  - Herbert O. Rocha (since 2014), Federal University of Roraima, Brazil - https://hbgit.github.io/
  - Rafael Menezes   (since 2016), Federal University of Roraima, Brazil - https://rafaelsa94.github.io/
  - Guilherme Bernardo (since 2025), Federal University of Roraima, Brazil - https://github.com/GuilhermeBn198

Questions and bug reports:  
  E-mail: map2check.tool@gmail.com

.-. 
 /v\
 // \\ > L I N U X - GPL <
 /( )\
 ^^-^^
bug found -> verified safe

Map2Check . Linux . GPL

Map2Check

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README