Detecting non-secure memory deallocation with CBMC

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.

Name thesis:degree_name

Master of Science (M.S.)

Level thesis:degree_level

Masters

Discipline thesis:degree_discipline

Computer Science

Grantor dc:publisher

Colorado State University. Libraries

Year dc:date.issued

2021

Authors dc:creator

• Singh, Mohit K., author
• Prabhu, Vinayak, advisor
• Ray, Indrajit, advisor
• Ghosh, Sudipto, committee member
• Ray, Indrakshi, committee member
• Simske, Steve, committee member

Statement 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.

Language dc:language.iso

eng, English

Identifier URI

https://doi.org/10.25675/3.02324

OAI identifier oai:identifier

oai:mountainscholar.org:10217/234155