5 ms·

SeL4 is old news - not a criticism, but has anyone added another formally proven layer or component? (Edit: I mean new components beyond the microkernel, not im

by mmooss 2y ago

SeL4 is old news - not a criticism, but has anyone added another formally proven layer or component? (Edit: I mean new components beyond the microkernel, not improvements to the microkernel.) Also, I suspect some people - maybe some on HN :) - get emotional overload when they see the word 'proof' and their intellectual functions stop. It's not a panacea for the infinite problem of secure IT; it isn't a way to create or discover a perfect and flawless diamond of software. IIUC it means it's proven to meet specific requirements in specific conditions, and those requirements and conditions can be quite narrow; and it says nothing about other functions and conditions that are out of spec. Is that roughly correct? What does it mean in practical terms? What does a security professional see when they see 'formally proven software'? What are the specs that SeL4 meet (no, I haven't looked at the OP in a long time)? Isn't that the essential information here?

saithound 2y ago
Has anyone added another formally proven layer or component? Yes, they're being added all the time. Recently added features: - Support for a bunch of new architectures, including RISC-V. - Mixed criticality scheduling, which provides capability-based access to CPU time, mechanisms to limit the upper bound of execution of a thread, ensuring that high-criticality tasks have priority and access to necessary resources, and allowing "passive servers" which run on scheduling time donated by the caller. - Microkit, a new verified abstraction layer which made it much much easier to build actual systems using seL4. - Very recently, the Device Driver Framework, a device-driver template, control and data plane implementation, and tools for writing device drivers and providing device virtualisation for high-performance I/O on seL4. Formal verification can guarantee that specific requirements hold in specific conditions. It's true that in general such requirements and conditions can be quite narrow. But seL4 itself has a whole lot of proofs about it, covering a wide range of properties that one would want in a kernel, and these guarantees hold under very weak assumptions. Even the correctness of the C compiler is not assumed, they have a separate tool which looks at the compiler output and proves that the compiled binary behaves correctly with respect to the required C semantics. The requirements that seL4 meets include the following: the binary code of the seL4 kernel correctly implements the behaviour described in the abstract specification and nothing more. There are no buffer overflows, no memory leaks, no pointer errors or null pointer dereferences, no undefined behavior in the C code, no termination of the kernel apart from the explicit ways enumerated in the spec, etc. The specification and therefore the seL4 binary satisfy the security properties of integrity and confidentiality: the former means that there is absolutely no way for a process to change data that the process has no explicit permission to change, and the latter means that a process cannot, in any way, read data it has no explicit permission to read. It even shows that a process without permission cannot indirectly infer the data through certain side channels. Beyond security, the expected worst-case execution-time guarantees and scheduling properties are also met.
- deleted 2y ago
  [deleted]
- deleted 2y ago
  [deleted]
dloss 2y ago
For example: No buffer overflows, null pointer exceptions, use-after-free, etc. On ARM and RISCV64 not even the C compiler has to be trusted, because functional correctness has been proven for the binary. And there are more proofs besides functional correctness. https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que...
- deleted 2y ago
  [deleted]
im_down_w_otp 2y ago
https://github.com/auxoncorp/ferros https://github.com/auxoncorp/ferros Lots of type-level programming for tracking resources, hardware access, and capabilities at compile-time and trying to bring some of the underlying kernel guarantees up to the compiler because finding out about and debugging issues at runtime was just the absolute worst.
snvzz 2y ago
The document was updated in January. A lot has happened in the last few years, such as the founding of seL4 foundation, the maturation of mixed criticality scheduling, the celebration of multiple seL4 summits, and the deployment in practical use by multiple companies and countries, in several scenarios.
- axman6 2y ago
  Notably, Apple joined the seL4 foundation, as they use it in several of their products: https://sel4.systems/Foundation/Membership/ https://sel4.systems/Foundation/Membership/ (Not sure if they've stated publicly which, but it's been pretty well known for a while now).
