Earlier quoted context omitted.
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.
Refactoring the FreeBSD Kernel with Checked C [pdf]
31–40 of 43 posts
Re: Refactoring the FreeBSD Kernel with Checked C [pdf]
#32>Checked C has low performance overhead (only 8.6% on selected benchmarks [25]) Isn't that actually kind of significant?
Yeah hugely so, 10% is a lot less than other safer languages people have switched to in order to get away from unsafe C.
Re: Refactoring the FreeBSD Kernel with Checked C [pdf]
#33>Checked C has low performance overhead (only 8.6% on selected benchmarks [25]) Isn't that actually kind of significant?
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.
Re: Refactoring the FreeBSD Kernel with Checked C [pdf]
#34I've looked at some source code written in Checked C. Doesn't it possibly take away some of the pleasure of writing C?
>pleasure of writing C?
Compared to C++?
Re: Refactoring the FreeBSD Kernel with Checked C [pdf]
#35Earlier quoted context omitted.
> 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.
> 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.
Re: Refactoring the FreeBSD Kernel with Checked C [pdf]
#36Re: Refactoring the FreeBSD Kernel with Checked C [pdf]
#37Earlier quoted context omitted.
Yes, compatibility is at least 80% of the deal with C. The "C" in C stands for compatible.
> 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
Re: Refactoring the FreeBSD Kernel with Checked C [pdf]
#38Earlier quoted context omitted.
And me thinking that C follows B in the US English alphabet.
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.
Re: Refactoring the FreeBSD Kernel with Checked C [pdf]
#39Earlier quoted context omitted.
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.
Re: Refactoring the FreeBSD Kernel with Checked C [pdf]
#40Checked 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.…
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.