theorem-labs / oss-verify-proofs

# OSS Verify: proofs about OSS-Fuzz fuzz targets
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.
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 gives the design principles of LPS and its limits.
- What is proved
- The theorem, in words
- What a proof does not say
- Versions
- Check a proof
- How the binaries are built
- Explore the proofs
- Statements for OSS-Fuzz fuzz targets
- What you have to trust
- Repository layout
## What is proved
| library | entry point | sanitizer builds proved |
|---|---|---|
| boost-beast | http_request | ASan, UBSan, ASan+UBSan |
| boost-json | fuzz_parse | ASan, UBSan, ASan+UBSan |
| bzip2 | bzip2_compress_target | ASan, ASan+UBSan |
| cgif | cgif_file_fuzzer | ASan+UBSan |
| cgif | cgif_rgb_fuzzer | ASan, ASan+UBSan |
| cjson | cjson_read_fuzzer | ASan, UBSan, ASan+UBSan |
| coturn | FuzzStunClient | ASan, UBSan, ASan+UBSan |
| double-conversion | string_to_double_fuzzer | ASan, UBSan, ASan+UBSan |
| fast_float | from_chars | ASan, UBSan, ASan+UBSan |
| glaze | binary_reflection | ASan, UBSan, ASan+UBSan |
| json-c | json_object_fuzzer | ASan, ASan+UBSan |
| jsoncons | fuzz_bigint | ASan, UBSan, ASan+UBSan |
| jsoncons | fuzz_bson_parser_max | ASan |
| jsoncons | fuzz_json_cursor | ASan, ASan+UBSan |
| jsoncons | fuzz_json_encoder | ASan, ASan+UBSan |
| jsoncons | fuzz_msgpack_encoder | ASan |
| jsoncons | fuzz_ubjson_encoder | ASan, UBSan, ASan+UBSan |
| jsoncons | fuzz_ubjson_parser_max | ASan, UBSan, ASan+UBSan |
| leptonica | bilateral_fuzzer | ASan, ASan+UBSan |
| leptonica | colorfill_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | edge_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | fhmtgen_fuzzer | ASan, ASan+UBSan |
| leptonica | graymorph_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | grayquant_fuzzer | ASan, ASan+UBSan |
| leptonica | jpegiostub_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | kernel_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | paintcmap_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | pix1_fuzzer | ASan, UBSan, ASan+UBSan |
| leptonica | pix_orient_fuzzer | ASan, ASan+UBSan |
| libpcap | fuzz_pcap | ASan, UBSan, ASan+UBSan |
| mbedtls | fuzz_pkcs7 | ASan |
| msgpack-c | unpack_pack_fuzzer | ASan, UBSan, ASan+UBSan |
| openssl | bign