Map2Check

Finding Software Vulnerabilities using Symbolic Execution and Fuzzing

---

Map2Check is a bug hunting tool that automatically generates and checks safety properties in C programs. 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 version 16, LibFuzzer, KLEE to generate input values to the test cases generated by Map2Check.

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:

$ 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:

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

Running the tool

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

$ ./map2check --memtrack program.c

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

$ ./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).

---

How to build Map2Check?

You can build Map2Check using our development Docker image (Dockerfile.dev), which provides Ubuntu 22.04 with LLVM 16 and KLEE 3.1 pre-installed:

$ 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:

$ 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).

Minor test:

$ 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):

$ 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

---

Instructions for SV-COMP

Use the map2check-wrapper.py script in the Map2Check binary directory to verify each single test-case.

Usage:

$ ./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