Removal of vulnerabilities in binary code by program model checking and concolic execution

Ferreirinha, Luís Pedro Félix

http://hdl.handle.net/10400.5/95544

Use this identifier to reference this record.

Name:	Description:	Size:	Format:
TM_Luís_Ferreirinha.pdf		843.5 KB	Adobe PDF	Download

Send Feedback

Authors

Ferreirinha, Luís Pedro Félix

Advisor(s)

Medeiros, Ibéria Vitória de Sousa

Abstract(s)

The C programming language, prevalent in Cyber-Physical systems, is crucial for system control where reliability is critical. However, it is also commonly susceptible to vulnerabilities, particularly buffer overflows, which are ranked among the most dangerous due to their potential for catastrophic consequences. Traditional vulnerability discovery techniques such as static and dynamic analysis, often struggle with scalability and precision when applied directly to the binary code of C. This dissertation introduces a novel approach designed to overcome these limitations by leveraging model checking and concolic execution techniques to verify security properties, defined in Linear Temporal Logic, of a program’s stack memory in binary code, and trampoline techniques to fix the identified security issues. The developed tool, BASICS: Binary Analysis and Stack Integrity Checker with Patching, constructs a memory state space from a program’s control flow graph and simulates function calls and loop constructs using concolic execution. Security properties defined in LTL model the behavior of buffer overflows, and BASICS identifies these vulnerabilities by analyzing counter-example traces generated when a security property is violated. The tool then addresses these vulnerabilities with a trampoline-based patching method. To ensure the effectiveness of the patches, BASICS tests the patched binaries with crash-inducing inputs extracted during concolic execution, confirming the successful removal of vulnerabilities. BASICS was evaluated using a dataset of small programs from NIST SARD and larger open-source applications. The evaluation demonstrated the tool’s effectiveness in detecting and patching buffer overflow vulnerabilities. This dissertation contributes to the field of computer security by introducing a new model checking approach for binary analysis, providing a framework for formal reasoning about stack memory, and delivering a customizable, open-source tool for detecting and patching vulnerabilities.