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

Abstract

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.
Pages171-175
Number of pages5
ISBN (Electronic)9791188428045
ISBN (Print)9791188428045
DOIs
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
Volume2020
ISSN (Print)1738-9445

Conference

Conference22nd International Conference on Advanced Communications Technology, ICACT 2020
CountryKorea, Republic of
CityPyeongchang
Period20/2/1620/2/19

Keywords

  • CBMC
  • information security
  • model checking
  • software weakness

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

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

  • Cite this

    Byun, M., Lee, Y., & Choi, J. Y. (2020). Analysis of software weakness detection of CBMC based on CWE. In 22nd International Conference on Advanced Communications Technology: Digital Security Global Agenda for Safe Society, ICACT 2020 - Proceeding (pp. 171-175). [9061281] (International Conference on Advanced Communication Technology, ICACT; Vol. 2020). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.23919/ICACT48636.2020.9061281