5 ms·

That's not an endgame if the resources required to block an attack are significantly greater than those required to make one. Moreover, verification is done wit

by pron 8y ago

That's not an endgame if the resources required to block an attack are significantly greater than those required to make one. Moreover, verification is done with respect to specific properties that ensure no attacks of a particular kind. The more kinds of attacks you need to defend yourself from, the harder you need to work (and you will miss some). Not saying we're not making steps in the right direction, but no one thinks it's an endgame.

monocasa 8y ago
It's an endgame wrt to memory safety (like I said). sel4 is memory safe. All the other mitigations like ASLR, canaries, etc are just hacks around the fact that proving memory safety of existing codebases is a Sisyphean task. And getting down to 5/1 proof to implemention is within the realm of what unit tests you should be writing anyway, so it's not that much of an economic investment.
- pron 8y ago
  I am not at all against formal verification. In fact, I evangelize it and use it myself quite a bit. But it is important to understand that it is very, very far from being a miracle cure. All software proofs prove correctness of specific theorems about a program given certain axioms. Those axioms must include, at the very least, the conformance of the hardware to some specification. But hardware can, at best, conform to the specification with some probability. For example, when you write `mov rax, [rdx]` it is not true that the computer will, 100% move the contents of the address pointed to by rdx into rax, only that it will do so with some high probability. Therefore, any proof about a software system (as opposed to an algorithm, which is an abstract mathematical entity) is a proof of a theorem of the form, "as long as the system behaves according to my assumptions, it will exhibit behaviors consistent with my conclusions." And that is even assuming that your conclusions cover all possible attacks. As it is generally impossible to formalize the concept of an arbitrary attack, you generally prove something far weaker. But none of this is even the biggest limitation of formal verification. The biggest would be its cost and lack of scalability. seL4 is about 1/5 the size of jQuery, and it is probably the largest piece of software ever verified end-to-end using deductive formal proofs as a verification technique. However much the effort of a similar technique can be reduced, it doesn't scale linearly with the size of the program (it may if the program does the same things, but usually larger programs are much more complex and have many more features).
  - monocasa 8y ago
    > However much the effort of a similar technique can be reduced, it doesn't scale linearly with the size of the program [citation needed] Sure, you can write an arbitrary application where that's true, but AFAIK it doesn't have to be. IMO, sel4's really cool part isn't that it just was formally verified, but it's total design specifically for verifiability. The argument reminds me of all the people in the late 90s talking about how unit tests would never take off because they tried to introduce it in their legacy spaghetti codebase, and it wasn't amenable to testing.
    - pron 8y ago
      > [citation needed] Watch Xavier Leroy's talks. > IMO, sel4's really cool part isn't that it just was formally verified, but it's total design specifically for verifiability. Well, they were very selective with their algorithm choices, so that only very simple algorithms were used. Whether that's cool or an unaffordable restriction depends on your perspective. > The argument reminds me of all the people in the late 90s talking about how unit tests would never take off because they tried to introduce it in their legacy spaghetti codebase, and it wasn't amenable to testing. Except that I've been both practicing and evangelizing formal methods for some years now. I argue in favor of using them, not against, but as someone with some experience in that field I want to make sure people's expectations are reasonable. Unreasonable expectations all but killed formal methods once before.
sanxiyn 8y ago
> 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.

by pron 8y ago

monocasa 8y ago

It's an endgame wrt to memory safety (like I said). sel4 is memory safe. All the other mitigations like ASLR, canaries, etc are just hacks around the fact that proving memory safety of existing codebases is a Sisyphean task. And getting down to 5/1 proof to implemention is within the realm of what unit tests you should be writing anyway, so it's not that much of an economic investment.

pron 8y ago
I am not at all against formal verification. In fact, I evangelize it and use it myself quite a bit. But it is important to understand that it is very, very far from being a miracle cure. All software proofs prove correctness of specific theorems about a program given certain axioms. Those axioms must include, at the very least, the conformance of the hardware to some specification. But hardware can, at best, conform to the specification with some probability. For example, when you write `mov rax, [rdx]` it is not true that the computer will, 100% move the contents of the address pointed to by rdx into rax, only that it will do so with some high probability. Therefore, any proof about a software system (as opposed to an algorithm, which is an abstract mathematical entity) is a proof of a theorem of the form, "as long as the system behaves according to my assumptions, it will exhibit behaviors consistent with my conclusions." And that is even assuming that your conclusions cover all possible attacks. As it is generally impossible to formalize the concept of an arbitrary attack, you generally prove something far weaker. But none of this is even the biggest limitation of formal verification. The biggest would be its cost and lack of scalability. seL4 is about 1/5 the size of jQuery, and it is probably the largest piece of software ever verified end-to-end using deductive formal proofs as a verification technique. However much the effort of a similar technique can be reduced, it doesn't scale linearly with the size of the program (it may if the program does the same things, but usually larger programs are much more complex and have many more features).
- monocasa 8y ago
  > However much the effort of a similar technique can be reduced, it doesn't scale linearly with the size of the program [citation needed] Sure, you can write an arbitrary application where that's true, but AFAIK it doesn't have to be. IMO, sel4's really cool part isn't that it just was formally verified, but it's total design specifically for verifiability. The argument reminds me of all the people in the late 90s talking about how unit tests would never take off because they tried to introduce it in their legacy spaghetti codebase, and it wasn't amenable to testing.
  - pron 8y ago
    > [citation needed] Watch Xavier Leroy's talks. > IMO, sel4's really cool part isn't that it just was formally verified, but it's total design specifically for verifiability. Well, they were very selective with their algorithm choices, so that only very simple algorithms were used. Whether that's cool or an unaffordable restriction depends on your perspective. > The argument reminds me of all the people in the late 90s talking about how unit tests would never take off because they tried to introduce it in their legacy spaghetti codebase, and it wasn't amenable to testing. Except that I've been both practicing and evangelizing formal methods for some years now. I argue in favor of using them, not against, but as someone with some experience in that field I want to make sure people's expectations are reasonable. Unreasonable expectations all but killed formal methods once before.

sanxiyn 8y ago

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