Difference between revisions of "Secure coding tools"

From Simson Garfinkel
Jump to navigationJump to search
m
Line 29: Line 29:
* [http://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_29.pdf What every compiler writer should know about programmers, or, “Optimization” based on undefined behaviour hurts performance], M. Anton Ertl and TU Wien, KPS 2015
* [http://www.complang.tuwien.ac.at/kps2015/proceedings/KPS_2015_submission_29.pdf 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  
* [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
Optimizations and the Loss of Causality], CERT Technical Report CS 15-392, Robert C. Seacord

Revision as of 04:28, 27 June 2018

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:

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.

Optimization Based on Undefined Behavior