3 ms·
So when you implement a buffer overflow in your C program, you can be assured it will overflow in the manner specified.
by ttul 8y ago
So when you implement a buffer overflow in your C program, you can be assured it will overflow in the manner specified.
- thekingofh 8y agoAnd that specified manner is 'Undefined'. Exactly to spec!
- pslam 8y agoIt's just one part of the tooling, and doesn't solve program-correctness on its own. A formally verified toolchain is only really useful for projects which have pervasive mitigations against these kinds of errors. In other words, if you have a code base which has been verified to a high standard, you would also want a toolchain verified to a high standard. In an ideal world you'd have a formally verified toolchain for a language without as many deficiencies as C, but here we are.
- pjmlp 8y agoYep, where all C compilers would be Frama-C compliant, integrated into the CI/CD, and all OSes would be targeting CPUs with memory tagging like Solaris on SPARC ADI, but oh well.
- tom_mellior 8y agoThat's both funny and true, but note that the same CompCert semantics is also the basis of a verified static analysis tool that can be used to prove the absence of such errors in C programs: http://compcert.inria.fr/verasco/ http://compcert.inria.fr/verasco/ If you have a program that runs successfully through both the analyzer and the compiler, you can have quite a bit of confidence in the result.
- Retra 8y agoI know you're being facetious, but even if your compiler is verifying that your overflows are happening correctly, it is not a stretch to see that it can report that such overflows are occurring at all and what assumptions are causing them.