7 ms·

SeL4 on RISC-V Verified to Binary Code

157 points by kryptiskt 5y ago

moonchild 5y ago
This approach is interesting, it's also used by compcert for its register allocator; the allocator itself is not formally verified, but the its results are. It's not complete, in a general sense, but I wonder if this sort of 'brute-force' approach to formal verification will become more popular over time, and lower the barrier to entry for formally verifying nontrivial programs.
- fuklief 5y ago
  In CompCert's case though, the register allocation verifier itself is verified. I'm not so sure the SMT solver used here are.
  - MaxBarraclough 5y ago
    > In CompCert's case though, the register allocation verifier itself is verified. I don't think so, I think moonchild's account of it is accurate. At least, it was accurate in 2012. From a 2012 blog post: [0] > In CompCert, this algorithm is not proven correct. Instead, after generating the graph, the compiler calls an OCaml implementation of IRC and then checks that the coloring is valid. If the checker confirms that the coloring is valid, the compiler uses it and proceeds along. If it does not confirm that it's valid, compilation is aborted. This checker is proven correct, and because it is simpler, its proof of correctness is easier. [0] http://gallium.inria.fr/blog/register-allocation/ http://gallium.inria.fr/blog/register-allocation/
    - fuklief 5y ago
      By "register allocation verifier", I meant the checker as mentioned in the post you quote.
    - archi42 5y ago
      > This checker is proven correct, and because it is simpler, its proof of correctness is easier. Still correct ;) What I belief GP (fuklief) meant was: The SMT solver might still be incorrect. Like the register allocator itself in CompCert. But for CompCert, the result is checked by a formally verified checker. I do not know if that's true or not for the result of the SMT solver.
      - creata 5y ago
        Don't SMT solvers output proof objects so that the results can be easily independently verified?
        syrak 5y ago
        Even if you had a verified SMT checker, you also need to prove that the encoding of the problem in SMT is correct, i.e., that a proof does translate to a valid register allocation solution, to achieve comparable guarantees to CompCert.
zibzab 5y ago
I might be wrong, but isn't their approach similar to what another team did some years back? https://www.researchgate.net/publication/262367164_Machine_code_verification_of_a_tiny_ARM_hypervisor https://www.researchgate.net/publication/262367164_Machine_c...
- saithound 5y ago
  I think they're doing different things. What they have in common is that they both use SMT solvers for automation. Glancing at the abstract, it seems like Dam, Guanciale and Nemati proved correctness theorems about a tiny hypervisor in ARMv7 assembly, using SMT solvers to automate some of the proof. The C compiler is not involved. Whereas seL4 is written in C, and the correctness theorems are proved using the C code and the specification. There is a compiler that turns the C code into RISC-V machine code. Then the new tool chain proves the equivalence of the C program and the RISC-V binary emitted by the compiler, using SMT solvers to automate some of that proof.
  - zibzab 5y ago
    The Dam paper mentions compiling C code to assembly first, but not much details is given. I think there is another step not covered in this paper that connects back to the C code. Maybe they saved that for another publication?
awelkie 5y ago
I've been wondering recently to what extent formal verification could be used to simplify CPU hardware and ISAs. For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. This paper[0] seems to imply that the savings would be non-negligible. Also interrupts and context switching could be avoided if programs are cooperatively scheduled and verified that they always yield after an appropriate amount of time. Those two examples are the only ones I could come up with, but I suspect that's because I don't know very much about hardware design. Are people working on this or am I just off-base here? [0]: https://arxiv.org/abs/2009.06789 https://arxiv.org/abs/2009.06789
- zozbot234 5y ago
  > For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. You'd need some sort of proof-carrying code to allow verification of these properties in binaries. Also, features like MMU's and interrupts are needed anyway to implement virtual memory, or user tasks with adjustable priorities.
  - fuklief 5y ago
    Would virtual memory still be necessary on a capability machine architecture [0] ? My understanding is that would not be the case since all programs can only access memory that's been allocated to it. By definition, capabilities cannot be created out of thin air like pointers can be ? [0]: https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/
    - warkdarrior 5y ago
      You probably still want to use virtual memory to simplify the programming model (flat address space) and to be able to overallocate memory across many processes. Without virtual memory you are pushing these functionalities to app developers.
