The Center for Education and Research in Information Assurance and Security (CERIAS)
The Center for Education and Research inInformation Assurance and Security (CERIAS)
Principal Investigator: Antonio Bianchi
Patching existing code bases quickly is of paramount importance to minimize the exposure of systems after vulnerabilities are discovered. Unfortunately, many issues hinder patch deployment, such as missing source code or unavailability of the original compilation tool-chain. Either full decompilation, patching, and recompilation, or micropatching of the original binary can address this issue. However, these approaches currently do not scale and, more importantly, do not offer any assurance that the patched binary preserves the intended functionality. In fact, formal reasoning about the functionality of a patched binary remains an intractable problem. For these reasons, embedded systems’ code is left
unpatched, exposing critical devices to severe security vulnerabilities.
To solve these issues, our crucial intuition is that: formally comparing the functionality of two binaries becomes a tractable problem when their differences are limited. Consequently, we propose a system to automatically inject patches in a binary, minimally modifying it, and assure the functionality of the patched binary. More precisely, we propose a novel approach based on the following key aspects: 1) a novel intermediate representation, 2) a formal verification method, and 3) a directed compilation technique.
Our proposed system, called DICER , will automatically inject, compile, and verify code patches in binary code, without assuming the existence of the original source code, nor the original compilation tool-chain.
This project is part of a DARPA-sponsored project named DARPA AMP, "Assured Micropatching." It is expected to last 4 years and it will be completed in collaboration with UC Santa Barbara and EPFL.
Other PIs: Dave (Jing) Tian Dongyan Xu