7 ms·

If you really want, you could write your code in Agda or similar and prove it correct. See also seL4 https://github.com/seL4/seL4 https://github.com/seL4/seL4

by eru 2y ago

If you really want, you could write your code in Agda or similar and prove it correct. See also seL4 https://github.com/seL4/seL4 https://github.com/seL4/seL4 which is a proven correct kernel. https://sel4.systems/Verification/proofs.html https://sel4.systems/Verification/proofs.html

uecker 2y ago
... written in C.
- eru 2y ago
  It's written in C in the same way it's written in assembly: C is just used as part of the process to go from a high level spec to executable code. You can also compile eg Haskell via C. The subset of C used in seL4 is highly constrained.
- immibis 2y ago
  Proven correct C
- johnnyjeans 2y ago
  a subset of C is provable, and is the de-facto standard in the industry. what is it with rust people and thinking robust, automatic correctness checking was invented in the last 20 years?
  - Ygg2 2y ago
    Wow, the Linux kernel must be full of dunces that rather than writing in proven correct C, added another language that other maintainers hate. What morons! /sarcasm Disclaimer: above is sarcasm, while I don't think Linux Kernel Maintainers are perfect, I don't consider them dunces either. If they can't avoid writing UAF (use after free) or DF (Double free) bugs then what hope does the average C programmer has?
    - uecker 2y ago
      While the memory safety issues are a concern, switching to Rust + Unsafe will only reduce but not eliminate those issues and it is unclear whether adding a lot of complexity is actually worth it compared to other efforts to improve memory safety in C.
      - Ygg2 2y ago
        > switching to Rust + Unsafe will only reduce but not eliminate those issues Except in practice the code written in Rust experiences no safety issues[1]. I've seen this argument before a million times it is one part FUD (by making actual memory issues bigger than they are) one part Nirvana fallacy (argments that make so Java isn't memory safe because it will have to call into C). [1] https://storage.googleapis.com/gweb-research2023-media/pubtools/7665.pdf https://storage.googleapis.com/gweb-research2023-media/pubto... > is actually worth it compared to other efforts to improve memory safety in C As I aluded before, I am sure Linux Kernel Maintainers are aware of sel4. Which begs the question, why they didn't do it? It's in C, proves everything, and solves even more than Rust, why isn't it in kernel? I'm going to hazard a guess, the effort of going full proof for something like Linux would be through the roof. You would need lifetime of LKML dedication.
        uecker 2y ago
        Software written in Rust also experiences safety issues. If you believe otherwise, you are delusional. In the end, if you want extremely safe software there is no other way than formal verification. (and then there can still hardware be issues or bugs in the specification)
        Ygg2 2y ago
        > Software written in Rust also experiences safety issues. Yes. And? Seatbelts and air bags all experience safety issues, and general public was against them for a very long time. It doesn't mean they don't increase safety. Or that because you could fall into volcano you should abolish seatbelts. How about for start software with no memory errors? How about more XSS and less UAF? Also, not even formal proofs are enough. A smart enough attacker will use the gap between spec and implementation and target those errors. And while I agree we need more formal proofs and invariant oriented software design, those options are even less popular than Haskell.

by eru 2y ago

uecker 2y ago

... written in C.

eru 2y ago
It's written in C in the same way it's written in assembly: C is just used as part of the process to go from a high level spec to executable code. You can also compile eg Haskell via C. The subset of C used in seL4 is highly constrained.
immibis 2y ago
Proven correct C
johnnyjeans 2y ago
a subset of C is provable, and is the de-facto standard in the industry. what is it with rust people and thinking robust, automatic correctness checking was invented in the last 20 years?
- Ygg2 2y ago
  Wow, the Linux kernel must be full of dunces that rather than writing in proven correct C, added another language that other maintainers hate. What morons! /sarcasm Disclaimer: above is sarcasm, while I don't think Linux Kernel Maintainers are perfect, I don't consider them dunces either. If they can't avoid writing UAF (use after free) or DF (Double free) bugs then what hope does the average C programmer has?
  - uecker 2y ago
    While the memory safety issues are a concern, switching to Rust + Unsafe will only reduce but not eliminate those issues and it is unclear whether adding a lot of complexity is actually worth it compared to other efforts to improve memory safety in C.
    - Ygg2 2y ago
      > switching to Rust + Unsafe will only reduce but not eliminate those issues Except in practice the code written in Rust experiences no safety issues[1]. I've seen this argument before a million times it is one part FUD (by making actual memory issues bigger than they are) one part Nirvana fallacy (argments that make so Java isn't memory safe because it will have to call into C). [1] https://storage.googleapis.com/gweb-research2023-media/pubtools/7665.pdf https://storage.googleapis.com/gweb-research2023-media/pubto... > is actually worth it compared to other efforts to improve memory safety in C As I aluded before, I am sure Linux Kernel Maintainers are aware of sel4. Which begs the question, why they didn't do it? It's in C, proves everything, and solves even more than Rust, why isn't it in kernel? I'm going to hazard a guess, the effort of going full proof for something like Linux would be through the roof. You would need lifetime of LKML dedication.
      - uecker 2y ago
        Software written in Rust also experiences safety issues. If you believe otherwise, you are delusional. In the end, if you want extremely safe software there is no other way than formal verification. (and then there can still hardware be issues or bugs in the specification)
        Ygg2 2y ago
        > Software written in Rust also experiences safety issues. Yes. And? Seatbelts and air bags all experience safety issues, and general public was against them for a very long time. It doesn't mean they don't increase safety. Or that because you could fall into volcano you should abolish seatbelts. How about for start software with no memory errors? How about more XSS and less UAF? Also, not even formal proofs are enough. A smart enough attacker will use the gap between spec and implementation and target those errors. And while I agree we need more formal proofs and invariant oriented software design, those options are even less popular than Haskell.