3 ms·

> Moreover, verification is done with respect to specific properties that ensure no attacks of a particular kind. No. seL4 proved functional correctness. It el

> Moreover, verification is done with respect to specific properties that ensure no attacks of a particular kind. No. seL4 proved functional correctness. It eliminates all attacks, not just particular kinds. Functional correctness means implementation matches specification. As a corollary, seL4 has no buffer overflows. Proof: Assume seL4 has a buffer overflow. Exploit it to run arbitrary code. Arbitrary code execution is not part of specification, hence implementation does not match specification, leading to contradiction. QED. Above proof applies to use after free, or any other exploits enabling arbitrary code execution, including methods which are not discovered yet.

burntsushi 8y ago
I read this and thought, "this can't be right, they must be assuming some things." According to them, they, sensibly, are indeed assuming some things to be correct without proof: http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml This is effectively the same idea behind Rust's `unsafe`. It represents the things you assume to be true. Of course, when compared to seL4, the scales are massively different. :-)
pron 8y ago
Formal proofs prove certain theorems about your programs. If you could formalize the notion of an arbitrary attack you could prove it's impossible, but there is no such formalization. Of course, you don't need to verify the lack of a certain attack techniques, only their effect, and so you can certainly verify even with respect to undiscovered techniques, but this still would never cover all attacks regardless of their effect. E.g. you may be able to prove no arbitrary code execution, but you may still fail to verify no data leaks. If you have a data leak, you can steal passwords and certifications, and if you have those you can execute arbitrary code without any arbitrary code execution attack or privilege escalation. Note that this could occur even if the kernel is itself impervious to data leaks, due to vulnerabilities in user code. Even with regard to what you do prove, the conclusions depend on certain assumptions about the hardware which, even if true (and they often aren't -- read some of the seL4 caveats) at best hold with high probability, not certainty. I am an avid fan of formal methods, and have been using them quite extensively in the past few years, but you should understand what they can and cannot do. You can read about formal methods on my blog: https://pron.github.io/ https://pron.github.io/ The paper discussed here also mentions some common misunderstandings, about seL4 in particular: http://verse.systems/blog/post/2018-10-02-Proofs-And-Side-Effects/ http://verse.systems/blog/post/2018-10-02-Proofs-And-Side-Ef... Nevertheless, there is no doubt that a kernel such as seL4 has a much lower probability of being hacked than, say, Linux, given similar hacking efforts, and I would trust it much more. But it really isn't an endgame.
sempron64 8y ago
From the assumptions page: http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml ``` Hardware: we assume the hardware works correctly. In practice, this means the hardware is assumed not to be tampered with, and working according to specification. It also means, it must be run within its operating conditions. Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels ``` Rowhammer and Spectre exploits hardware not working to spec. These sorts of attacks using heretofore "unreasonable" exploitation of side-channel and hardware vulnerabilities are exactly what worries me. We have no solutions for these classes of attacks. Complex high-speed systems are still inherently unsolvably vulnerable, it seems.

burntsushi 8y ago

I read this and thought, "this can't be right, they must be assuming some things." According to them, they, sensibly, are indeed assuming some things to be correct without proof: http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml This is effectively the same idea behind Rust's `unsafe`. It represents the things you assume to be true. Of course, when compared to seL4, the scales are massively different. :-)

pron 8y ago

Formal proofs prove certain theorems about your programs. If you could formalize the notion of an arbitrary attack you could prove it's impossible, but there is no such formalization. Of course, you don't need to verify the lack of a certain attack techniques, only their effect, and so you can certainly verify even with respect to undiscovered techniques, but this still would never cover all attacks regardless of their effect. E.g. you may be able to prove no arbitrary code execution, but you may still fail to verify no data leaks. If you have a data leak, you can steal passwords and certifications, and if you have those you can execute arbitrary code without any arbitrary code execution attack or privilege escalation. Note that this could occur even if the kernel is itself impervious to data leaks, due to vulnerabilities in user code. Even with regard to what you do prove, the conclusions depend on certain assumptions about the hardware which, even if true (and they often aren't -- read some of the seL4 caveats) at best hold with high probability, not certainty. I am an avid fan of formal methods, and have been using them quite extensively in the past few years, but you should understand what they can and cannot do. You can read about formal methods on my blog: https://pron.github.io/ https://pron.github.io/ The paper discussed here also mentions some common misunderstandings, about seL4 in particular: http://verse.systems/blog/post/2018-10-02-Proofs-And-Side-Effects/ http://verse.systems/blog/post/2018-10-02-Proofs-And-Side-Ef... Nevertheless, there is no doubt that a kernel such as seL4 has a much lower probability of being hacked than, say, Linux, given similar hacking efforts, and I would trust it much more. But it really isn't an endgame.

sempron64 8y ago

From the assumptions page: http://sel4.systems/Info/FAQ/proof.pml http://sel4.systems/Info/FAQ/proof.pml ``` Hardware: we assume the hardware works correctly. In practice, this means the hardware is assumed not to be tampered with, and working according to specification. It also means, it must be run within its operating conditions. Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels ``` Rowhammer and Spectre exploits hardware not working to spec. These sorts of attacks using heretofore "unreasonable" exploitation of side-channel and hardware vulnerabilities are exactly what worries me. We have no solutions for these classes of attacks. Complex high-speed systems are still inherently unsolvably vulnerable, it seems.