# OSS Verify: proofs about OSS-Fuzz fuzz targets [](https://github.com/theorem-labs/oss-verify-proofs/actions/workflows/release-check.yml?query=branch%3Amain) OSS-Fuzz runs the fuzz targets of open-source projects to search for inputs that make them fail. This repository holds Rocq proofs that, for some of these fuzz targets, no such input exists within stated limits. Each proof is about compiled binaries, not source code. It shows that, on every input within the limits, the build with a sanitizer behaves like the plain build, and that the sanitizer never detects an error. OSS Verify is a Theorem program; a maintainer enrolls a project at [theorem-labs/oss-verify](https://github.com/theorem-labs/oss-verify). 60 entry points in 25 libraries have proofs. The proofs are checked with Rocq 9.2.0. They are stated in LPS, a formal model of a Linux process that runs a RISC-V binary. **LPS is best effort and not complete.** It describes part of Linux, and it makes some assumptions that it does not check. A proof is only as good as LPS. [docs/semantics.md](docs/semantics.md) gives the design principles of LPS and its limits. - [What is proved](#what-is-proved) - [The theorem, in words](#the-theorem-in-words) - [What a proof does not say](#what-a-proof-does-not-say) - [Versions](#versions) - [Check a proof](#check-a-proof) - [How the binaries are built](#how-the-binaries-are-built) - [Explore the proofs](#explore-the-proofs) - [Statements for OSS-Fuzz fuzz targets](#statements-for-oss-fuzz-fuzz-targets) - [What you have to trust](#what-you-have-to-trust) - [Repository layout](#repository-layout) ## What is proved | library | entry point | sanitizer builds proved | |---|---|---| | boost-beast | [http_request](proofs/boost-beast/http_request/) | ASan, UBSan, ASan+UBSan | | boost-json | [fuzz_parse](proofs/boost-json/fuzz_parse/) | ASan, UBSan, ASan+UBSan | | bzip2 | [bzip2_compress_target](proofs/bzip2/bzip2_compress_target/) | ASan, ASan+UBSan | | cgif | [cgif_file_fuzzer](proofs/cgif/cgif_file_fuzzer/) | ASan+UBSan | | cgif | [cgif_rgb_fuzzer](proofs/cgif/cgif_rgb_fuzzer/) | ASan, ASan+UBSan | | cjson | [cjson_read_fuzzer](proofs/cjson/cjson_read_fuzzer/) | ASan, UBSan, ASan+UBSan | | coturn | [FuzzStunClient](proofs/coturn/FuzzStunClient/) | ASan, UBSan, ASan+UBSan | | double-conversion | [string_to_double_fuzzer](proofs/double-conversion/string_to_double_fuzzer/) | ASan, UBSan, ASan+UBSan | | fast_float | [from_chars](proofs/fast_float/from_chars/) | ASan, UBSan, ASan+UBSan | | glaze | [binary_reflection](proofs/glaze/binary_reflection/) | ASan, UBSan, ASan+UBSan | | json-c | [json_object_fuzzer](proofs/json-c/json_object_fuzzer/) | ASan, ASan+UBSan | | jsoncons | [fuzz_bigint](proofs/jsoncons/fuzz_bigint/) | ASan, UBSan, ASan+UBSan | | jsoncons | [fuzz_bson_parser_max](proofs/jsoncons/fuzz_bson_parser_max/) | ASan | | jsoncons | [fuzz_json_cursor](proofs/jsoncons/fuzz_json_cursor/) | ASan, ASan+UBSan | | jsoncons | [fuzz_json_encoder](proofs/jsoncons/fuzz_json_encoder/) | ASan, ASan+UBSan | | jsoncons | [fuzz_msgpack_encoder](proofs/jsoncons/fuzz_msgpack_encoder/) | ASan | | jsoncons | [fuzz_ubjson_encoder](proofs/jsoncons/fuzz_ubjson_encoder/) | ASan, UBSan, ASan+UBSan | | jsoncons | [fuzz_ubjson_parser_max](proofs/jsoncons/fuzz_ubjson_parser_max/) | ASan, UBSan, ASan+UBSan | | leptonica | [bilateral_fuzzer](proofs/leptonica/bilateral_fuzzer/) | ASan, ASan+UBSan | | leptonica | [colorfill_fuzzer](proofs/leptonica/colorfill_fuzzer/) | ASan, UBSan, ASan+UBSan | | leptonica | [edge_fuzzer](proofs/leptonica/edge_fuzzer/) | ASan, UBSan, ASan+UBSan | | leptonica | [fhmtgen_fuzzer](proofs/leptonica/fhmtgen_fuzzer/) | ASan, ASan+UBSan | | leptonica | [graymorph_fuzzer](proofs/leptonica/graymorph_fuzzer/) | ASan, UBSan, ASan+UBSan | | leptonica | [grayquant_fuzzer](proofs/leptonica/grayquant_fuzzer/) | ASan, ASan+UBSan | | leptonica | [jpegiostub_fuzzer](proofs/leptonica/jpegiostub_fuzzer/) | ASan, UBSan, ASan+UBSan | | leptonica | [kernel_fuzzer](proofs/leptonica/kernel_fuzzer/) | ASan, UBSan, ASan+UBSan | | leptonica | [paintcmap_fuzzer](proofs/leptonica/paintcmap_fuzzer/) | ASan, UBSan, ASan+UBSan | | leptonica | [pix1_fuzzer](proofs/leptonica/pix1_fuzzer/) | ASan, UBSan, ASan+UBSan | | leptonica | [pix_orient_fuzzer](proofs/leptonica/pix_orient_fuzzer/) | ASan, ASan+UBSan | | libpcap | [fuzz_pcap](proofs/libpcap/fuzz_pcap/) | ASan, UBSan, ASan+UBSan | | mbedtls | [fuzz_pkcs7](proofs/mbedtls/fuzz_pkcs7/) | ASan | | msgpack-c | [unpack_pack_fuzzer](proofs/msgpack-c/unpack_pack_fuzzer/) | ASan, UBSan, ASan+UBSan | | openssl | [bignum](proofs/openssl/bignum/) | ASan, ASan+UBSan | | openssl | [bndiv](proofs/openssl/bndiv/) | ASan, UBSan | | openssl | [ct](proofs/openssl/ct/) | ASan+UBSan | | openssl | [echconfiglist_parser](proofs/openssl/echconfiglist_parser/) | ASan, UBSan | | openssl | [hashtable](proofs/openssl/hashtable/) | ASan | | openssl | [pem](proofs/openssl/pem/) | ASan+UBSan | | openssl | [punycode](proofs/openssl/punycode/) | ASan, UBSan, ASan+UBSan | | pupnp | [FuzzHttp](proofs/pupnp/FuzzHttp/) | ASan, ASan+UBSan | | simdjson | [fuzz_atpointer](proofs/simdjson/fuzz_atpointer/) | ASan, UBSan, ASan+UBSan | | simdjson | [fuzz_dump](proofs/simdjson/fuzz_dump/) | ASan, UBSan | | simdjson | [fuzz_dump_raw_tape](proofs/simdjson/fuzz_dump_raw_tape/) | ASan, UBSan | | simdjson | [fuzz_element](proofs/simdjson/fuzz_element/) | ASan+UBSan | | simdjson | [fuzz_implementations](proofs/simdjson/fuzz_implementations/) | ASan, UBSan | | simdjson | [fuzz_minifyimpl](proofs/simdjson/fuzz_minifyimpl/) | ASan, UBSan, ASan+UBSan | | simdjson | [fuzz_ondemand](proofs/simdjson/fuzz_ondemand/) | ASan, UBSan, ASan+UBSan | | simdjson | [fuzz_parser](proofs/simdjson/fuzz_parser/) | ASan, UBSan, ASan+UBSan | | simdjson | [fuzz_print_json](proofs/simdjson/fuzz_print_json/) | ASan, ASan+UBSan | | simdjson | [fuzz_utf8](proofs/simdjson/fuzz_utf8/) | ASan, UBSan, ASan+UBSan | | skcms | [iccprofile_info](proofs/skcms/iccprofile_info/) | ASan, UBSan, ASan+UBSan | | speex | [speex_decode_fuzzer_float](proofs/speex/speex_decode_fuzzer_float/) | ASan, ASan+UBSan | | spirv-tools | [spvtools_binary_parser_fuzzer](proofs/spirv-tools/spvtools_binary_parser_fuzzer/) | ASan, UBSan | | tinyobjloader | [fuzz_tobj_c](proofs/tinyobjloader/fuzz_tobj_c/) | ASan, ASan+UBSan | | varnish | [esi_parse_fuzzer](proofs/varnish/esi_parse_fuzzer/) | ASan, UBSan, ASan+UBSan | | yajl-ruby | [json_fuzzer](proofs/yajl-ruby/json_fuzzer/) | ASan, UBSan, ASan+UBSan | | zstd | [fse_read_ncount](proofs/zstd/fse_read_ncount/) | ASan, ASan+UBSan | | zstd | [huf_decompress](proofs/zstd/huf_decompress/) | ASan | | zstd | [simple_decompress](proofs/zstd/simple_decompress/) | ASan+UBSan | | zstd | [zstd_frame_info](proofs/zstd/zstd_frame_info/) | ASan, ASan+UBSan | [index/PROOFS.md](index/PROOFS.md) has one row for each entry point: the statements proved, the system-call failures they allow, the binaries, and where the proof is. Every proof is about the binaries of this release and the statements under `projects/`. All of them use one LPS version and one static AddressSanitizer ([Versions](#versions)). [docs/origin.md](docs/origin.md) says how the proofs were made: the proving task, its submissions and its checker, and how a proof enters this repository. ## The theorem, in words Every proof here proves one or more agreement statements. There is one agreement statement for each sanitizer build: AddressSanitizer (ASan), UndefinedBehaviorSanitizer (UBSan), or both (ASan+UBSan). An agreement statement says: > On every input on which the plain build stays within its memory budget, neither build reaches an error, and the plain build and the sanitizer build have the same set of observable behaviours. - **Every input** means every process input that LPS accepts as valid: the arguments, the environment variables, the files (so the input file, its contents or its absence), standard input, and the rest of what a process receives. LPS leaves out a few inputs; for example, an argument after the program name may not contain `/` ([docs/semantics.md](docs/semantics.md)). - **An error** is a crash, an invalid memory access, an `abort()` (a failed `assert()`, a sanitizer report or an uncaught C++ exception), a failed UBSan check, or a step that LPS does not interpret. - **Observable behaviours** are the bytes that the process reads and writes on its standard streams and connections, in order, its exit status, and the final contents of its files. - **The memory budget** of the plain build is 2 GiB in a statement about a build with ASan (ASan or ASan+UBSan), and 16 GiB in a statement about the UBSan build. The budget is a premise: an input on which the plain build needs more memory is not covered. - **System-call failures.** Each statement says which system calls the environment may refuse without cause. In most of the proofs here, a memory request is refused only when the budget is spent or no address range is free. So a proof rules out every error that the sanitizer build detects, on every input that the statement covers. If the harness checks a property with `assert()`, `abort()` or a trap, and the check is in the binary, the proof also shows that the property holds on every covered input ([docs/exploring.md](docs/exploring.md)). The Rocq definitions are in [theories/Shapes.v](theories/Shapes.v). Each agreement form is proved equal to its LPS definition, `strong_universal_error_free_T_budgets` or one of its variants. [docs/statements.md](docs/statements.md) explains each form. ## What a proof does not say - It does not say that the library is correct. Errors that the sanitizers cannot detect are not excluded: for example, a wrong result or a memory leak. - It is about the code that one entry point reaches, not about the whole library. - It is about these binaries: static riscv64 programs, built with clang 20.1.8 against musl. It is not about the source code, and not about the x86-64 builds of OSS-Fuzz. - It is true in LPS. Where LPS differs from Linux, the proof may not apply ([docs/semantics.md](docs/semantics.md)). - An agreement statement does not exclude a run that never ends. Only a halts statement does. No proof in this release proves a halts statement, so none of them rules out a run that never ends. ## Versions | item | version | |---|---| | Rocq | 9.2.0, the official release (opam package `rocq-core`). The proofs load their libraries with plain `Require`. | | checker image | `ghcr.io/theorem-labs/oss-fuzz-theorems-checker@sha256:cc9ae43a9f4b0dd59d7c8d30727d36e039bfe72a2a9f9c4a99c68e413037e902`. It holds Rocq, LPS with its `elf-snapshot` tool, the Rocq libraries that the proofs use, dune and Python 3, and no proof automation ([toolchain/checker.Dockerfile](toolchain/checker.Dockerfile)). | | LPS | [rocq-linux-process-semantics](https://github.com/theorem-labs/rocq-linux-process-semantics) commit [`f1006fe81783`](https://github.com/theorem-labs/rocq-linux-process-semantics/commit/f1006fe8178338a499b5e5c41be83006c4edd058), for every statement and every proof ([docs/semantics.md](docs/semantics.md)) | | static AddressSanitizer | [static-asan](https://github.com/theorem-labs/static-asan) commit [`b0506135`](https://github.com/theorem-labs/static-asan/commit/b05061352064fa2be1813ac5429149f3de5f057d): the published source of the static AddressSanitizer that built every ASan binary of this release ([docs/building.md](docs/building.md#the-addresssanitizer-runtime)) | | OSS-Fuzz | [`bd2ce219`](https://github.com/google/oss-fuzz/tree/bd2ce21991a94a362b92fb1bf25f86d5a1a60842) | | axioms | only the axioms in [toolchain/allowed-axioms.txt](toolchain/allowed-axioms.txt): the primitive integer, array and string types of Rocq with their specifications, and six axioms of the standard library (`classic`, `functional_extensionality_dep`, `constructive_indefinite_description`, `propositional_extensionality`, `sig_forall_dec` and `sig_not_dec`) | ## Check a proof You need Docker, zstd, and Python 3 with PyYAML (`tools/oft/requirements.txt`). The checker image holds Rocq and LPS, but not PyYAML, so the commands below mount it. On 16 cores, one proof check needs up to 20 GiB of memory. It compiles one file per core, so more cores need more memory; `docker run --cpuset-cpus` limits the cores. git clone https://github.com/theorem-labs/oss-verify-proofs && cd oss-verify-proofs ./oft fetch coturn # the project's binaries, each checked against its SHA-256 python3 -m pip install --require-hashes --target "$HOME/oft-pydeps" -r tools/oft/requirements.txt docker run --rm --network none -u "$(id -u):$(id -g)" -e HOME=/tmp -e PYTHONPATH=/pydeps \ -v "$HOME/oft-pydeps:/pydeps:ro" -v "$PWD:/work" -w /work ghcr.io/theorem-labs/oss-fuzz-theorems-checker@sha256:cc9ae43a9f4b0dd59d7c8d30727d36e039bfe72a2a9f9c4a99c68e413037e902 \ ./oft check coturn/FuzzStunClient --parts statements,proofs `oft check` does these steps. It checks each binary against its SHA-256. It builds the memory images and the statements. It compiles each proof. It compiles a small wrapper that gives the proof's theorem the type of the statement. Then it reads what `Print Assumptions` prints for the wrapper, and it refuses every assumption that is not in the allowed list ([docs/checking.md](docs/checking.md)). CI runs the same check. The [release-check](.github/workflows/release-check.yml) workflow checks every committed proof on each push to `main` and once a week, and the badge at the top shows its result. The [pr](.github/workflows/pr.yml) workflow checks what a pull request changes. The [weekly](.github/workflows/weekly.yml) workflow checks every statement and every proof, with no cache ([docs/checking.md](docs/checking.md#what-ci-runs)). ## How the binaries are built Each binary is a static riscv64 Linux program, built with clang 20.1.8 against musl. An entry point has up to four builds: plain, ASan, UBSan and ASan+UBSan. [docs/building.md](docs/building.md) gives the compiler flags and the sanitizer settings. [docs/running.md](docs/running.md) tells you how to run a binary and what its input file holds. Each proof has a build record in `proofs///provenance/`. The record gives the upstream repository and commit, the harness file, the recipe, the compiler, the builder image, the static AddressSanitizer commit, the compiler and linker flags, the SHA-256 of each binary, and the licences. [docs/reproducing.md](docs/reproducing.md) tells you how to rebuild a binary and compare its SHA-256. ## Explore the proofs [docs/exploring.md](docs/exploring.md) points to what the proofs show beyond "no sanitizer error": properties that the harnesses check, and lemmas about what the library code computes. It also tells you how to find the machine-generated data in a proof. ## Statements for OSS-Fuzz fuzz targets This repository also states theorems about many OSS-Fuzz fuzz targets, proved or not. For each of the 1,381 projects in OSS-Fuzz there is a directory under [projects/](projects/). We can build the fuzz targets of 427 of these projects. 2,148 of their 5,290 fuzz targets have statements in this release; [index/STATUS.md](index/STATUS.md) says why the others do not. Each of these fuzz targets is compiled up to four ways (2,141 of the 2,148 harnesses have all four), and each build gets Rocq statements about those exact bytes. These are statements, not results: 138 are proved, some are known to be false, and proofs are added as they are found. In this release: 20,164 statements: 138 proved, 0 known false (0 counterexamples, 0 false (witnessed)), 0 suspected false, 229 blocked by the model, 0 withheld (0 waiting for their source bundle, 0 not published yet), 19,797 open. [analyses/known-issues.md](analyses/known-issues.md) lists every statement that is not open or proved, with the reason. There are four kinds of statement: a build halts; a sanitizer build agrees with the plain build; the two builds disagree on at most a fraction *b* of a stated input distribution; and the inputs on which they agree are decidable ([docs/statements.md](docs/statements.md)). One example: [`zlib/checksum_fuzzer/plain_halts`](projects/zlib/checksum_fuzzer/Statements.v): on every input on which the plain build is never refused memory for exceeding 16 GiB, and when the environment refuses nothing that it is not forced to (both are premises), every execution exits with status 0 or 2. The harness `checksum_fuzzer` asserts that CRC-32 combine law, per chunk (chunk size = data[0], min 1): crc32_combine_op(crc_so_far, crc32(0,chunk), crc32_combine_gen(chunk_len)) must equal crc32_z(crc_so_far, chunk); chunked crc32_z over the whole input (chunk size data[0]) must equal the one-shot crc32(0, data, len) (and 4 checks more), so a proof shows that these hold on every input it covers. Definition plain_halts : Prop := halts_within_budget Budgets.Standard.lim_source Exits.ok_or_refused Images.plain. | status | projects | |---|---:| | [available](docs/status.md#available) | 427 | | [language pending](docs/status.md#language-pending) | 781 | | [not yet built](docs/status.md#not-yet-built) | 97 | | [needs model support](docs/status.md#needs-model) | 3 | | [no compiler](docs/status.md#no-compiler) | 3 | | [no harness](docs/status.md#no-harness) | 32 | | [excluded](docs/status.md#excluded) | 6 | | [held](docs/status.md#held) | 32 | | **all OSS-Fuzz projects** | **1,381** | The 427 available projects have 2,148 harnesses with statements and 20,164 statements; 8,578 binaries are attached to this release and 0 more are withheld. [index/STATUS.md](index/STATUS.md) lists every project; `index/*.tsv` has the same data for scripts. To prove or refute a statement, see [docs/proving.md](docs/proving.md) and [CONTRIBUTING.md](CONTRIBUTING.md). A counterexample that shows a bug in a library goes to that library first ([SECURITY.md](SECURITY.md)). To enroll your own project, see [theorem-labs/oss-verify](https://github.com/theorem-labs/oss-verify). ## What you have to trust - The Rocq kernel, with its bytecode machine (`vm_compute`), and the axioms in [toolchain/allowed-axioms.txt](toolchain/allowed-axioms.txt). - LPS, at the commit that [release.yaml](release.yaml) names ([docs/semantics.md](docs/semantics.md)). - The tools that turn an ELF file into an LPS memory image: LPS's `elf-snapshot`, and `rocq-read-file` 0.0.2, an OCaml plugin that reads the image's bytes into Rocq at compile time. - `oft check`: the wrapper that it writes, and its reading of `Print Assumptions` ([tools/oft/check.py](tools/oft/check.py)). [docs/trust.md](docs/trust.md) says what each of these covers. ## Repository layout | path | contents | |---|---| | `proofs////` | the proof of one statement, and its `proof.yaml` | | `proofs///provenance/` | the build record of that harness's binaries | | `proofs///lib/` | the lemmas that the proofs of that harness share | | `projects///` | the facts (`harness.yaml`), the statements (`Statements.v`), the images (`Images.v`), the harness page, and, for most harnesses, a copy of the harness source (`source/`) | | `theories/` | the statement forms (`Shapes.v`), the image library, and the input-file format (`Driver.v`) | | `index/` | tables of every proof, project, harness, statement and binary | | `toolchain/` | the Dockerfiles of the checker and runner images, the pinned versions (`toolchain.lock`), the allowed axioms, and the list of LPS files | | `tools/oft/` | the `oft` tool: fetch, generate, lint and check | | `tests/` | a generator of toy binaries, and controls that the checker must accept or refuse | | `counterexamples/` | inputs that make a binary break a statement, each with a control input | | `analyses/` | the checks that the harnesses make (`harness-checks/`), and every statement that is not open or proved (`known-issues.md`) | | `LICENSES/` | licence texts of proof files made from proofs under another licence | | `docs/` | the documentation | ## Citing [CITATION.cff](CITATION.cff). A statement is cited as `project/harness/statement@r`, for example `zlib/checksum_fuzzer/plain_halts@r1`. Until LPS is released, revisions are provisional ([docs/versioning.md](docs/versioning.md)). ## Licence What we wrote is under the MIT licence ([LICENSE](LICENSE)): the statements, the tools, the documentation and our proofs. Proofs that we made from proofs that Anthropic licensed under the Apache License 2.0 or the MIT licence, at the recipient's option, keep those licences. The licence texts are [LICENSES/anthropic-proofs-LICENSE](LICENSES/anthropic-proofs-LICENSE) and [LICENSES/anthropic-proofs-LICENSE-MIT](LICENSES/anthropic-proofs-LICENSE-MIT) and the notices are [LICENSES/anthropic-proofs-NOTICE](LICENSES/anthropic-proofs-NOTICE); the build record of each such proof names these three files ([docs/licensing.md](docs/licensing.md)). The binaries, the source archives and the harness copies keep their own licences ([NOTICE](NOTICE)). This project is not affiliated with or endorsed by Google or the OSS-Fuzz project.