Hacker News Reader

Comment by rwmj | Hacker News Reader

However you can do what Airbus do and formally prove your C code and use a formally proven toolchain like compcert to compile it. Or you can take a performance hit and add bounds checking to the C code[1]. Aircraft systems are probably the best chance that CHERI has, and that's pretty niche, small runs and very expensive, and still better solved in software.

[1] I literally wrote the paper on this back in 1996: https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html

View on HN

Most people on HN would run screaming away if they had to follow high integrity computing processes on their daily C programming.

If they think programming with Modula-2 and Object Pascal is programming with a straightjacket, good luck with MISRA, Frama-C, DOD and ISO certifications for reliable C code.

For the record, I found programming in MISRA C guidelines really fun; but then again, I did it out of personal interest. If I had to do it professionally, I guess the pressure would be less pleasant.

Right: unfortunately it really is a bit much to dismiss CHERI as a no-hope effort to boil the seas if the alternative plan is to rewrite everything in formally verified C (even if you'd also try to move some of it into GC languages instead).

The alternative is you use a compiler that adds bounds checking. It's possible to do this with C, with fine object granularity (even separate stack objects), and even preserve compatibility with existing non-bounds checked library code / system calls. When I did it back in 1996 there was a large overhead to doing that, but compilers can do much better these days. And anyway you have to compare the overhead to the cost of designing and building your own small run CPU and eshewing mainstream processors, which is also huge.

https://www.doc.ic.ac.uk/~phjk/BoundsChecking.html

Yet to this day no major OS vendor, selling C and C++ compilers, has ever bothered with.

Hardware memory tagging, via SPARC ADI, ARM MTE, CHERI has become a thing, before software based processes so far have failed adoption, and the OS vendors like Google, Microsoft, Apple, Oracle, rather go with hardware approach.

Major OS vendors have added loads of hardening to their C compilers. Not bounds checking specifically (because even if the overhead was only 20% that would be too high) but tons of other stuff such as: stack canaries, control flow integrity, hardened string functions, ASLR, zeroing uninitialized auto variables, forced warnings, linker hardening. These are added as standard in all decent Linux distros today. Probably Windows too, I've no idea. There's a good summary here: https://best.openssf.org/Compiler-Hardening-Guides/Compiler-...

There are also bounds checking options for major C compilers so if you want to use it, you can, eg. -fbounds-safety or the various sanitize options in Clang.

But no-one's claiming that the techniques which have been widely deployed already are bad or unworthy or haven't made a positive difference. (Certainly I'm not!) However it's evident that they haven't made a sufficient difference (and while they have an overall low cost compared to other approaches all that effort to patch and make do isn't free either).

Kind of, because to this day it has been a quixotic battle for devs to use them at scale.

Those OS vendors rather push for Swift, Java/Kotlin, C#, and Rust instead.

Alongside ARM MTE, Pluton, SPARC ADI.

Also, all those hardening measures and lack of bounds checking could have been solved with WG14 papers, nowhere to be found. C isn't set in stone.

Those techniques are implemented by default in Fedora & Debian. You have to opt out if for some reason you don't want to use them. So almost all C software compiled in these two major distros are using all of them. (Likely in other distros too, but I'm less familiar with how they configure their compilers).

Fedora will soon implement shadow stacks across the entire C codebase: https://discussion.fedoraproject.org/t/f45-change-proposal-e...

I thought MISRA was fine, and I don’t really understand why people complain about it. At least as a Fortran programmer who had to dabble in some C, I found I could read and write MISRA C much more easily than the obfuscated nonsense that C programmers get up to without rules, haha. (Actually come to think of it, it could just be that the MISRA codebase was engineered from the beginning).

Reply on news.ycombinator.com