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 language | English |
|---|---|
| Title of host publication | 22nd International Conference on Advanced Communications Technology |
| Subtitle of host publication | Digital Security Global Agenda for Safe Society, ICACT 2020 - Proceeding |
| Publisher | Institute of Electrical and Electronics Engineers Inc. |
| Pages | 171-175 |
| Number of pages | 5 |
| ISBN (Electronic) | 9791188428045 |
| ISBN (Print) | 9791188428045 |
| DOIs | |
| Publication status | Published - 2020 Feb 1 |
| Event | 22nd International Conference on Advanced Communications Technology, ICACT 2020 - Pyeongchang, Korea, Republic of Duration: 2020 Feb 16 → 2020 Feb 19 |
Publication series
| Name | International Conference on Advanced Communication Technology, ICACT |
|---|---|
| Volume | 2020 |
| ISSN (Print) | 1738-9445 |
Conference
| Conference | 22nd International Conference on Advanced Communications Technology, ICACT 2020 |
|---|---|
| Country/Territory | Korea, Republic of |
| City | Pyeongchang |
| Period | 20/2/16 → 20/2/19 |
Bibliographical note
Publisher Copyright:© 2020 Global IT Research Institute - GIRI.
Keywords
- CBMC
- information security
- model checking
- software weakness
ASJC Scopus subject areas
- Electrical and Electronic Engineering