- gmueckl 5y ago
ephaeton 5y ago
Quote regarding their previous work: "However, there is still the risk of security holes resulting from (...) the compiler and kernel developers interpreting the C semantics differently." Was that really a "risk" ? I think it's a given. "Beware of bugs in the above code; I have only proved it correct, not tried it." - Knuth also: https://cacm.acm.org/magazines/2018/7/229036-c-is-not-a-low-level-language/fulltext https://cacm.acm.org/magazines/2018/7/229036-c-is-not-a-low-... In light of that, I'm not convinced by the current increment either.
- saithound 5y ago
  That was really a risk. It's no longer a risk. In any situation where the developer's interpretation of the semantics differs from the binary semantics, their tool chain will reject the compiled binary. That's the point. The gcc git repository receives hundreds of contributions every week. Despite the heroic efforts of the open-source communities, it's still very easy to submit buggy or malicious patches (just think about the University of Minnesota scandal [1]). One of those could easily be used to target seL4, especially since it's hard to target seL4 in any other way, given all the other security guarantees. A tool that double-checks the compiler will buy the stakeholders significant peace of mind. [1] https://news.ycombinator.com/item?id=26887670 https://news.ycombinator.com/item?id=26887670
  - darksaints 5y ago
    I believe seL4 no longer uses gcc, but rather uses CompCert, which is also formally verified for adherence to standardized C semantics.
    - ephaeton 5y ago
      my reticule aims at the creation of the formal C semantics being used to verify the output. If both you and I make an off-by-one, we can always agree on the (say, index) value, but we'll both be always wrong. And C semantics is something especially finicky, given how often we delve in "undefined behaviour" territory, or our nowadays hardware does something that "back then" was unthinkable.
darksaints 5y ago
One of the discussions that always forms when talking about formally verified software is the whole verifying-the-verifier scenario. AKA, all of the reasons why you still can't trust it. And while that is an interesting conversation to have, it does a disservice to the practical benefits of the software verification process. The Linux CVE database was recently analyzed and it was determined that 96% of the vulnerabilities would be mitigated to at least non-critical status, if not completely eliminated, if linux were a microkernel architecture. Now throw in capabilities oriented security, and most of non-critical exploits become non-exploits. Throw in formal verification of the kernel, and you've basically eliminated everything except for hardware exploits. Assuming mass adoption, what seL4 effectively does is turn million dollar black market zero days into billion dollar zero days...possibly more. A million dollar exploit probably isn't even a line-item in the FBI budget. A billion dollar exploit would be a "needs-congressional-approval" type of line-item in the national US intelligence budget. Unless your job revolves around protecting the nuclear arsenal of a major nation-state, you won't ever have to worry about OS vulnerabilities, and you can rely on the security characteristics of the OS to drastically narrow down your attack surface. To me, that is a pretty big deal. It is slowly becoming a moral imperative that we start adopting this sort of security as a core standard.
- pjmlp 5y ago
  The irony is that in cloud environments with dozen of layers on top of Linux kernel, the whole mikrokernel vs monolith is a moot point. So much for monolith performance, when one needs to pile layers and layers of security on top.
- dmos62 5y ago
  I'm fuzzy on what it would take for there to be a mainstream formally-verified micro-kernel capability-based OS. Is it probable for Linux to be gradually refactored into that, or are will it take a fundamentally new OS?
  - CameronNemo 5y ago
    I think it would be possible to adapt some Linux drivers to run in a sandboxed capacity within a capability/microkernel system. IIRC there was once an L4 based project that integrated with Linux. https://en.wikipedia.org/wiki/L4Linux https://en.wikipedia.org/wiki/L4Linux
sel4groupie 5y ago
Man they been working on porting it to Qubes for a minute now

