{"id":{"repo_id":"colostate","oai_identifier":"oai:mountainscholar.org:10217/234155"},"canonical_url":"https://search.dev.ndltd.org/etd/colostate/oai:mountainscholar.org:10217/234155","repository":{"repo_id":"colostate","name":"Colorado State University","base_url":"https://api.mountainscholar.org/server/oai/request"},"display":{"title":"Detecting non-secure memory deallocation with CBMC","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Singh, Mohit K., author","Prabhu, Vinayak, advisor","Ray, Indrajit, advisor","Ghosh, Sudipto, committee member","Ray, Indrakshi, committee member","Simske, Steve, committee member"],"institution":"Colorado State University. Libraries","degree_name":"Master of Science (M.S.)","degree_level":"Masters","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":[],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2021,"date_issued":"2021","date_published":"2021","updated_at":"2026-07-27T19:12:54Z","subjects":[],"languages":["eng","English"],"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."],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://doi.org/10.25675/3.02324"],"render_values":[{"text":"https://doi.org/10.25675/3.02324","href":"https://doi.org/10.25675/3.02324","code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/10217/234155","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:creator","label":"Author","values":["Singh, Mohit K., author","Prabhu, Vinayak, advisor","Ray, Indrajit, advisor","Ghosh, Sudipto, committee member","Ray, Indrakshi, committee member","Simske, Steve, committee member"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2022-01-07T11:28:28Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2022-01-07T11:28:28Z"]},{"key":"dc:date.issued","label":"Date","values":["2021"]},{"key":"dc:publisher","label":"Institution","values":["Colorado State University. Libraries"]},{"key":"dc:type","label":"Dc Type","values":["Text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Masters"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master of Science (M.S.)"]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["Colorado State University"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["English"]},{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["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."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["Singh_colostate_0053N_16834.pdf"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/10217/234155","https://doi.org/10.25675/3.02324"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["born digital","masters theses"]},{"key":"dc:title","label":"Title","values":["Detecting non-secure memory deallocation with CBMC"]}]}],"canonical_facts":{"dc:creator":["Singh, Mohit K., author","Prabhu, Vinayak, advisor","Ray, Indrajit, advisor","Ghosh, Sudipto, committee member","Ray, Indrakshi, committee member","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","masters theses"],"dc:identifier":["Singh_colostate_0053N_16834.pdf"],"dc:identifier.uri":["https://hdl.handle.net/10217/234155","https://doi.org/10.25675/3.02324"],"dc:language":["English"],"dc:language.iso":["eng"],"dc:publisher":["Colorado State University. Libraries"],"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"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Masters"],"thesis:degree_name":["Master of Science (M.S.)"],"thesis:institution_name":["Colorado State University"]},"updated_at":"2026-07-27T19:12:54Z"}