6 ms·

Refactoring the FreeBSD Kernel with Checked C [pdf]

85 points by lelf 6y ago

MuffinFlavored 6y ago
Why not Rust? :D > Microsoft has developed an extension to the C language named Checked C which provides new source language constructs that allow the compiler to prevent NULL pointer dereferences and spatial memory safety errors through static analysis and run-time check insertion. I thought static analysis/fuzzing/unit tests were supposed to catch these kinds of things?
- zozbot234 6y ago
  It might be interesting to support these "new language constructs" in c2rust.
  - Ericson2314 6y ago
    That is actually a really good idea!
- toast0 6y ago
  Static analysis can't cover everything. Neither does fuzzing or unit tests. Static analysis plus run time checks where static analysis is inconclusive should mean if you overrun a buffer, you'll kernel panic rather than continue with an unsafe read/write. (If the whole kernel were refactored)
- saagarjha 6y ago
  Rust would be a significantly more invasive change, of course ;)
- simion314 6y ago
  Also see OpenBSD thoughts https://marc.info/?l=openbsd-misc&m=151233345723889&w=2 https://marc.info/?l=openbsd-misc&m=151233345723889&w=2 (I am just providing the link I am not competent enough on the topic to evaluate it;s merits)
  - loeg 6y ago
    Well, this is Theo specifically. It's a bit of a chicken and egg thing with BSDs. Base system code should compile with a base system compiler. But there is no reason to bring a Rust (or Checked C) compiler into base if nothing uses it.
    - simion314 6y ago
      From my reading is impossible to bring a Rust compiler yet (or at that time) because Rust can't compile itself on x86 and he also complained about the compilation times. From other similar threads that were suggesting to rewrite Linux in Rust I seen that Rust supports far less architectures then C so IMO the best solution for Rust community is too contribute to Rust kernels writen from scratch, it will start from zero users but this is how Linux started, then if the kernel and base tools are much better I can see it getting adopted in niche stuff at the start then in more and more things, IMO the RIR makes no sense for existing operating systems as Linux or BSDs, maybe for iOS, OSX where Apple controls the hardware and has the money and engineers to make the change and force the users to like it.
      - MuffinFlavored 6y ago
        > is too contribute to Rust kernels writen from scratch I'm pretty sure all of the I/O would be `unsafe` though, which begs the question... why write it in Rust in the first place?
        loeg 6y ago
        Because most of your code can be safe? Kernels have many internal objects and data structures and algorithms that could be managed in safe code, with unsafe only used around the edges. The idea with Rust unsafe is that the unsafe portions are not 100% of the whole, and can be located relatively easily.
- Stierlitz 6y ago
  @MuffinFlavored: “I thought static analysis/fuzzing/unit tests were supposed to catch these kinds of things?” How dare you criticise MICROS~1
moonchild 6y ago
Checked c is interesting, but the syntax is quite ugly. I wish it had done what cyclone did and used different symbols for different types of pointers (e.g. it used @ instead of * for fat pointers).
loeg 6y ago
This seems to be an evolution of a bachelor’s thesis, which provides some snippets: https://github.com/Duaiden/bachelor-thesis/tree/master/code https://github.com/Duaiden/bachelor-thesis/tree/master/code (first author). And this looks to be some test code and results, as well as possibly their kernel image: https://github.com/2000jedi/checkedc-tests/blob/master/kernel https://github.com/2000jedi/checkedc-tests/blob/master/kerne... (2nd first author). I have not found any other code related to the paper.

85 points by lelf 6y ago

Why not Rust? :D > Microsoft has developed an extension to the C language named Checked C which provides new source language constructs that allow the compiler to prevent NULL pointer dereferences and spatial memory safety errors through static analysis and run-time check insertion. I thought static analysis/fuzzing/unit tests were supposed to catch these kinds of things?

zozbot234 6y ago
It might be interesting to support these "new language constructs" in c2rust.
- Ericson2314 6y ago
  That is actually a really good idea!
toast0 6y ago
Static analysis can't cover everything. Neither does fuzzing or unit tests. Static analysis plus run time checks where static analysis is inconclusive should mean if you overrun a buffer, you'll kernel panic rather than continue with an unsafe read/write. (If the whole kernel were refactored)
saagarjha 6y ago
Rust would be a significantly more invasive change, of course ;)
simion314 6y ago
Also see OpenBSD thoughts https://marc.info/?l=openbsd-misc&m=151233345723889&w=2 https://marc.info/?l=openbsd-misc&m=151233345723889&w=2 (I am just providing the link I am not competent enough on the topic to evaluate it;s merits)
- loeg 6y ago
  Well, this is Theo specifically. It's a bit of a chicken and egg thing with BSDs. Base system code should compile with a base system compiler. But there is no reason to bring a Rust (or Checked C) compiler into base if nothing uses it.
  - simion314 6y ago
    From my reading is impossible to bring a Rust compiler yet (or at that time) because Rust can't compile itself on x86 and he also complained about the compilation times. From other similar threads that were suggesting to rewrite Linux in Rust I seen that Rust supports far less architectures then C so IMO the best solution for Rust community is too contribute to Rust kernels writen from scratch, it will start from zero users but this is how Linux started, then if the kernel and base tools are much better I can see it getting adopted in niche stuff at the start then in more and more things, IMO the RIR makes no sense for existing operating systems as Linux or BSDs, maybe for iOS, OSX where Apple controls the hardware and has the money and engineers to make the change and force the users to like it.
    - MuffinFlavored 6y ago
      > is too contribute to Rust kernels writen from scratch I'm pretty sure all of the I/O would be `unsafe` though, which begs the question... why write it in Rust in the first place?
      - loeg 6y ago
        Because most of your code can be safe? Kernels have many internal objects and data structures and algorithms that could be managed in safe code, with unsafe only used around the edges. The idea with Rust unsafe is that the unsafe portions are not 100% of the whole, and can be located relatively easily.
Stierlitz 6y ago
@MuffinFlavored: “I thought static analysis/fuzzing/unit tests were supposed to catch these kinds of things?” How dare you criticise MICROS~1

moonchild 6y ago

Checked c is interesting, but the syntax is quite ugly. I wish it had done what cyclone did and used different symbols for different types of pointers (e.g. it used @ instead of * for fat pointers).

loeg 6y ago

This seems to be an evolution of a bachelor’s thesis, which provides some snippets: https://github.com/Duaiden/bachelor-thesis/tree/master/code https://github.com/Duaiden/bachelor-thesis/tree/master/code (first author). And this looks to be some test code and results, as well as possibly their kernel image: https://github.com/2000jedi/checkedc-tests/blob/master/kernel https://github.com/2000jedi/checkedc-tests/blob/master/kerne... (2nd first author). I have not found any other code related to the paper.