In the introduction "In this post we'll take a look at that sandbox escape. It's notable for using only logic bugs". My understanding was that Rust only cover memory corruption type of bug.
Notably, no language will ever be able to catch pure logic errors by itself. The computer can't and shouldn't try to divine what you meant. It'll only do what it's told.
Now, there are certainly advantages different languages have in ease of writing tests and things like that. There's also formal verification. But unlike memory errors, it's impossible to know if you told the computer to do something you didn't intend.
> Notably, no language will ever be able to catch pure logic errors by itself.
It's true you'll never be able to catch all logic errors automatically, partly because you need full correctness specifications for that.
But languages like Rust with powerful static type systems can catch lots more important logic errors than C, or C++ --- e.g. using typestate (catches bugs with operations on values in incorrect states), affine types (catches bugs with operations on "dead" values), newtypes (e.g. lets you distinguish sanitized vs unsanitized strings), sum types (avoids bugs where "magic values" (e.g. errors) are treated as "normal values").
Also modern languages like Swift, and Rust to a lesser extent, are treating integer overflow as an error instead of just allowing it (or worse, treating it as UB).
typestates are great, but in rust i wonder if it would be more ergonomic and easier to get right if it was officially a feature instead of a pattern you have to implement...?
Amazingly, typestates used to be a headline feature of Rust, in the very, very, very old days. Like, "Wow, Rust is the language that's going to make typestates mainstream!" was a thing people thought when seeing it.
The halting problem doesn't prevent correctness proofs, it only means that you get a three-valued answer: proof, counterexample, or too complex to determine. "Too complex to determine" usually means that the code needs to be rewritten to have simpler structure.
And of course the proof is only for those properties that you write down, and you could also have a bug in the spec for those properties.
I guess that's the true Turing Test, can an artificial general intelligence determine the complexity level and relative risk level of infinite loops for an algorithm written for a Turing machine.
This exploit chain illustrates how once you have obtained a memory corruption primitive it is very hard to prevent full compromise. This makes it more important than ever to limit the ability of attackers to acquire memory corruption primitives.
The best hope for legacy C and C++ code right now is a combination of extensive fuzzing and dynamic analysis to detect as many memory corruption bugs as you can, plus mitigations in CPUs and compilers to make it harder to turn memory corruption bugs into malicious execution, plus sandboxing to limit the damage of malicious execution. This exploit chain demonstrates techniques to bypass that entire mitigation stage (and also shows that Apple severely bungled their sandbox design).
This doesn't bode well for the mitigation approach. They add significant complexity to the silicon and software stack, which has a cost in performance, but also ultimately security --- at some point we will see these mitigations themselves contributing to attack vectors. In return they make exploitation a lot more difficult, but mitigation bypass techniques can often be packaged and reused. For example stack overflow techniques have been effectively mitigated but that doesn't matter to attackers these days, who are now very good at using heap overflow and UAF. Meanwhile those stack overflow mitigations (stack cookies etc) still have to remain in place, making our systems more complex and slower.
For this specific work, any mitigation is much worse than just solving the problem correctly.
The WUFFS code to do this sort of stuff (parse file data, turn it into an array of RGB pixel values) is not only inherently safe, it's also typically faster than you'd write in C or C++ because the safety gives programmers that fearlessness Rust talks about for concurrency. The language is going to catch you every single time you fall, so, you get completely comfortable doing ludicrous acrobatics knowing worst case is a compiler diagnostic or a unit test fails and try again. When you have a hidden array overflow in C++ it's Undefined Behaviour, when you have a hidden array overflow in (safe) Rust it's a runtime Panic, when you have a hidden array overflow in WUFFS that's not a valid WUFFS program, it will not compile now it's not so hidden any more.
So you're right, this doesn't bode well for mitigation - the answer isn't "more complex and slower" but "use the correct tools".
Now, there are certainly advantages different languages have in ease of writing tests and things like that. There's also formal verification. But unlike memory errors, it's impossible to know if you told the computer to do something you didn't intend.