Live data from Hacker News

Refactoring the FreeBSD Kernel with Checked C [pdf]

cs.rochester.edu

41–43 of 43 posts

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

#42
post #20

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

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

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

#43
post #39
post #31

Earlier quoted context omitted.

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