Refactoring the FreeBSD Kernel with Checked C [pdf] | Hacker News Reader

Refactoring the FreeBSD Kernel with Checked C [pdf]

cs.rochester.edu

85 pointslelf13 comments

This seems to be an evolution of a bachelor’s thesis, which provides some snippets: 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/kerne... (2nd first author). I have not found any other code related to the paper.

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).

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?

It might be interesting to support these "new language constructs" in c2rust.

That is actually a really good idea!

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)

Rust would be a significantly more invasive change, of course ;)

Also see OpenBSD thoughts 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)

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.

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.

> 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?

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.

@MuffinFlavored: “I thought static analysis/fuzzing/unit tests were supposed to catch these kinds of things?”

How dare you criticise MICROS~1

Reply on news.ycombinator.com