Analysis of software weakness detection of CBMC based on CWE

Minjae Byun, Yongjun Lee, Jin Young Choi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)


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.

Original languageEnglish
Title of host publication22nd International Conference on Advanced Communications Technology
Subtitle of host publicationDigital Security Global Agenda for Safe Society, ICACT 2020 - Proceeding
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages5
ISBN (Electronic)9791188428045
ISBN (Print)9791188428045
Publication statusPublished - 2020 Feb 1
Event22nd International Conference on Advanced Communications Technology, ICACT 2020 - Pyeongchang, Korea, Republic of
Duration: 2020 Feb 162020 Feb 19

Publication series

NameInternational Conference on Advanced Communication Technology, ICACT
ISSN (Print)1738-9445


Conference22nd International Conference on Advanced Communications Technology, ICACT 2020
Country/TerritoryKorea, Republic of

Bibliographical note

Publisher Copyright:
© 2020 Global IT Research Institute - GIRI.


  • CBMC
  • information security
  • model checking
  • software weakness

ASJC Scopus subject areas

  • Electrical and Electronic Engineering


Dive into the research topics of 'Analysis of software weakness detection of CBMC based on CWE'. Together they form a unique fingerprint.

Cite this