Secure coding tools

C/C++:

• Clang Thread Safety Analysis
• Rosecheckers – perform static analysis on C/C++ source
• Compiler-Enforced Buffer Overflow Elimination

Android:

• DidFail – uses static analysis to detect potential leaks – Android

See also:

• https://www.cert.org/secure-coding/products-services/scale.cfm?
• https://www.dhs.gov/science-and-technology/csd-swamp
• https://continuousassurance.org/

Formal Verification Tools

CompCert is a formally verified optimizing C compiler. "On typical embedded processors, code generated by CompCert typi­cally runs twice as fast as code generated by GCC without optimizations, and only 20% slower than GCC code at optimization level 3. Details about the benchmark mix used to obtain these numbers are avail­able on request."

CompCert is free for non-commercial use.

• Project page
• Wikipedia article on CompCert
• Github Repository
• Comparision with GCC

Optimization Based on Undefined Behavior

• What every compiler writer should know about programmers, or, “Optimization” based on undefined behaviour hurts performance, M. Anton Ertl and TU Wien, KPS 2015

• [https://pubweb.eng.utah.edu/~cs5785/slides-f10/Dangerous+Optimizations.pdf Dangerous

Optimizations and the Loss of Causality], CERT Technical Report CS 15-392, Robert C. Seacord