Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Refactoring the FreeBSD Kernel with Checked C [pdf]

cs.rochester.edu

Post reply on HN
Print view View original

11–20 of 43 posts

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#11

Post by yjftsjthsd-h »

AdmiralAsshat wrote: post #7

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 tim…

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

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#14

Post by colonwqbang »

yjftsjthsd-h wrote: post #11
AdmiralAsshat wrote: post #7

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 tim…

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

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#16

Post by moonchild »

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

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#17

Post by tyingq »

moonchild wrote: post #16

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

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?

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#18

Post by wahern »

tyingq wrote: post #17
moonchild wrote: post #16

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

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/

Re: Refactoring the FreeBSD Kernel with Checked C [pdf]

#20

Post by irogers »

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.
Post reply on HN