Authors:

Owen J Cochell

Date Created:

Not specified

Course Title:

Professor:

Not specified

About Paper:

Embedded systems suffer from a lack of memory safety features. Hence, they are vulnerable to any memory corruption vulnerabilities that are present in their firmware. Furthermore, their firmware is commonly written in memory-unsafe languages like C and C++, which increases the likelihood of memory corruption vulnerabilities and affects the safety of these systems. Consequently, it is important to find and fix any memory corruption vulnerability in the firmware before they are deployed to production embedded systems. Ansi-C Bounded Model Checking (CBMC) is a promising technique for verifying that firmware is free from memory corruption vulnerability, or exposing any such vulnerability in the firmware. To be effective, CBMC relies on harnesses that correctly model the firmware and execute with acceptable duration. However, no automation is available that can easily develop harnesses that enable sound, precise, and fast verification. This project aims to identify a set of guidelines that can aid in developing harnesses that enable sound, precise, and fast CBMC verification. We do this by developing harnesses for software components in the Contiki-ng network stack. We inject 24 known vulnerabilities into the Contiki-ng stack implementation and iterate on the harnesses until they can uncover the injected vulnerabilities. From our experiences writing CBMC harnesses, we have identified the steps required to generate harnesses that are sound, precise, and fast, and the challenges that make harness development challenging. We have also found and reported 2 zero-day vulnerabilities, and we are currently investigating 15 identified vulnerable behaviors. Finally, the lessons from our experience will guide the design of an automated tool that will make the development of correct CBMC harnesses easier. Keywords: C; CBMC; Networking; Security; Formal Analysis

Source:

Purdue University / 2024

Topics:

No topics listed

Co-authors:

Owen J Cochell