Problem is, sandboxing is harder to implement so it's often done suboptimally or not at all.
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.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
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.