I really struggle with FORTIFY_SOURCE as a concept. It detects buffer overflows by propagating a little bit more static size information into the callee. It looks like something that catches a subset of the vulnerabilities that a static analyser could find and catches them dynamically, at run time, whereas a static analyser catches the same things at compile time before you’ve shipped the vulnerable code. I asked someone from Google’s Android Security team about this a while ago: why were they bothering to enable FORTIFY_SOURCE for Android, had they found any vulnerabilities with it that the clang static analyser couldn’t find? Apparently it hadn’t, it’s just that their dev workflow didn’t include running the static analyser.
To me, things like FORTIFY_SOURCE are just an admission that your security engineering practices are so weak that bugs that a static analyser would catch are showing up in production. It’s better to compile the protections in than have vulnerabilities but it’s nowhere near as good as having pre-merge static analyser checks that prevent you from introducing the vulnerabilities in the first place.
People have also used Frama-C to formally verify kernel functions like memcpy and memset: https://arxiv.org/abs/1809.00626
It’s understandable that Frama-C is not more well-known and used (it requires a lot of effort), but it would be a huge boost for the security of existing C codebases without having to succumb to the ‘rewrite it in Rust’ frenzy.