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

Refactoring the FreeBSD Kernel with Checked C [pdf]

cs.rochester.edu

163 pointswglb41 comments

Checked c is interesting, but I think a more fruitful avenue would be verifast[0]. Verifast is completely compatible with existing c codebases (so you can keep using your existing c compiler), and is able to verify more interesting behaviour than checked c. [1] finds that it would have prevented 5 of 50 recent CVEs in FreeBSD, whose causes include unlocked memory accesses, resource leaks, and bad reference counts.

0. https://github.com/verifast/verifast

1. https://metasepi.org/en/posts/2020-10-14-avoid-freebsd-secur...

For a monolithic kernel? No chance it will be able to give the same security guarantees. Never mind the usual practical issues with symbolic execution like modeling the environment.

It mentions "symbolic execution" of code. Does that work fine with kernel code, being that the tool itself isn't in the right ring, etc?

Symbolic execution happens before deployment, and often can be incorporated into the compilation pipeline, much like a classic static analyzer. One of the most popular implementations (at least in the FOSS community) is KLEE: https://klee.github.io/

KLEE is only popular with the HN crowd, but not certainly not in the industry. There cbmc/satabs is leading. Esp. automotive. Also much older, and much easier to use. I recently even added formal verification to my CTL library variant, the STL for C.

https://github.com/rurban/ctl/commit/cc65e82ba1fdafcf9c83697...

cbmc found some huge bugs the testsuites were not able to find.

KLEE has similar status as Z3. Hugely popular, but rarely used in practice. Educational toys, or used in side-projects only.

I think the question being asked includes, "would existing symbolic execution tools be able to tell that e.g. a page-table was mangled"

