Analysis of software weakness detection of CBMC based on CWE

Model checking is a method of verifying whether a target system satisfies a specific property using mathematical and logical proofs. Model checking tools to verify design (1) require a formal description of the design and (2) there can be discrepancies between the model and actual implementation. To solve these problems, various tools such as CBMC and BLAST that can directly input C codes have been proposed. However, in terms of security, it is difficult to figure out which software weaknesses these tools can verify. In this paper, we matched the properties that CBMC can verify with corresponding CWEs, considering interdependencies of CWEs. We also conducted an experiment using Juliet Test Suite to check CBMC can actually verify the codes including these CWEs.