[anyfoo]

This again.

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.

[lifthrasiir]

> Strong type systems can give provably correct code.

"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.

[anyfoo]

I did not claim that everything about the code was proven correct, but a subset of properties expressable by the type system.

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.

[robertlagrant]

> Strong type systems can give provably correct code

^ I think this is where you seemed to claim that everything about the code was proven correct.

[kentonv]

> Strong type systems can give provably correct code.

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...)

[anyfoo]

Yeah, anything can be implemented incorrectly. My point was specifically that ignoring memory safe languages in favor of post-exploit mitigation is foolish, not that the latter is useless.

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.

[lmm]

> In theory, perhaps. In practice, the compiler / runtime will have bugs.

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.

[0x53]

What does provably correct mean here? I think you mean that the code doesn’t have any memory corruption vulnerabilities. However, that is only one class of vulnerability, so more techniques then just relying on a memory safe language are required for secure software.

[anyfoo]

It means that the type system can prove certain properties for you. For example, in languages with dependent type systems like Agda, you can construct a sorted list type that the compiler will prove it sorted at all times, otherwise it won’t compile. Or a complex tree type that is always balanced. Or a set of only even numbers, and again it won’t compile otherwise…

(Sadly, if you go that far, it isn’t generally Turing complete anymore. Though in some cases that’s a good thing.)