157 points by kryptiskt 5y ago

This approach is interesting, it's also used by compcert for its register allocator; the allocator itself is not formally verified, but the its results are. It's not complete, in a general sense, but I wonder if this sort of 'brute-force' approach to formal verification will become more popular over time, and lower the barrier to entry for formally verifying nontrivial programs.

fuklief 5y ago
In CompCert's case though, the register allocation verifier itself is verified. I'm not so sure the SMT solver used here are.
- MaxBarraclough 5y ago
  > In CompCert's case though, the register allocation verifier itself is verified. I don't think so, I think moonchild's account of it is accurate. At least, it was accurate in 2012. From a 2012 blog post: [0] > In CompCert, this algorithm is not proven correct. Instead, after generating the graph, the compiler calls an OCaml implementation of IRC and then checks that the coloring is valid. If the checker confirms that the coloring is valid, the compiler uses it and proceeds along. If it does not confirm that it's valid, compilation is aborted. This checker is proven correct, and because it is simpler, its proof of correctness is easier. [0] http://gallium.inria.fr/blog/register-allocation/ http://gallium.inria.fr/blog/register-allocation/
  - fuklief 5y ago
    By "register allocation verifier", I meant the checker as mentioned in the post you quote.
  - archi42 5y ago
    > This checker is proven correct, and because it is simpler, its proof of correctness is easier. Still correct ;) What I belief GP (fuklief) meant was: The SMT solver might still be incorrect. Like the register allocator itself in CompCert. But for CompCert, the result is checked by a formally verified checker. I do not know if that's true or not for the result of the SMT solver.
    - creata 5y ago
      Don't SMT solvers output proof objects so that the results can be easily independently verified?
      - syrak 5y ago
        Even if you had a verified SMT checker, you also need to prove that the encoding of the problem in SMT is correct, i.e., that a proof does translate to a valid register allocation solution, to achieve comparable guarantees to CompCert.

zibzab 5y ago

I might be wrong, but isn't their approach similar to what another team did some years back? https://www.researchgate.net/publication/262367164_Machine_code_verification_of_a_tiny_ARM_hypervisor https://www.researchgate.net/publication/262367164_Machine_c...

saithound 5y ago
I think they're doing different things. What they have in common is that they both use SMT solvers for automation. Glancing at the abstract, it seems like Dam, Guanciale and Nemati proved correctness theorems about a tiny hypervisor in ARMv7 assembly, using SMT solvers to automate some of the proof. The C compiler is not involved. Whereas seL4 is written in C, and the correctness theorems are proved using the C code and the specification. There is a compiler that turns the C code into RISC-V machine code. Then the new tool chain proves the equivalence of the C program and the RISC-V binary emitted by the compiler, using SMT solvers to automate some of that proof.
- zibzab 5y ago
  The Dam paper mentions compiling C code to assembly first, but not much details is given. I think there is another step not covered in this paper that connects back to the C code. Maybe they saved that for another publication?

awelkie 5y ago

I've been wondering recently to what extent formal verification could be used to simplify CPU hardware and ISAs. For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. This paper[0] seems to imply that the savings would be non-negligible. Also interrupts and context switching could be avoided if programs are cooperatively scheduled and verified that they always yield after an appropriate amount of time. Those two examples are the only ones I could come up with, but I suspect that's because I don't know very much about hardware design. Are people working on this or am I just off-base here? [0]: https://arxiv.org/abs/2009.06789 https://arxiv.org/abs/2009.06789

zozbot234 5y ago
> For example, MMUs are unnecessary if the OS verifies that all programs only access memory that's been allocated to it. You'd need some sort of proof-carrying code to allow verification of these properties in binaries. Also, features like MMU's and interrupts are needed anyway to implement virtual memory, or user tasks with adjustable priorities.
- fuklief 5y ago
  Would virtual memory still be necessary on a capability machine architecture [0] ? My understanding is that would not be the case since all programs can only access memory that's been allocated to it. By definition, capabilities cannot be created out of thin air like pointers can be ? [0]: https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/ https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/
  - warkdarrior 5y ago
    You probably still want to use virtual memory to simplify the programming model (flat address space) and to be able to overallocate memory across many processes. Without virtual memory you are pushing these functionalities to app developers.
