| Wuffs author here. It's not full-blown formal verification but it doesn't have to be. Unlike most formal verification projects that I've seen, the proof part of Wuffs isn't about correctness (proving that "this implementation satisfies the PNG specification"), it's about safety (proving that "this implementation won't read/write out of bounds"), which is much more tractable. Especially as the PNG spec (or WebP spec) doesn't mandate how to treat malicious input (like unbalanced Huffman tables). Wuffs doesn't have a WebP decoder yet but it's literally in the Roadmap and I've previously written the golang.org/x/image/webp package in the Go programming language. Wuffs does have a PNG decoder, PNG uses Deflate compression and Deflate and WebP's "decode a Huffman tree" data tables are very similar. Wuffs also has an equivalent of zlib's enough.c program mentioned in the original blog post to calculate worst-case memory requirements. Wuffs' version is called script/print-deflate-huff-table-size.go and it says that, for a 9-bit primary table, we need 852 table entries. Round that up to 1024, for nearest power-of-two. If you look for HUFFS_TABLE_SIZE = 1024 and HUFFS_TABLE_MASK = 1023 in Wuffs' std/deflate source code, you'll notice that Wuffs' Deflate decoder isn't susceptible to the same problem as the C/C++ WebP decoder the original blog post discussed. This is because, unless the Wuffs compiler can prove otherwise, the code doesn't just look up the table like `this.huffs[0][i]`, it's like `this.huffs[0][i&mask]` and `i&mask` is always in bounds. The mask is either HUFFS_TABLE_MASK or it's of a refinement type guaranteed <= 511. The array is always (statically) allocated with 1024 entries even though enough.c says that, with dynamic allocation, we could possibly get away with a smaller table. As you already know, for Wuffs (and unlike C/C++), taking out the `&mask` will lead to a compile-time error. Wuffs code won't compile unless the compiler can prove that array indexes are always within bounds. From the grandparent: > this WebP bug occurred because the largest table size was formally proven but it didn't match what was fed to the source code With WebP+enough.c this 'largest table size' was calculated by exhaustive, brute-force search (not really a formal proof) but it was based on assumptions (balanced codes) that didn't match actual (malicious) input. Or, in zlib-the-library, there's other C code (https://github.com/madler/zlib/blob/ac8f12c97d1afd9bafa9c710...) that rejects unbalanced Huffman codes, but IIUC similar enforcement was (until very recently) missing in libwebp. With Wuffs, even if the worst-case calculation was based on an incorrect model (or forgetting to separately reject unbalanced codes), the end result (on malicious input) might be "the wrong pixels" but it shouldn't be "buffer overflow". |
Yes, I actually think that the choice to unequivocally prove safety rather than to attempt to prove that you implemented something specific (but with the risk that our specification is wrong), is almost invariably the right choice for this problem space. It would not have been appropriate for the TLS 1.3 protocol (which has a machine proof that it satisfies our intended criteria stated in the RFC, modulo the Selfie attack and assuming our cryptographic primitives all do what they said they do), but it's exactly the right thing for say a DOCX parser, or ZIP parser, or a JPEG compressor or similar for which WUFFS is the right choice.