Symbolic execution would tell you whether a page-table could be mangled, and if so which range of input of values would lead to that state. (Though you may need to annotate your code to define what a bad state looks like if it's not something as simple as a NULL pointer dereference.)

But the capacity for achieving that is a function of the engine and how it integrates with the language. Similar to formal verification it's strongly computationally bound in practice, so the best results (e.g. more comprehensive coverage) are achieved when you structure your code in a way that components (functions, groups of functions, etc) can be symbolically executed individually; and when you can drop annotations in the code to narrow down value ranges that the engine can't determine itself within a reasonable amount of time. So in principle a symbolic execution engine could determine whether a page-table could be mangled, but in practice it probably wouldn't be able to definitively tell you one way or another if you simply tossed the entire FreeBSD kernel source code at such an engine.

I'm not particularly knowledgable in this space. I'm abstaining from giving a proper description of what symbolic execution actually is because I'll probably just confuse things. But I have used KLEE and even found bugs using it. It's a steep learning curve so once you get to the point where you can make use of KLEE much of the theory will begin to make sense even if you can't describe it properly ;) And if you've ever used formal verification systems, especially ones with strong language integration, things will make sense much earlier.

I don't think there's a clean dividing line between symbolic execution and static analyzers. Some modern static analysis tests and optimizations in GCC and clang could be described as employing symbolic execution. A proper symbolic execution engine can just perform such tests more comprehensively, exploring much longer, deeper control flow paths with far greater state spaces.

Checked C appears to be a relatively recent research project from Microsoft[0][1], so I'm not sure that FreeBSD would be terribly keen on refactoring around it. There have also been many "safer C" languages before, so the only advantage that the paper offers is that Checked C seems to have a higher degree of backwards compatibility. I suppose that would allow the implementation/refactoring to gradually occur over time, rather than requiring a herculean initial effort.

[0] https://www.microsoft.com/en-us/research/project/checked-c/

[1]https://github.com/Microsoft/checkedc

> the only advantage that the paper offers is that Checked C seems to have a higher degree of backwards compatibility.

In fairness, that's a big deal, especially when trying to port a large existing code base.

Yes, compatibility is at least 80% of the deal with C. The "C" in C stands for compatible.

And me thinking that C follows B in the US English alphabet.

B stands for before C

I read that it was so named because C follows B in "BCPL"

> After creating the type system, the associated syntax, and the compiler for the new language, I felt that it deserved a new name; NB seemed insufficiently distinctive. I decided to follow the single-letter style and called it C, leaving open the question whether the name represented a progression through the alphabet or through the letters in BCPL.

http://cm.bell-labs.co/who/dmr/chist.html

> The "C" in C stands for compatible.

Source?

Wiki says:

> A successor to the programming language B, C was originally developed at Bell Labs by Dennis Ritchie between 1972 and 1973 to construct utilities running on Unix.

> In 1972, Ritchie started to improve B, which resulted in creating a new language C.

https://en.wikipedia.org/wiki/C_%28programming_language

It's a play on words

Regardless how much security minded people would like to replace C, the POSIX world isn't going away in generations to come, so this kind of solutions is welcomed.

The only alternative to it, besides improved static analyzers, is the ongoing work from CPU and OS vendors to bring hardware tagged memory into mainstream computing.

>Checked C has low performance overhead (only 8.6% on selected benchmarks [25])

Isn't that actually kind of significant?

That 8.6 figure comes from the paper linked below [0]. It’s an average. For many benchmarks, the difference is less than one percent, for others it’s 20 or more. In the freebsd article, they see around 1%.

[0] https://www.microsoft.com/en-us/research/uploads/prod/2018/0...

Depends on what you optimize. If sudo's password feedback code was 8.6% slower, it would be insignificant. If openssl's heartbeat code was 8.6% slower, it would be insignificant.

The numbers on a paper itself are much lower, so I would say it is a worthy idea. If not for "whole" kernel, then at least for the calls that they have replaced.

Yeah hugely so, 10% is a lot less than other safer languages people have switched to in order to get away from unsafe C.

Given there is before and after code, perhaps the translation can be automated. If the whole code base were auto-translated, what bugs could be detected and fed back to the C implementation? I'm assuming there is going to be hesitance from the FreeBSD community from migrating their codebase from C to Checked C, but that doesn't mean this work needs to come to nought. On top of bounded memory accesses, it'd be interesting to see better thread, signal, interrupt, etc. safety support. I guess at some point this just looks like Rust.

At Correct Computation (https://correctcomputation.com/, we are hiring), we are developing a tool called 3C to provide automation assistance for the conversion of C code into Checked C. A completely automated approach is impractical (i.e., without making lots of changes to the target program's code and adding lots of overhead), but we have found a "best effort" approach works well.

See here for more info (which transitively links to a tutorial of 3C's use): https://github.com/correctcomputation/checkedc-clang/blob/ma...

Slightly tangential, I am under the impression that the CHERI project has actually identified security bugs and reported them back to FreeBSD.

https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/

When was this paper published? Why do so many academic papers seem to omit or bury the publication date? I see the bibliography cites some papers with 2020 dates, so this paper must be from 2020 or 2021.

Why do so many academic papers seem to omit or bury the publication date? I see the bibliography cites some papers with 2020 dates, so this paper must be from 2020 or 2021.

That really irks me. It's apparently a holdover from the days when papers were published in magazine-type journals which had an issue date. Putting a date on the paper made it clear how far behind the publisher was. Papers should now have dates on them.

https://ieeexplore.ieee.org/document/9229980

Published in: 2020 IEEE Secure Development (SecDev)

Date of Conference: 28-30 Sept. 2020

Date Added to IEEE Xplore: 21 October 2020

The "no performance or code size overhead" result is remarkable.

It seems to me that the path of least resistance for memory safety in C-based OS kernels is to port them to a memory-safe C compiler and runtime.

I've looked at some source code written in Checked C. Doesn't it possibly take away some of the pleasure of writing C?

I don’t think pleasure is really the goal. The goal is systems that don’t fail spectacularly on unexpected inputs ...

My (overly charitable?) interpretation is, "Is Checked C so painful to write that we'd be better off just using a better managed language"

Of course, if it's feasible to refactor existing C code like in the paper, this seems like a good path forward, vs trying to "start over" with whatever other checked language of choice you pick.

The alternative is turn to hardware tagged memory.

https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/cheri...

https://docs.oracle.com/cd/E37838_01/html/E61059/gqajs.html

https://developer.apple.com/documentation/security/preparing...

https://www.youtube.com/watch?v=zkoOD4hmiGE

Given that we are swimming in transistors, holding on to hardware architectures that are rooted in a simplistic model keeps us from making obvious gains in software by having more capable hardware.

Well, the industry could have adopted designs like Burroughs, Xerox or Genera, instead they decided to make faster PDP-11s.

Clearly the pleasure of C is the feeling you get when your software fails spectacularly on unexpected inputs.

Yes. But it turns out that dragons may fly out of your nose when you're having fun this way.

Can I still use the original Bourne shell macros? If so, there's still hope…

If you mean cowboy programming, thankfully.

>pleasure of writing C?

Compared to C++?

It would be interesting if someone refactored ReactOS with Microsoft Checked C.

Reply on news.ycombinator.com