Detecting non-secure memory deallocation with CBMC
| dc.contributor.author | Singh, Mohit K., author | |
| dc.contributor.author | Prabhu, Vinayak, advisor | |
| dc.contributor.author | Ray, Indrajit, advisor | |
| dc.contributor.author | Ghosh, Sudipto, committee member | |
| dc.contributor.author | Ray, Indrakshi, committee member | |
| dc.contributor.author | Simske, Steve, committee member | |
| dc.date.accessioned | 2022-01-07T11:28:28Z | |
| dc.date.available | 2022-01-07T11:28:28Z | |
| dc.date.issued | 2021 | |
| dc.description.abstract | Scrubbing sensitive data before releasing memory is a widely recommended but often ignored programming practice for developing secure software. Consequently, sensitive data such as cryptographic keys, passwords, and personal data, can remain in memory indefinitely, thereby increasing the risk of exposure to hackers who can retrieve the data using memory dumps or exploit vulnerabilities such as Heartbleed and Etherleak. We propose an approach for detecting a specific memory safety bug called Improper Clearing of Heap Memory Before Release, referred to as Common Weakness Enumeration 244. The CWE-244 bug in a program allows the leakage of confidential information when a variable is not wiped before heap memory is freed. Our approach uses the CBMC model checker to detect this weakness and is based on instrumenting the program using (1) global variable declarations that track and monitor the state of the program variables relevant for CWE-244, and (2) assertions that help CBMC to detect unscrubbed memory. We develop a tool, SecMD-Checker, implementing our instrumentation based algorithm, and we provide experimental validation on the Juliet Test Suite that the tool is able to detect all the CWE-244 instances present in the test suite. The proposed approach has the potential to work with other model checkers and can be extended for detecting other weaknesses that require variable tracking and monitoring, such as CWE-226, CWE-319, and CWE-1239. | |
| dc.format.medium | born digital | |
| dc.format.medium | masters theses | |
| dc.identifier | Singh_colostate_0053N_16834.pdf | |
| dc.identifier.uri | https://hdl.handle.net/10217/234155 | |
| dc.language | English | |
| dc.language.iso | eng | |
| dc.publisher | Colorado State University. Libraries | |
| dc.relation.ispartof | 2020- | |
| dc.rights | Copyright and other restrictions may apply. User is responsible for compliance with all applicable laws. For information about copyright law, please see https://libguides.colostate.edu/copyright. | |
| dc.title | Detecting non-secure memory deallocation with CBMC | |
| dc.type | Text | |
| dcterms.rights.dpla | This Item is protected by copyright and/or related rights (https://rightsstatements.org/vocab/InC/1.0/). You are free to use this Item in any way that is permitted by the copyright and related rights legislation that applies to your use. For other uses you need to obtain permission from the rights-holder(s). | |
| thesis.degree.discipline | Computer Science | |
| thesis.degree.grantor | Colorado State University | |
| thesis.degree.level | Masters | |
| thesis.degree.name | Master of Science (M.S.) |
Files
Original bundle
1 - 1 of 1
Loading...
- Name:
- Singh_colostate_0053N_16834.pdf
- Size:
- 914.5 KB
- Format:
- Adobe Portable Document Format