ryao 2y ago
Being "formally proven" to be free of various flaws did not make seL4 immune to memory corruption flaws. Despite the formal proof, a memory corruption flaw was found a few years ago. The PRs for the commits fixing it and amending seL4's proof are public: https://github.com/seL4/seL4/pull/243 https://github.com/seL4/seL4/pull/243 https://github.com/seL4/l4v/pull/453 https://github.com/seL4/l4v/pull/453 You will find a number of other memory related bugs in its issue tracker: https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Abug%20 https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab... Interestingly, the PR fixing "register clobbering" in memory was not labelled bug, so it is not listed when you filter by "bug". I used to think seL4 was immune to these issues given its proof allegedly saying it is, but upon seeing this, I have come to think that the proof is not as comprehensive as the wider community has been lead to believe. That said, seL4 is still a very impressive piece of software. Finally, to answer your question. The specification that seL4 meets is published on github: https://github.com/seL4/l4v https://github.com/seL4/l4v
- isubasinghe 2y ago
  I believe only certain versions and on certain architectures is seL4 verified for. There are no bugs found at the C source code level for these builds of seL4.
  - vacuity 2y ago
    Even if it's not exactly seL4, there's good value in taking inspiration for design elements. It would still be a lot more robust than commodity operating systems.
    - deleted 2y ago
      [deleted]
  - ryao 2y ago
    This issue appears to have affected all architectures. This issue was present in the specification against which seL4 was verified. You can say that there are no bugs by virtue of it following the specification, but if the specification was wrong and in this case it was, then were there really no bugs?
nickpsecurity 2y ago
In high-assurance, formal methods were one of many used for the system. It was reduced complexity, precisely-specified behavior, likewise for security policy, proofs the design/code fulfilled it, exhaustive testing, leak analysis, pestering, and ability to recheck all this. That's so hard it was mostly done for only kernels commercially. From there, your real-world use will involve user-level components, protocols with interactions, and so on. Add one thing to the proven TCB and maybe your proof disappears. So, every trusted component has to be rigorously designed. Then, all the interactions for a holistic argument. Most don't do that. For example, seL4 hosting a web browser won't help you if it's a web application. IBOS and a WAF on seL4, all proven, might cover that. Harder argument. Most of these projects never go beyond the kernel or TLS stack or whatever. You can do stuff with that. Look up Nizza Secure Systems Architecture for a paper with many examples. Yet, they usually don't cut it. They're not compatible with popular apps either. So, most people just harden Linux or BSD or Windows.
- mmooss 2y ago
  > IBOS and a WAF on seL4, all proven If you mean web application firewall, that seems too complex to be proven? With infinite possible inputs, inspecting it would seem to require too much code to prove - unless it merely verifies traffic matches a short whitelist. Why talk about high assurance talked in the past tense? Is the field moribund? (I don't mean to point out a typo, if that's what it is.)
  - nickpsecurity 2y ago
    It could potentially be proven. We think it's unlikely due to cost or complexity. So, the fields default position was that most things would be low to medium assurance. Only select components would be high assurance. I hope that answers your broader question about adoption of seL4-like techniques for larger systems. Far as past tense, I left high-assurance security when I found out Jesus died for my sins and rose again. Had to learn an entirely new life with a focus on human beings instead of tech. I'm recently considering going back into security since I spend up to 12 hours a day at work anyway (two jobs). I should also note another reason I say past tense. Many people I learned from have died, retired, or switched focuses. The reason for the later is that there's no real market for high-assurance security. Most won't spend the money or make the tradeoffs. So, security-enhancing popular platforms while assuming they'll get hacked (and responding correctly) seemed like a better use of time. I mean, I could probably could all the high-security vendors on my hands...