gmueckl 5y ago

ephaeton 5y ago

Quote regarding their previous work: "However, there is still the risk of security holes resulting from (...) the compiler and kernel developers interpreting the C semantics differently." Was that really a "risk" ? I think it's a given. "Beware of bugs in the above code; I have only proved it correct, not tried it." - Knuth also: https://cacm.acm.org/magazines/2018/7/229036-c-is-not-a-low-level-language/fulltext https://cacm.acm.org/magazines/2018/7/229036-c-is-not-a-low-... In light of that, I'm not convinced by the current increment either.

saithound 5y ago
That was really a risk. It's no longer a risk. In any situation where the developer's interpretation of the semantics differs from the binary semantics, their tool chain will reject the compiled binary. That's the point. The gcc git repository receives hundreds of contributions every week. Despite the heroic efforts of the open-source communities, it's still very easy to submit buggy or malicious patches (just think about the University of Minnesota scandal [1]). One of those could easily be used to target seL4, especially since it's hard to target seL4 in any other way, given all the other security guarantees. A tool that double-checks the compiler will buy the stakeholders significant peace of mind. [1] https://news.ycombinator.com/item?id=26887670 https://news.ycombinator.com/item?id=26887670
- darksaints 5y ago
  I believe seL4 no longer uses gcc, but rather uses CompCert, which is also formally verified for adherence to standardized C semantics.
  - ephaeton 5y ago
    my reticule aims at the creation of the formal C semantics being used to verify the output. If both you and I make an off-by-one, we can always agree on the (say, index) value, but we'll both be always wrong. And C semantics is something especially finicky, given how often we delve in "undefined behaviour" territory, or our nowadays hardware does something that "back then" was unthinkable.

darksaints 5y ago

One of the discussions that always forms when talking about formally verified software is the whole verifying-the-verifier scenario. AKA, all of the reasons why you still can't trust it. And while that is an interesting conversation to have, it does a disservice to the practical benefits of the software verification process. The Linux CVE database was recently analyzed and it was determined that 96% of the vulnerabilities would be mitigated to at least non-critical status, if not completely eliminated, if linux were a microkernel architecture. Now throw in capabilities oriented security, and most of non-critical exploits become non-exploits. Throw in formal verification of the kernel, and you've basically eliminated everything except for hardware exploits. Assuming mass adoption, what seL4 effectively does is turn million dollar black market zero days into billion dollar zero days...possibly more. A million dollar exploit probably isn't even a line-item in the FBI budget. A billion dollar exploit would be a "needs-congressional-approval" type of line-item in the national US intelligence budget. Unless your job revolves around protecting the nuclear arsenal of a major nation-state, you won't ever have to worry about OS vulnerabilities, and you can rely on the security characteristics of the OS to drastically narrow down your attack surface. To me, that is a pretty big deal. It is slowly becoming a moral imperative that we start adopting this sort of security as a core standard.

pjmlp 5y ago
The irony is that in cloud environments with dozen of layers on top of Linux kernel, the whole mikrokernel vs monolith is a moot point. So much for monolith performance, when one needs to pile layers and layers of security on top.
dmos62 5y ago
I'm fuzzy on what it would take for there to be a mainstream formally-verified micro-kernel capability-based OS. Is it probable for Linux to be gradually refactored into that, or are will it take a fundamentally new OS?
- CameronNemo 5y ago
  I think it would be possible to adapt some Linux drivers to run in a sandboxed capacity within a capability/microkernel system. IIRC there was once an L4 based project that integrated with Linux. https://en.wikipedia.org/wiki/L4Linux https://en.wikipedia.org/wiki/L4Linux

sel4groupie 5y ago

Man they been working on porting it to Qubes for a minute now