TY - GEN
T1 - Analysis of software weakness detection of CBMC based on CWE
AU - Byun, Minjae
AU - Lee, Yongjun
AU - Choi, Jin Young
PY - 2020/2/1
Y1 - 2020/2/1
N2 - 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.
AB - 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.
KW - CBMC
KW - information security
KW - model checking
KW - software weakness
UR - http://www.scopus.com/inward/record.url?scp=85083993516&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85083993516&partnerID=8YFLogxK
U2 - 10.23919/ICACT48636.2020.9061281
DO - 10.23919/ICACT48636.2020.9061281
M3 - Conference contribution
AN - SCOPUS:85083993516
SN - 9791188428045
T3 - International Conference on Advanced Communication Technology, ICACT
SP - 171
EP - 175
BT - 22nd International Conference on Advanced Communications Technology
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 22nd International Conference on Advanced Communications Technology, ICACT 2020
Y2 - 16 February 2020 through 19 February 2020
ER -