trissylegs 2y ago
The developers of seL4 have been in funding hell for years. Most of their work was darpa research for remotely controlled drones. The US Military would very much like drones that can't be hacked. Their current work is on LionsOS which is more towards greater adoptions: https://lionsos.org/ https://lionsos.org/
- snvzz 2y ago
  >The developers of seL4 have been in funding hell for years. The actual story re: happenings in CSIRO is detailed in Gernot's blog[0], which is also quite interesting in its more technical posts. 0. https://microkerneldude.org/ https://microkerneldude.org/

by mmooss 2y ago

saithound 2y ago

Has anyone added another formally proven layer or component? Yes, they're being added all the time. Recently added features: - Support for a bunch of new architectures, including RISC-V. - Mixed criticality scheduling, which provides capability-based access to CPU time, mechanisms to limit the upper bound of execution of a thread, ensuring that high-criticality tasks have priority and access to necessary resources, and allowing "passive servers" which run on scheduling time donated by the caller. - Microkit, a new verified abstraction layer which made it much much easier to build actual systems using seL4. - Very recently, the Device Driver Framework, a device-driver template, control and data plane implementation, and tools for writing device drivers and providing device virtualisation for high-performance I/O on seL4. Formal verification can guarantee that specific requirements hold in specific conditions. It's true that in general such requirements and conditions can be quite narrow. But seL4 itself has a whole lot of proofs about it, covering a wide range of properties that one would want in a kernel, and these guarantees hold under very weak assumptions. Even the correctness of the C compiler is not assumed, they have a separate tool which looks at the compiler output and proves that the compiled binary behaves correctly with respect to the required C semantics. The requirements that seL4 meets include the following: the binary code of the seL4 kernel correctly implements the behaviour described in the abstract specification and nothing more. There are no buffer overflows, no memory leaks, no pointer errors or null pointer dereferences, no undefined behavior in the C code, no termination of the kernel apart from the explicit ways enumerated in the spec, etc. The specification and therefore the seL4 binary satisfy the security properties of integrity and confidentiality: the former means that there is absolutely no way for a process to change data that the process has no explicit permission to change, and the latter means that a process cannot, in any way, read data it has no explicit permission to read. It even shows that a process without permission cannot indirectly infer the data through certain side channels. Beyond security, the expected worst-case execution-time guarantees and scheduling properties are also met.

deleted 2y ago
[deleted]
deleted 2y ago
[deleted]

dloss 2y ago

For example: No buffer overflows, null pointer exceptions, use-after-free, etc. On ARM and RISCV64 not even the C compiler has to be trusted, because functional correctness has been proven for the binary. And there are more proofs besides functional correctness. https://docs.sel4.systems/projects/sel4/frequently-asked-questions.html https://docs.sel4.systems/projects/sel4/frequently-asked-que...

deleted 2y ago
[deleted]

im_down_w_otp 2y ago

https://github.com/auxoncorp/ferros https://github.com/auxoncorp/ferros Lots of type-level programming for tracking resources, hardware access, and capabilities at compile-time and trying to bring some of the underlying kernel guarantees up to the compiler because finding out about and debugging issues at runtime was just the absolute worst.

snvzz 2y ago

The document was updated in January. A lot has happened in the last few years, such as the founding of seL4 foundation, the maturation of mixed criticality scheduling, the celebration of multiple seL4 summits, and the deployment in practical use by multiple companies and countries, in several scenarios.

axman6 2y ago
Notably, Apple joined the seL4 foundation, as they use it in several of their products: https://sel4.systems/Foundation/Membership/ https://sel4.systems/Foundation/Membership/ (Not sure if they've stated publicly which, but it's been pretty well known for a while now).

ryao 2y ago

