Formally Verifying the jsmn JSON Parser

Setup

1. Install CBMC. Directions for installing CBMC can be found at the official CBMC git repository
2. Clone this repository with --recurse-submodules to pull the exact version of jsmn we intend to verify
3. On windows, we used msys2 for make.

Usage

• See the specific version of jsmn being verified with git submodule status:

> git submodule status
 25647e692c7906b96ffd2b05ca54c097948e879c jsmn (v1.0.0-11-g25647e6)

• Run the entire suite of proofs with make all

• List all available verification proofs with make list

• Run a specific verification proof with make $proof where $proof is a target found in make list

• For help, run make help

Approach

We aim to verify safety and liveness properties of jsmn using CBMC, a bounded model checker.

Safety Properties

• No buffer overflows or overruns are possible
• No null pointer dereferences are possible
• No signed integer overflow resulting in undefined behavior
• No memory leaks (trivial, the library is 0 allocation)

Bounded Liveness

• For all inputs up to size n (not yet chosen), the the jsmn parser eventually returns within c*n steps where c is a constant

Development

Each proof lives in its own directory under proofs/ and contains a:

• Makefile that will run the proof by simply running make
• README.md that explains what the proof does