6 ms·

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 o

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/ac8f12c97d1afd9bafa9c710f827d40a407d3266/inftrees.c#L125-L133 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".

lifthrasiir 3y ago
> 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. Maybe I'm stretching the definition, but the exhaustive search is also a proof, especially when it can be done quickly or an efficient proof certificate can be generated (enough.c is the former). I even think that enough.c can be modified to generate a reasonably sized trace to aid verification.
- nigeltao 3y ago
  As an intellectual 'puzzle', I'd be curious to see what that sort of trace-guided verification could look like, if that's even feasible. My recollection of enough.c is that, algorithmically, it's sufficiently complicated that I need to really think hard when I'm reading the code. But also, it uses clever data structures specifically to reduce the memory requirements at runtime. In comparison, "array size is always 1024, array index is always bitwise-anded with 1023, therefore always in-bounds" is undeniably simple and, per "The Fastest, Safest PNG Decoder in the World", practical and fast.
  - lifthrasiir 3y ago
    While I agree that you don't need the tight bound (especially because I think the tight bound for incomplete trees is not much higher than one for complete trees), you do need to be confident that 1024 is either a loose but correct bound or highly unlikely to be reached in practice. So you need to calculate some kind of bounds anyway... And this is another reason I thought something more than Wuffs is desirable [1]; a dynamic memory allocation, when allowed, makes many things easier to implement and prove. [1] https://news.ycombinator.com/item?id=37480019 https://news.ycombinator.com/item?id=37480019
    - nigeltao 3y ago
      1024 is a loose but correct bound. That's what enough.c (or script/print-deflate-huff-table-size.go) says. Stepping back, I'm not sure if I understand what you're saying. Perhaps we're just disagreeing on how "formal" (as in, part of a "formal verification" process) the enough.c program (or equivalent) needs to be? --- As for dynamic memory allocation, Wuffs has a mechanism for the callee (Wuffs code) to tell the caller (C/C++ glue code) that it needs N bytes of "scratch space" or "work buffer", where N is dynamically dependent (e.g. dependent on the image dimensions in pixels). It's not "dynamic memory allocation" in that Wuffs still doesn't malloc/new and free/delete per se. But it is dynamically (run time, not compile time) sized. Grepping for "work buffer" or "workbuf" in Wuffs' example/ or std/ code (or SkWuffsCodec.cpp) should give some leads, if you want to study some code. The workbuf_len is often zero but, for Wuffs' std/jpeg and std/png, it is positive. Manage the work buffer in the same way as the pixel buffer: it's always caller-owned and callee-borrowed.

lifthrasiir 3y ago

> 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. Maybe I'm stretching the definition, but the exhaustive search is also a proof, especially when it can be done quickly or an efficient proof certificate can be generated (enough.c is the former). I even think that enough.c can be modified to generate a reasonably sized trace to aid verification.

nigeltao 3y ago
As an intellectual 'puzzle', I'd be curious to see what that sort of trace-guided verification could look like, if that's even feasible. My recollection of enough.c is that, algorithmically, it's sufficiently complicated that I need to really think hard when I'm reading the code. But also, it uses clever data structures specifically to reduce the memory requirements at runtime. In comparison, "array size is always 1024, array index is always bitwise-anded with 1023, therefore always in-bounds" is undeniably simple and, per "The Fastest, Safest PNG Decoder in the World", practical and fast.
- lifthrasiir 3y ago
  While I agree that you don't need the tight bound (especially because I think the tight bound for incomplete trees is not much higher than one for complete trees), you do need to be confident that 1024 is either a loose but correct bound or highly unlikely to be reached in practice. So you need to calculate some kind of bounds anyway... And this is another reason I thought something more than Wuffs is desirable [1]; a dynamic memory allocation, when allowed, makes many things easier to implement and prove. [1] https://news.ycombinator.com/item?id=37480019 https://news.ycombinator.com/item?id=37480019
  - nigeltao 3y ago
    1024 is a loose but correct bound. That's what enough.c (or script/print-deflate-huff-table-size.go) says. Stepping back, I'm not sure if I understand what you're saying. Perhaps we're just disagreeing on how "formal" (as in, part of a "formal verification" process) the enough.c program (or equivalent) needs to be? --- As for dynamic memory allocation, Wuffs has a mechanism for the callee (Wuffs code) to tell the caller (C/C++ glue code) that it needs N bytes of "scratch space" or "work buffer", where N is dynamically dependent (e.g. dependent on the image dimensions in pixels). It's not "dynamic memory allocation" in that Wuffs still doesn't malloc/new and free/delete per se. But it is dynamically (run time, not compile time) sized. Grepping for "work buffer" or "workbuf" in Wuffs' example/ or std/ code (or SkWuffsCodec.cpp) should give some leads, if you want to study some code. The workbuf_len is often zero but, for Wuffs' std/jpeg and std/png, it is positive. Manage the work buffer in the same way as the pixel buffer: it's always caller-owned and callee-borrowed.