The WebP 0day
blog.isosceles.com
blog.isosceles.com
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/sortin...
Smashing The Stack For Fun And Profit (1996)
(OG Phrack link) http://phrack.org/issues/49/14.html (Text-zine)
(TISM Berkeley CS coursework) https://inst.eecs.berkeley.edu/~cs161/fa08/papers/stack_smas... (PDF)
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.
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!
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.
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".
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.
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.
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.
Ah, I think I misremembered that bit of Wuffs code, specifically around `HUFFS_TABLE_SIZE`. The comment does mention enough.c but I thought `HUFFS_TABLE_SIZE` was also set to the tight bound found by it, which was not the case, and wondered why you seemed to downplay the importance of enough.c verification. I agree that you don't need any additional verification in the current code.
> 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).
Isn't it fixed during the decoding process though? If my understanding is correct `decode_frame` is not supposed to change what `workbuf_len` will return later (or examples don't account for them yet). Technically speaking you can already use the suspend mechanism to request a memory allocation of any size, so it is more about a matter of public API, but such code would be very regular and repetitive. I thought a limited mechanism to enable an in-situ dynamic allocation---preferably desugared---might improve a usability a lot.
For Wuffs' image decoding, it's flexible up until decode_image_config returns. It's fixed afterwards.
In practice, that works fine for BMP, GIF, JPEG and PNG (and I'm confident will work for WebP too). No in-situ dynamic allocation (with or without sugar) needed. Even though, for the libjpeg-turbo C code, `grep mem..alloc_ jd*.c | wc -l` shows more than 50 "allocation" call sites, Wuffs' JPEG decoder does just fine with just the one work buffer.
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.
Why is the logo (https://raw.githubusercontent.com/google/wuffs/main/doc/logo...) no longer shown in the readme?
I was pretty sure I had heard of the project before but I had to find the logo to be absolutely certain, it's truly one of a kind.
For a demo, see "Scrap your Bounds Checks with Liquid Haskell", giving a 6x speed up in high-performance parsing of UDP packets.
[1]: https://news.ycombinator.com/item?id=37349276 "A Gentle Introduction to Liquid Types"
[2]: https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell"
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.
It can be quite a bit of work to recreate a POC of the exploit even knowing the location and the fix.
A lossless decompressor in an image decoder can be quite fuzzing resistant.
Maybe obvious to security people but fun to read about as a muggle.
I'm sure you're right about that.'Fuzzing resistant, takes human-directed fuzzing to recreate a PoC' seemed fun, but, as you say, that's the magic of memory unsafety.
1. Are other Chrome-based browsers (e.g. Brave) affected by this?
2. Is desktop Chrome affected, or is this purely a mobile thing?
3. Why haven't I heard of WebP before? Am I living under a rock, or is this a mobile-first technology?
Source? I've roundtripped bitmap->WebP->bitmap and got the same bits out
Why do I see WebP as an image format used to sneakily degrade PNG files? I've seen gaming wikis and CDNs serve PNG URLs as lossy WebP, ruining pixel art and degrading color detail in 2D art. And Discord CDN's "file.webp?size=1024&quality=lossless" serves icons/emotes with chroma subsampling (and ffprobe doesn't say the file is lossless, unlike test.webp above).
> today, not sure in the past
Dunno about ffmpeg, but the official library supported lossless encoding a decade ago
> Why do I see WebP as an image format used to sneakily degrade PNG files?
Why does Twitter reencode PNG to JPEG even when this results in larger file sizes and terrible quality for 2D art and technical drawings? All the services you've listed are free and they all cater to the lowest common denominator. They'll never use lossless WebP by default for the same reason they won't use PNG. Lossless media is virtually unheard-of outside our bubbles. If you're lucky there will be a "download original" button
It's been supported in desktop chrome for a long while. There's dozens of JPEG replacements that have come and gone, and WebP is primarily notable for having Google's clout behind it. When Google bought Duck/On2 they got a lot of video compression technology, some of which went into WebP.
Chrome desktop was affected as well, both on Linux and Windows. Chrome bundles its own version of libwebp, so even if your Linux distribution hasn't patched yet, as long as Chrome is up-to-date you should be OK (in terms of browser attacks at least).
There's lots of wonderfully obscure image file formats that are supported by the major browsers and operating systems. For example you can load a KTX2 file (Khronos Texture Container) on MacOS, or a DNG file (Adobe Digital Negative) on Android. Lots of interesting and highly exposed attack surface for attackers to explore.
Not MacOS though?
Also for corporate users this is a pain as you have to update Safari via Software Update unlike browsers like Chrome which automatically update.
Safari:
https://support.apple.com/en-us/HT213930
MacOS:
https://support.apple.com/en-us/HT213906
The bug is in the codec library, and WebP has implementation monoculture, so everyone uses the same library, and everyone needs to patch.
3. Google tried to make WebP a thing 10 years ago, but it didn't get much traction, since it was Chrome-only for a long time. It never got properly standardized (it is open source tho). It compresses low-quality images better than JPEG, but tends to blur and smear colors in higher-quality images.
Ironically WebP became widely supported at the same time when it became technically obsoleted by AVIF and JPEG XL.
It is a libwebp vuln right? So anyone that does not link to libwebp is or may be ok.
Aha! Finally the day has come when KDE's Dolphin emerges as the most secure file manager, in a "this sign can't stop me because I can't read" fashion.
All the proprietary software with their own bundled versions of electron or vendored libraries, etc. on the other hand...
That and every snap/flatpack/etc. package, every container image you are using and possibly pip packages that can come with and compile all kinds of dependencies and haven't been maintained for ten years...
The security benefit a well maintained Linux distro provides has been eroding for years now.
I think there are two problems:
1. people running single/small numbers of servers copying practices that are used by people running fleets of containers who can have someone promptly updating everything has needed. 2. As always, convenience. The easiest and best supported way to pip install things is without --system-site-packages.
I have always felt we were going the wrong way with this. I thought I was the only one!
Firefox very quickly implemented WebP when YouTube (a Google property) added support for animated WebP based hover thumbnails.
Firefox and Safari only caved years later once Chrome-only WebP-only websites were too common to ignore.
WebP is gaining popularity as replacement for JPEG, I'm surprised you haven't stumbled it on yet, cause more and more images I download from the web turn out to be WebP.
Fixed[1] in Firefox 117.0.1 as well as some ESR and Thunderbird versions.
[1]: https://www.mozilla.org/en-US/security/advisories/mfsa2023-4...
This support has always been overstated. Photoshop still doesn’t support it, you encounter other weirdness like Apple Preview.app can view them but not edit them.
Preview.app is the exception to the rule, but it still has acceptable UX. After you finish drawing the first brush stroke on a WebP file, it will ask you to reopen the edited file as a tiff before you continue editing. No loss of data or functionality
Or will updating the SMS App, Chrome, WhatsApp, Signal etc be sufficient to cover all the likely input routes?
Updating Chrome on an unsupported device would fix the issue, but you would still need an Android OS upgrade to fix the issue for apps like Signal and WhatsApp. Chrome bundles its own version of libwebp, but messaging apps and other highly exposed stuff like Gmail all use the OS provided interfaces for displaying images. Hopefully we'll start getting updates for security-supported Android devices in early October.
Nice of Google to drop security support for the Pixel 4a just before this bug drops.
It’s just icing on the proverbial cake that a month after they drop security support for the 4a a 0-click remote exploit is found.
Or the app could bundle the library, they can push updates faster but then again they could just use an old version and never update like most 3rd party dependencies these days.
The argument of a $1000 Androd phone vs a $1500 iPhone falls over if you have to replace that Android phone 2 more times in the same period.
If the target is an Android, definitely an advanced exploit like this isn’t needed, so even if it will work, an easier ones most likely to be used.
Considering there are over 3 billion active Android users according to Google [2], that's at least 834 million people who are potentially vulnerable to this exploit that will likely never receive a patch. That's awful enough by itself, but particularly terrible since the exploit could be as simple as having someone view an image. Chrome may be fixed, but there are over 2 billion WhatsApp users. [3]
1. https://www.androidauthority.com/wp-content/uploads/2023/06/...
2. https://www.theverge.com/2021/5/18/22440813/android-devices-...
“Native image decoder - New NDK APIs let apps decode and encode images (such as JPEG, PNG, WebP) from native code for graphics or post processing, while retaining a smaller APK size since you don’t need to bundle an external library. The native decoder also takes advantage of Android’s process for ongoing platform security updates. See the NDK sample code for examples.”
However, poking about in the Android mainline module docs I can find no evidence that the image decoder libraries are included in the system updates that get pushed through Google Play. I’ve unpacked the obvious modules & found the video codecs, but no sign whatsoever of the image decoder libraries,
It would be helpful to be able to tell whether a given phone has received such an update, especially in the case of 0-click exploits like this one! Are all Android 11+ phones guaranteed to receive it? (it would seem so, if this is a core security component) Is there anyway to tell whether you’ve received it? This aspect of Android updates seems to be entirely opaque to the end user - updates get pushed through Google Play services & that’s it.
After some investigation, I found https://support.google.com/product-documentation/answer/1141...
which gives some details of Android system updates pushed through Google Play. This changelog does not list CVEs or specific bugfixes, so it’s impossible to tell which bugs have been closed via this route, but it is at least slightly better than nothing at all.
It is possible to map those updates to actual CVEs mentioned in the AOSP sources via a circuitous route involving adb & running a bunch of commands on your phone, according to this blog post: https://www.esper.io/blog/building-a-google-play-system-upda...
Looking at the current AOSP wepb sources, no module tags have been attached to the current release, so it doesn’t look like it’s been pushed out yet, if it’s possible for Google to do so at all outside the monthly security updates for in-support phones.
It sounds like the exploit was triggered in another process by iMessage forwarding the post-parse attachment content to that process - the blog post says this is passkit related so I assume any app that has passkit interaction could do this. iMessage is simply universally available so why use a different medium.
Not doing so is a disservice to their customers frankly.
They're currently bugging me about updating a 9 year old ipad I just use as a kindle. They flatly blow Google away on device updates, and will continue to do so even if Google isn't lying about their new / supposed 5 year update plan (and NB: that's 5 years from the release date, not 5 years from the last sale date, which could be reasonable.)
This looks like the generalized version of the problem...
In other words, you have Software A, it generates a lookup table B which is then used to process an input stream of data.
Now the responsibility shifts to you as a software developer (if you care even a little bit about security/correctness of your code) -- to either assert that:
A) The software is written in such a way that there are NO possible cases of input data misusing/failing the lookup table, or
B) The software will only be used in a controlled environment (i.e., point to point communication where both communicants are trusted) such that the stream is guaranteed never to contain data that misuses/fails/causes anomalies with the lookup table.
Since B is all-but-impossible for anything other than a small group or office, that is, truly impossible on the Internet scale, that leaves only A).
Thus, the generalized "best practice" for present or future Software Engineering, can be summarized as follows:
If a lookup table is used in someone's software for whatever reasons -- then then the responsibility goes to the software developer(s) to assert that that lookup table functions correctly and for all types or data, OR that the software detects and appropriately handles erroneous data BEFORE it gets to the lookup table...
In fact, if I were a serious security researcher and had the time -- I'd collect a list of ALL reported security vulnerabilities in the past that had to do, one way or another with lookup tables...
Then I'd read through them, one by one, and compare them for generalities.
I'm guessing (but not knowing) -- that there is a pattern there...
Then I'd go through all software that used lookup tables on streams of data in one way or another -- and audit ALL of them for security vulnerabilities.
Now, clearly this is not a task for one man in one lifetime...
This is a "team sport"...
But if I were a serious security vulnerability researcher -- that is the generalized path that I would take...
Many memory safety bugs can be found by fuzzing code as a black box. Fuzzing is used by code authors too, because even people who wrote the source code don't fully understand what edge cases exist based on the source code! If the code has Undefined Behavior bugs, then the source code may not even match what the actual program does.
There are good decompilers, and as I've mentioned, writing an exploit will necessary depend on working with compiled code — you must know what's in memory, on the stack, and where "gadgets" are the exploit can jump to. This information is not present in the source code. Deep understanding of compiled code is a prerequisite for writing an exploit.
Bugs have been found in closed-source Windows for as long as it existed. Even the recent attack on Apple Messages combined this bug with a bug in Apple's closed-source sandbox. Security by obscurity has always been tempting, and never worked as well as hoped.
I've read the JPEG spec (and written a decoder) before, so I decided to look at the WebP spec: https://developers.google.com/speed/webp/docs/webp_lossless_...
The important information is in section 6. The first thing I notice is that it's not very clear how the codes are constructed, unlike the JPEG one (which actually has a ton of very readable flowcharts on the process), but it appears to be similar to LZH/deflate(zlib). The "specification" looks more like a selected set of source code fragments with accompanying descriptions.
Perhaps I should try writing a WebP decoder too, having already done GIF, JPEG, and PNG, but based on the above "specification", it's almost as if they don't want you to.
I agree the specification really lacks examples, but it explicitly states that it uses canonical Huffman trees so that only code lengths have to be transmitted. I think this is clear enough to pinpoint the actual tree. (I don't think there is any canonical Huffman tree implementation that uses the inverse lexicographical order.)
> This is a decades-old technology that should've had the bugs worked out of its many implementations by now and there are also countless articles about how to implement it.
Because there are many implementations of Huffman trees with different trade-offs? Charles Bloom once said that the definitive 1997 paper on Huffman optimizations [1] is still not well known at that point (2010) and many optimizations were rediscovered and then forgotten, so there should be many inefficient implementations out there.
[1] https://cbloomrants.blogspot.com/2010/08/08-12-10-lost-huffm...
If one is concerned about this as an end user, I've seen some extensions that block webp and try to request a png/jpg/etc. version from the host.
I can't attest to how effective it is as I didn't use it long. But it worked with some of the big image hosting sites like imgur.
For me, this was just so I was able to download images in a usable format. Most OSs can't treat webp like normal images, like generating thumbnails or opening a preview app.
That was a few years ago though so maybe things have changed.
It just sounds like typical growing pains from using non-safe languages (C).
I get the appeal for browser speeds, but I really wish we as an industry could move away from methods that encourage the same mistakes we've been making since we started writing in C.
It feels like we're using self tapping screws to build a bridge instead of rivets because it's faster. And we can just keep adding more screws if the bridge starts to sag.
Excuse me? It is Google that assigned this as Chrome only. Over the last 7 days alone every single major Linux distribution has had to push an update (including Red Hat which assigned this a 9.6 score), and Docker images like Python which has over 1 billion pulls, not to mention Puppeteer(hello?), WordPress, Node.js, etc. and CRBug is still private to this day.
I am not being condescending but sites like BleepingComputer reported this as they saw it rather than doing any investigation. And the same goes for a lot of security companies that reported on this issue in third person. It’s really difficult to foster trust when you know that the person on the other side hasn’t bothered to do any due diligence.
Adam Caudill (1Password was one of the first to patch it) did a nice blog post, “Whose CVE is it anyway?”[0] highlighting the issue I am talking about in my comment.
Citizen Lab has refused to comment on whether both are related, but it doesn’t take a genius does it…
[0]: https://adamcaudill.com/2023/09/14/whose-cve-is-it-anyway/
The author mentions that many other systems need to patch as well. However, wow many of those billion Python docker pulls are rendering untrusted WebP images? Same for Node, etc. These should also be promptly patched, but they're not in the same ballpark here as iOS/Android/Chrome.
I'm sorry but I call for libraries used by millions around the world to NOT use C. And I love C... But this risk ratio is off the charts and they ought to not use C for such critical libraries.
Even as a C guru, you are going to make a mistake, at some point.
I think this is the fix https://github.com/webmproject/libwebp/commit/dce8397fec159c...
"malloc fail"? :facepalm: (oh yes, Slack, Discord, Teams, everything is affected, including all modern OS).
[0]: https://security-tracker.debian.org/tracker/CVE-2023-4863
!?!
C/C++ as well as dynamic languages create huge surfaces of undefined behavior and subtle bugs that are too difficult to lint and too burdensome for even the most astute coders.
Fundamental libraries should also be formally verified in a manner similar to seL4.
Also, another problem is a pervasive attitude of unprofessionalism and dismissiveness of rigor, quality, correctness, and security in FOSS. The current approach of building empires on quicksand is foolish.
Problem is, sandboxing is harder to implement so it's often done suboptimally or not at all.
The nice thing about sandboxing and fuzzing can be applied to existing code.
Google Chrome also implements sandboxing and many areas. It's not feasible everywhere. So for new code / libraries we should default to a memory-safe language.
But realistically that only solves a tiny fraction of the problem, since realistically new greenfield projects started today will likely take 10+ years to become widely used, if they do at all.
WebP was written at a time when C/C++ was still the only viable language in which to write an image compression library. Saying "things like this should be written in Rust!" just doesn't actually do anything to make software like WebP secure. Improving fuzzers and sandboxing might.
I'm pretty sure that even now a lot speaks against using rust for greenfield projects precisely for that reason: few people want to integrate Rust into their build chain. You basically always have to have a compiler that's 1 release old or otherwise you cannot compile new Rust software like the very widely used time crate.
If you are a new and unproven format, do you really want to bear that hit? You could make two implementations, one in C and one in Rust, but that will mean you spread your probably quite scarce engineers over two projects.
He’s certainly aware of memory safe programming.
For dav1d I heard that one of the reasons why C was chosen was precisely this portability concern. format decoders are usually quite low level components and can get integrated into all sorts of environments. I'm sure there is someone out there who made a visual studio project with a 3 year old VS version with dav1d inside for some embedded project. For such devs, Rust is a way harder sell.
You basically always have to have a compiler that's 1 release
old or otherwise you cannot compile new Rust software like the
very widely used time crate.
That's an interesting example as the time crate stagnated for quite a while and even the current version only requires Rust 1.67 or newer. The current Rust version is 1.72.Strong type systems can give provably correct code. For trusted code (e.g. not third party code), sandboxing is a post-exploit mitigation. And such a post-exploit mitigation cannot necessarily guard against any class of bugs that (at least in some aspect) provably correct code can.
Yes, of course privilege separation as much as possible is still extremely valuable, but to say that sandboxing is a "better" solution, implying that one should not pursue provable correct code in favor of post-exploit mitigation, is a harsh liability. It's the same as the "oh, we don't need to use a type safe language, we have unit tests"-crowd, only worse.
In theory, perhaps. In practice, the compiler / runtime will have bugs. So you still need a sandboxing layer. Best to do both.
(The sandbox will have bugs too. But if you have two layers, hopefully it's hard for attackers to get ahold of zero days for both at the same time...)
They probably won't. The trusted kernel for these systems is tiny; a sandbox is orders of magnitude more complex with orders of magnitude more chances for bugs to creep in.
But in practice, type systems can be proven to be sound, implementations of type checkers can be proven correct, and while it’s still possible to make mistakes there, that isn’t so much an issue in mathematics, simply because of how rigorous it is. This does not just include type systems, there’s even an effort to rebase the foundation of mathematics on a type system instead of set theory!
In other words, we likely agree that steel vaults can have holes. But we probably also agree that an average steel vault is better in keeping things in or out of it than a velvet curtain.
(Sadly, if you go that far, it isn’t generally Turing complete anymore. Though in some cases that’s a good thing.)
"Sound" [1] type systems only guarantee the absence of some class of bugs as well. There are a lot of bug classes that remain exploitable. Memory safety happens to be a low-hanging fruit because many existing softwares are not even written in such languages.
[1] "Strong" type systems generally refer to the intolerance towards implicit type conversions or memory unsafety, and that alone doesn't make type systems provably safe in some sense.
I agree that using the word “strong” was wrong. I basically meant it in the sense of “good”/“elaborate”, mistakenly ignoring that “strong” already has a very specific meaning in type systems. Thanks for correcting.
^ I think this is where you seemed to claim that everything about the code was proven correct.
Memory safety could solve the problem altogether, but then again no program is 100% memory safe, there's always some kind of primitive that uses memory-unsafe code under the hood, so it's not perfect either.
The “perfect” solution would probably be:
- use memory safe languages
- all primitives using memory unsafe stuff should get formally verified
Rust is kind of aiming at this (with things like [1] and [2]), but it's not there yet.
[1]: https://dl.acm.org/doi/pdf/10.1145/3158154 [2]: https://github.com/rust-secure-code/safety-dance
[1] https://security.googleblog.com/2021/02/mitigating-memory-sa...
Nah. Dynamic languages don't actually have types (even if they have something that they call types), and even typed-but-GCed languages often don't really use the types for memory safety.
Any dynamic language that has a string type has something similar to (for example) a buffer and a length associated with it internally. You can formalize that from the compiler’s perspective, even if you don’t expose it to the outside.
You could argue that the language doesn’t necessarily have memory safety associated with its types, because a compliant compiler or interpreter could represent strings in any way it chooses, and on some academic level there’s merit to that, but in practice you’d be rather stupid to implement the string value type in an interpreter or compiler for a language with a common string type in a memory unsafe way.
I'm just trying to point out a bigger issue with software, in my opinion. Even more so when talking about the standard implementation of an image format as big as this. It really puts a lot into perspective on how bad software is commonly designed.
My DivestOS 14.1 (A7) through 19.1 (A12) has this patched, and 20.0 (A13) is currently compiling: https://divestos.org/pages/news#2023-09.2
GrapheneOS shipped it: https://grapheneos.org/releases#2023091800
CalyxOS has it staged for next update: https://review.calyxos.org/c/CalyxOS/platform_external_webp/...
LineageOS 18.1+ also pulled it in: https://review.lineageos.org/q/topic:%22CVE-2023-4863%22
Additionally all of the above have shipped Chromium 117.0.5938.60 which contained the same fix as well: https://divestos.org/misc/ch-dates.txt
And yet another argument for "You ought to be using Qubes." Random web access needs to be treated as "Genuinely high risk" anymore. A disposable VM with nothing of value in it for "casual web use" seems the right option for exploring the security hostile environment of "the internet."
Eh, I think it's a good bit harder to escape a HVM isolated virtual machine than a sandbox. At least, I'm not aware of many cross-Xen VM escapes.
My most valuable stuff (passwords, bank accounts, logins) is accessible from the browser. You'd need to somehow sandbox and frequently destroy/restore the rendering and javascript engine to avoid leaking this information cross site while having a fairly strict firewall between those and the external browser. (IE: cookie/session/password storage).
It's "A range of VMs, with different browsers in them, for different purposes."
My "random web use" browser VMs don't have anything in them - they're ephemeral. If I need a password, I copy it from another VM over. If you escape into that VM, you might be able to grab a password being pasted, but I don't access anything I consider sensitive in them - just random forum accounts, etc. And it's easy enough to spin up other disposable VMs for stuff in Qubes (I actually mostly browse through the Tor network, to add traffic to it).
So, for your use case, you'd have one VM with your "core" stuff - passwords, logged in to webmail, banking. And then you do everything else web related in a different VM.
Probably a good solution for the highly technical, not something I could ever propose to my mother.
For Qubes specifically she can understand theres a bank Qube and a Facebook Qube and a nothing-special Qubes and its all color coordinated. She doesn't even need to know they are VMs, they're just color coded windows
So Qubes won't help you everywhere, and the WebP decoder is everywhere.
Updating the OS-wide datatype means all apps are updated, not just the browser. Why is this STILL not the case on supposedly modern OSes these days?
Having some insecure unaudited badly written codec is fine for a lot of use cases because it operates on trusted data. But this is of course quite a different situation than being exposed to all webpages you visit.
The Amiga 3000 lived in a different world with a different internet.
One place where macOS allows arbitrary codecs is Quicklook plugins, but these are designed to run in a separate process. It'd be wise to implement image codecs the same way, but so far they're typically a library linked in the same process.
They also used to let you just embed a Quartz Composer file which let you do some "fun" stuff with the webcam that would terrify users.
I've been following the progress of some of the fixes in apps I use and it's meandering through intermediates at an urgency that is more akin to the ssh 9.1p1 vulnerability which required peopel to ssh into an affected server.
Basically, don’t rest easy and get complacent. Updating the OS distros is not enough.
$ flatpak update --no-related --force remove
Checking for updates...
Nothing to do.
My base system (Debian) got the patch almost two weeks ago. Might as well trash flatpak for good.
Had Microsoft done this the tech world would be up in arms. When Google does it, it's OK.
I have to add extensions to convert this crap when I want to download images. I hope that Google loses their dominance to Microsoft with AI.
And in the past, they tried to shove Windows Media Video and Audio down our throats, which are inferior relatives of MPEG-4, AAC, FLAC, etc.