Analysis of software weakness detection of CBMC based on CWE
2020 22nd International Conference on Advanced Communication Technology (ICACT)(2020)
摘要
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.
更多查看译文
关键词
CBMC,information security,model checking,software weakness
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络