3 ms·

To me, this bug is most similar to the Timsort bug back in 2015 [1]. Timsort is an ingenious hybrid sorting algorithm originated from CPython and many implemen

To me, this bug is most similar to the Timsort bug back in 2015 [1]. Timsort is an ingenious hybrid sorting algorithm originated from CPython and many implementations including OpenJDK adopted it mostly via a source-by-source translation. Timsort particularly maintains a stack of sorted runs, and due to the construction there is a small enough finite limit in the maximum possible stack size. However the original CPython implementation didn't exactly match what was proven, so there were rare cases where stack overflow could happen. So this was a serious security bug in CPython, but wasn't in OpenJDK because Java instead threw an exception in that case. Similarly, this WebP bug occurred because the largest table size was formally proven but it didn't match what was fed to the source code. This kind of bugs is not only hard to verify but also hard to review, because of course there is a proof and the source code seems to match the proof, so it should be okay! This bug suggests strong needs for approachable formal verification, including the use of memory-safe languages (type systems can be regarded as a weak form of formal verification), not human reviews. [1] http://envisage-project.eu/wp-content/uploads/2015/02/sorting.pdf http://envisage-project.eu/wp-content/uploads/2015/02/sortin...

3abiton 3y ago
TIL Stack Overflow is not just the name of a website.
- defrost 3y ago
  If that's a serious TIL then you might enjoy the Ye Olde Timey classic Smashing The Stack For Fun And Profit (1996) (OG Phrack link) http://phrack.org/issues/49/14.html http://phrack.org/issues/49/14.html (Text-zine) (TISM Berkeley CS coursework) https://inst.eecs.berkeley.edu/~cs161/fa08/papers/stack_smashing.pdf https://inst.eecs.berkeley.edu/~cs161/fa08/papers/stack_smas... (PDF)
  - tedunangst 3y ago
    But unrelated to the stack overflow in Tim sort.
    - defrost 3y ago
      Not entirely - I wrote a lot of numerical backend code intended for 24/7/365 continuous use in the face of potentially any input .. aquisition | instrumentation equipment failures can produce glitch inputs just as damaging as delibrately crafted malicious inputs from a hacker reverse engineering existing code. The common ground being code that has to be robust in the face of any input has to be (correctly!) verified, constrained within hard resource limits, have graceful fail over behaviour, some measure of sanity checking, etc. Otherwise, if an e\/il hax0r doesn't get you .. mother nature and sheer bloody chance will.
- seabass-labrax 3y ago
  I would really recommend trying to write a little C program that deliberately causes a stack overflow. It is completely harmless and is good fun if you've never encountered this kind of low-level systems code before. It's also pretty fun to try asking for weird amounts of memory with 'malloc' or seeing how many times you can ask the OS for no memory before something fails. You might need to force-reboot your computer after that though!
tialaramex 3y ago
Specifically, since performance is crucial for this type of work, it should be written in WUFFS. WUFFS doesn't emit bounds checks (as Java does and as Rust would where it's unclear why something should be in bounds at runtime) it just rejects programs where it can't see why the indexes are in-bounds. https://github.com/google/wuffs https://github.com/google/wuffs You can explicitly write the same checks and meet this requirement, but chances are since you believe you're producing a high performance piece of software which doesn't need checks you'll instead be pulled up by the fact the WUFFS tooling won't accept your code and discover you got it wrong. This is weaker than full blown formal verification, but not for the purpose we care about in program safety, thus a big improvement on humans writing LGTM.
- lifthrasiir 3y ago
  Yeah, Wuffs can be classified as memory-safe languages in this case and should be endorsed as much as possible. I mean, I said a lot about the limitation of Wuffs in the last conversation, but that's because I believe something like Wuffs should be used more widely, and the current limitation of Wuffs can hinder the progress. We need several angles of attack to make it real, and Wuffs is only one of them.
- nigeltao 3y ago
  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".
user3939382 3y ago
> type systems can be regarded as a weak form of formal verification Depends on the type system, right? I was recently looking at Idris which is a general purpose programming language but apparently can be used for proofs.

3abiton 3y ago

TIL Stack Overflow is not just the name of a website.

defrost 3y ago
If that's a serious TIL then you might enjoy the Ye Olde Timey classic Smashing The Stack For Fun And Profit (1996) (OG Phrack link) http://phrack.org/issues/49/14.html http://phrack.org/issues/49/14.html (Text-zine) (TISM Berkeley CS coursework) https://inst.eecs.berkeley.edu/~cs161/fa08/papers/stack_smashing.pdf https://inst.eecs.berkeley.edu/~cs161/fa08/papers/stack_smas... (PDF)
- tedunangst 3y ago
  But unrelated to the stack overflow in Tim sort.
  - defrost 3y ago
    Not entirely - I wrote a lot of numerical backend code intended for 24/7/365 continuous use in the face of potentially any input .. aquisition | instrumentation equipment failures can produce glitch inputs just as damaging as delibrately crafted malicious inputs from a hacker reverse engineering existing code. The common ground being code that has to be robust in the face of any input has to be (correctly!) verified, constrained within hard resource limits, have graceful fail over behaviour, some measure of sanity checking, etc. Otherwise, if an e\/il hax0r doesn't get you .. mother nature and sheer bloody chance will.
seabass-labrax 3y ago
I would really recommend trying to write a little C program that deliberately causes a stack overflow. It is completely harmless and is good fun if you've never encountered this kind of low-level systems code before. It's also pretty fun to try asking for weird amounts of memory with 'malloc' or seeing how many times you can ask the OS for no memory before something fails. You might need to force-reboot your computer after that though!

tialaramex 3y ago

Specifically, since performance is crucial for this type of work, it should be written in WUFFS. WUFFS doesn't emit bounds checks (as Java does and as Rust would where it's unclear why something should be in bounds at runtime) it just rejects programs where it can't see why the indexes are in-bounds. https://github.com/google/wuffs https://github.com/google/wuffs You can explicitly write the same checks and meet this requirement, but chances are since you believe you're producing a high performance piece of software which doesn't need checks you'll instead be pulled up by the fact the WUFFS tooling won't accept your code and discover you got it wrong. This is weaker than full blown formal verification, but not for the purpose we care about in program safety, thus a big improvement on humans writing LGTM.

lifthrasiir 3y ago
Yeah, Wuffs can be classified as memory-safe languages in this case and should be endorsed as much as possible. I mean, I said a lot about the limitation of Wuffs in the last conversation, but that's because I believe something like Wuffs should be used more widely, and the current limitation of Wuffs can hinder the progress. We need several angles of attack to make it real, and Wuffs is only one of them.
nigeltao 3y ago
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".

user3939382 3y ago

> type systems can be regarded as a weak form of formal verification Depends on the type system, right? I was recently looking at Idris which is a general purpose programming language but apparently can be used for proofs.