Being "formally proven" to be free of various flaws did not make seL4 immune to memory corruption flaws. Despite the formal proof, a memory corruption flaw was found a few years ago. The PRs for the commits fixing it and amending seL4's proof are public: https://github.com/seL4/seL4/pull/243 https://github.com/seL4/seL4/pull/243 https://github.com/seL4/l4v/pull/453 https://github.com/seL4/l4v/pull/453 You will find a number of other memory related bugs in its issue tracker: https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Abug%20 https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab... Interestingly, the PR fixing "register clobbering" in memory was not labelled bug, so it is not listed when you filter by "bug". I used to think seL4 was immune to these issues given its proof allegedly saying it is, but upon seeing this, I have come to think that the proof is not as comprehensive as the wider community has been lead to believe. That said, seL4 is still a very impressive piece of software. Finally, to answer your question. The specification that seL4 meets is published on github: https://github.com/seL4/l4v https://github.com/seL4/l4v

isubasinghe 2y ago
I believe only certain versions and on certain architectures is seL4 verified for. There are no bugs found at the C source code level for these builds of seL4.
- vacuity 2y ago
  Even if it's not exactly seL4, there's good value in taking inspiration for design elements. It would still be a lot more robust than commodity operating systems.
  - deleted 2y ago
    [deleted]
- ryao 2y ago
  This issue appears to have affected all architectures. This issue was present in the specification against which seL4 was verified. You can say that there are no bugs by virtue of it following the specification, but if the specification was wrong and in this case it was, then were there really no bugs?

nickpsecurity 2y ago

In high-assurance, formal methods were one of many used for the system. It was reduced complexity, precisely-specified behavior, likewise for security policy, proofs the design/code fulfilled it, exhaustive testing, leak analysis, pestering, and ability to recheck all this. That's so hard it was mostly done for only kernels commercially. From there, your real-world use will involve user-level components, protocols with interactions, and so on. Add one thing to the proven TCB and maybe your proof disappears. So, every trusted component has to be rigorously designed. Then, all the interactions for a holistic argument. Most don't do that. For example, seL4 hosting a web browser won't help you if it's a web application. IBOS and a WAF on seL4, all proven, might cover that. Harder argument. Most of these projects never go beyond the kernel or TLS stack or whatever. You can do stuff with that. Look up Nizza Secure Systems Architecture for a paper with many examples. Yet, they usually don't cut it. They're not compatible with popular apps either. So, most people just harden Linux or BSD or Windows.

mmooss 2y ago
> IBOS and a WAF on seL4, all proven If you mean web application firewall, that seems too complex to be proven? With infinite possible inputs, inspecting it would seem to require too much code to prove - unless it merely verifies traffic matches a short whitelist. Why talk about high assurance talked in the past tense? Is the field moribund? (I don't mean to point out a typo, if that's what it is.)
- nickpsecurity 2y ago
  It could potentially be proven. We think it's unlikely due to cost or complexity. So, the fields default position was that most things would be low to medium assurance. Only select components would be high assurance. I hope that answers your broader question about adoption of seL4-like techniques for larger systems. Far as past tense, I left high-assurance security when I found out Jesus died for my sins and rose again. Had to learn an entirely new life with a focus on human beings instead of tech. I'm recently considering going back into security since I spend up to 12 hours a day at work anyway (two jobs). I should also note another reason I say past tense. Many people I learned from have died, retired, or switched focuses. The reason for the later is that there's no real market for high-assurance security. Most won't spend the money or make the tradeoffs. So, security-enhancing popular platforms while assuming they'll get hacked (and responding correctly) seemed like a better use of time. I mean, I could probably could all the high-security vendors on my hands...

trissylegs 2y ago

The developers of seL4 have been in funding hell for years. Most of their work was darpa research for remotely controlled drones. The US Military would very much like drones that can't be hacked. Their current work is on LionsOS which is more towards greater adoptions: https://lionsos.org/ https://lionsos.org/

snvzz 2y ago
>The developers of seL4 have been in funding hell for years. The actual story re: happenings in CSIRO is detailed in Gernot's blog[0], which is also quite interesting in its more technical posts. 0. https://microkerneldude.org/ https://microkerneldude.org/