Difference between revisions of "Secure coding tools"
From Simson Garfinkel
Jump to navigationJump to search
m |
m |
||
| Line 11: | Line 11: | ||
* https://www.dhs.gov/science-and-technology/csd-swamp | * https://www.dhs.gov/science-and-technology/csd-swamp | ||
* https://continuousassurance.org/ | * https://continuousassurance.org/ | ||
==Formal Verification Tools== | |||
CompCert is a formally verified optimizing C compiler. "On typical embedded processors, code generated by CompCert typically 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 available on request." | |||
CompCert is free for non-commercial use. | |||
* [http://compcert.inria.fr Project page] | |||
* [https://en.wikipedia.org/wiki/CompCert Wikipedia article on CompCert] | |||
* [https://github.com/AbsInt/CompCert Github Repository] | |||
* [https://www.absint.com/compcert/ Comparision with GCC] | |||
Revision as of 03:12, 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:
- 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 typically 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 available on request."
CompCert is free for non-commercial use.
