3 ms·
Sadly I never put enough effort into trying out such checks. but your excitement about them gives me motivation to properly try them out.
by antonio2368 3y ago
Sadly I never put enough effort into trying out such checks.
but your excitement about them gives me motivation to properly try them out.
- nanolith 3y agoCBMC is subtle and will require some code changes to use effectively. The real key for using it, in my opinion, is to isolate individual classes and functions. Avoid instrumenting code with recursion and loops, and focus on defining and verifying function contracts, class invariants, and resource / memory lifetimes. It will require a significant amount of work to mock up standard library and third party library APIs, but the real beauty of CBMC is that once you define the interface contracts for these APIs and libraries, you can verify every use of them. I used CBMC previously to verify proper usage rules with C / JNI integration. JNI can be one complicated beast, and CBMC handily managed rule checks for its use. I'm an extremely careful developer who unit tests everything and strives for 99% coverage. CBMC was still able to detect a memory overwrite flaw in a networking library I wrote that was based on undefined behavior due to integer promotion and offset math. This passed the various sanitizers and unit tests I had in place, but CBMC was able to reduce it to an actual crash condition that was potentially exploitable. I don't think I can over-emphasize the usefulness of this tool.