4 ms·

Quote regarding their previous work: "However, there is still the risk of security holes resulting from (...) the compiler and kernel developers interpreting th

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.
    - mondoshawan 5y ago
      The formal C semantics are defined in Isabelle/HOL, checked, and then the compiler output is also checked. They use standard GCC compilers for all of this. See https://riscv.org/blog/2021/05/sel4-on-risc-v-verified-to-binary-code/ https://riscv.org/blog/2021/05/sel4-on-risc-v-verified-to-bi...
    - vilhelm_s 5y ago
      Yes, making a mistake when writing down the C semantics is definitely possible. The point of the work announced here is to get rid of that risk, so that the proof only relies on the semantics of the RiscV instructions (and the C semantics become an intermediate thing which are proven rather than trusted). It's still possible that they made a mistake when writing down the RiscV semantics, but machine code is much simpler than C so the risk is smaller.

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.
  - mondoshawan 5y ago
    The formal C semantics are defined in Isabelle/HOL, checked, and then the compiler output is also checked. They use standard GCC compilers for all of this. See https://riscv.org/blog/2021/05/sel4-on-risc-v-verified-to-binary-code/ https://riscv.org/blog/2021/05/sel4-on-risc-v-verified-to-bi...
  - vilhelm_s 5y ago
    Yes, making a mistake when writing down the C semantics is definitely possible. The point of the work announced here is to get rid of that risk, so that the proof only relies on the semantics of the RiscV instructions (and the C semantics become an intermediate thing which are proven rather than trusted). It's still possible that they made a mistake when writing down the RiscV semantics, but machine code is much simpler than C so the risk is smaller.