Difference between revisions of "Secure coding tools"
From Simson Garfinkel
Jump to navigationJump to search
m |
|||
| (7 intermediate revisions by the same user not shown) | |||
| Line 24: | Line 24: | ||
==Optimization Based on Undefined Behavior== | ==Optimization Based on Undefined Behavior== | ||
* [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://people.csail.mit.edu/nickolai/papers/wang-undef-2012-08-21.pdf Undefined Behavior: What Happened to My Code?], Xi Wang Haogang Chen Alvin Cheung Zhihao Jia, APSys '12, July 23-24, 2012, Soul, S. Korea. | ||
* [https://people.csail.mit.edu/nickolai/papers/wang-stack.pdf Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior], Wang, Zeldovich, Kaashoek, SOSP’13, Nov. 3–6, 2013, Farmington, Pennsylvania, USA. | |||
* [https://nebelwelt.net/publications/files/15LangSec.pdf The Correctness-Security Gap in Compiler Optimization], D'Silva, Payer and Song, Language Security 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 Optimizations and the Loss of Causality], CERT Technical Report CS 15-392, Robert C. Seacord | |||
* [https://people.csail.mit.edu/nickolai/papers/wang-undef-2012-08-21.pdf Undefined Behavior: What Happened to my Code?], Xi Wang, Haogang Chen, Alvin Cheung, Zhihao Jia, Nickolai Zeldovich, M. Frans Kaashoek, APSys ’12, July 23–24, 2012, Seoul, S. Korea, Copyright 2012 ACM 978-1-4503-1669-9/12/07 | |||
Latest revision as of 11:00, 1 May 2020
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.
Optimization Based on Undefined Behavior
- Undefined Behavior: What Happened to My Code?, Xi Wang Haogang Chen Alvin Cheung Zhihao Jia, APSys '12, July 23-24, 2012, Soul, S. Korea.
- Towards Optimization-Safe Systems: Analyzing the Impact of Undefined Behavior, Wang, Zeldovich, Kaashoek, SOSP’13, Nov. 3–6, 2013, Farmington, Pennsylvania, USA.
- The Correctness-Security Gap in Compiler Optimization, D'Silva, Payer and Song, Language Security 2015.
- What every compiler writer should know about programmers, or, “Optimization” based on undefined behaviour hurts performance, M. Anton Ertl and TU Wien, KPS 2015
- Dangerous Optimizations and the Loss of Causality, CERT Technical Report CS 15-392, Robert C. Seacord
- Undefined Behavior: What Happened to my Code?, Xi Wang, Haogang Chen, Alvin Cheung, Zhihao Jia, Nickolai Zeldovich, M. Frans Kaashoek, APSys ’12, July 23–24, 2012, Seoul, S. Korea, Copyright 2012 ACM 978-1-4503-1669-9/12/07
