Hawkeye

Modern hospitals rely on large numbers of networked medical devices whose firmware is complex, heterogeneous, and often unsupported by vendors. When vulnerabilities are discovered, remediation is frequently slow, manual, and difficult to validate, particularly for end-of-life devices where source code and development toolchains are unavailable. In these settings, hospital operators must balance security risk against the possibility that a mitigation could disrupt critical device functionality.

HawkEye addresses this challenge by automating the synthesis of high-assurance vulnerability remediations for medical device firmware and by producing explicit assurance artifacts that explain the safety and impact of each mitigation. The system is designed to support rapid remediation while preserving correct device behavior and providing operators with the information needed to make informed deployment decisions.

The HawkEye project is funded by ARPA-H's UPGRADE program.

Technical Approach

HawkEye is built around two complementary analysis and reasoning systems:

• CodeHawk: Aarno Labs’ binary analysis and patching framework based on abstract interpretation
• Axe: Kestrel Institute’s symbolic-execution and input-modeling toolkit

Together, these tools enable end-to-end remediation workflows directly at the binary level, without requiring source code or vendor cooperation.

At a high level, HawkEye takes vulnerability information and device firmware as input and produces:

• Verified firmware patches that eliminate vulnerabilities in place,
• Deployable network input filters that block only the inputs capable of triggering a vulnerability, and
• Remediation Assurance Reports (RARs) that explain correctness, non-interference, and functional impact.

Automated Firmware Patch Synthesis

HawkEye automatically generates firmware patches that eliminate vulnerabilities directly at the binary instruction level, without requiring source code or vendor tooling. Using CodeHawk’s static analysis, the system identifies vulnerability-relevant program semantics, e.g., memory bounds, control flow, and data dependencies, and applies validated remediation templates at precise instruction locations.

All patches are designed to be minimal: they modify execution only for exploiting inputs while preserving correct device behavior, and do not require a recompilation. CodeHawk produces formal assurance evidence showing that the vulnerability is eliminated, the patch has been correctly applied, and that non-exploiting behavior is unchanged.

Input Filter Synthesis for Network-Level Protection

When deploying a firmware patching is impractical or undesirable, HawkEye synthesizes deployable network input filters that block only the inputs capable of triggering a vulnerability. These filters can be deployed on existing network appliances, enabling rapid protection without modifying the device.

Input filters are derived by comparing the semantics of patched and unpatched firmware. Axe extracts logical models of input processing and identifies the precise input conditions that distinguish exploiting executions. From this difference, HawkEye generates a minimal executable filter and accompanying proof that the filter both blocks all exploiting inputs and preserves normal operation.

Device Functionality Modeling and Contextual Analysis

To support safe deployment decisions, HawkEye is developing a medical device functionality ontology to model device behavior. Devices are automatically situated within the ontology using public documentation, firmware analysis, and machine-learning–assisted extraction.

Firmware components are then mapped to high-level device functionalities using static analysis and learned classifiers based on features such as API usage, control flow, and embedded strings. This mapping enables HawkEye to reason about which device functions could be affected by a remediation and to contextualize mitigations in terms meaningful to operators.

Remediation Assurance Reports

For each mitigation, HawkEye produces a Remediation Assurance Report (RAR) that summarizes correctness, scope, and functional impact. RARs explain whether a mitigation eliminates the vulnerability, whether it alters correct behavior, which device functionalities may be affected, and how the mitigation can be tested and deployed.

RARs combine formal verification & validation results, functionality interference analysis, and automatically generated test cases, providing clear, actionable assurance information to support deployment decisions.

Ongoing and Planned Work

HawkEye development focuses on expanding automation, coverage, and scalability across device types and vulnerability classes. Planned efforts include:

• Extending fully automated remediation to additional vulnerability classes,
• Enhancing ontology-driven functionality mapping using machine learning,
• Generating targeted test suites to support validation and regression testing, and
• Analyzing vendor firmware updates to assess whether vulnerabilities are correctly fixed and how updates affect device behavior.

Team

• Aarno Labs leads HawkEye system development, binary analysis, patch synthesis, and assurance reporting.
• Kestrel Institute develops formal input models, filter synthesis, and proof infrastructure through the Axe toolkit.