This post focuses on our capabilities to analyze and understand patches and updates supplied by a vendor or manufacturer. Vendor patches are typically distributed as binary updates with limited documentation of the included changes, i.e., the updates are opaque. There are many questions a user may have regarding a vendor patch:

• Does the patch fix a vulnerability, and if so, what is the evidence?
• Does the patch modify any existing functionality, and if so, how?
• Does the patch introduce any new functionality, and if so, what is this new functionality?
• Does the patch introduce any new bugs or vulnerabilities?

The lack of transparency in vendor-issued binary patches is a serious problem, particularly in high-assurance environments like hospitals and defense, where security and safety are paramount and updates must be evaluated thoughtfully.

For example, the FDA’s process for security updates in medical devices relies on vendors to self-assess whether a change, such as a vulnerability fix, significantly affects safety or effectiveness. If the vendor determines the update is minor, it can be deployed without FDA premarket review. The FDA does not independently verify this judgment or review the patch itself; instead, it relies on vendors to follow internal quality processes and maintain documentation, which is only examined during inspections. This creates an ad hoc process in which patch assessments are opaque and unverified by regulators unless specific concerns arise, leaving critical systems potentially vulnerable to ineffective security updates or updates that introduce new vulnerabilities or bugs.

CodeHawk’s static analysis can help users answer these questions via a structured, semantically-informed approach to understanding vendor-supplied firmware patches. This blog post demonstrates how CodeHawk can formally reason about vendor patches’ changes, benefits, and risks, using the vendor patch of CVE-2024-12248 as a case study. By comparing the vendor-patched binary to the original firmware, we 1) verify that the vulnerability has been remediated by employing CodeHawk’s C analyzer and 2) uncover and understand significant structural and functional changes introduced by the patch.

Background

CVE-2024-12248 affects a widely used patient monitor and was originally disclosed by our DIGIHEALS AMdP team, with CodeHawk’s automated memory safety analysis flagging the vulnerability. The vulnerability allows remote code execution by exploiting unchecked access to a global array indexed by untrusted network data. After reporting the issue, we later received a vendor-supplied patched firmware image for review. This presented an opportunity to use CodeHawk’s analysis tools not only to verify the vendor’s fix but also to systematically examine what else changed in the firmware.

This research is part of our AMdP project, funded by ARPA-H under the DIGIHEALS program. This is the third in a series of posts focusing on Aarno Labs’ CodeHawk Analysis and Patching Platform. In the first post, we described how CodeHawk’s automated memory safety analysis flagged the vulnerability and helped us to understand the cause and severity of the issue quickly. The second post demonstrated how CodeHawk’s high-assurance binary patching workflow enabled us to rapidly create a verified remediation without access to source code.

Binary Relational Analysis

CodeHawk’s Binary Relational Analysis compares a patched binary to its original counterpart and provides an overall syntactic and in-depth semantic comparison for specific parts of the binary. The syntactic comparison shows how much of the original binary changed due to the patch. In contrast to our binary micropatching strategy that minimizes changes to the binary, most vendor patches are generated by recompiling the target binary. This process creates disturbances across the whole binary due to changes in both global and relative addresses. For example, adding a new global variable to the binary may increase the size of one of the ELF sections, causing other sections to move. Similarly, adding code to a function will cause all functions after it to be at different locations. This means that a naive instruction-level comparison is not feasible.

Instead, CodeHawk uses information derived from each function’s Control-Flow Graph (CFG) to match original and patched functions and determine the parts of the patched binary with real functional changes. This process is semi-automated and low effort: CodeHawk automatically computes the required information and tries to match functions from both binaries. When patched functions are found that cannot be matched, the user intervenes to provide the information required to help CodeHawk synchronize again. In addition to supporting function modification, this process also supports the addition and deletion of functions from the binary, as we will see later in this post.

Once syntactic analysis is finished, the user can perform an in-depth semantic analysis of one or more of the functions that have been reported as changed. Using the semantic analysis, a user can see a side-by-side comparison of the lifting for the original and patched functions, in a process similar to a code review. They can also see a comparison between the output of CodeHawk’s C Analyzer for the original and the patched version. Under the hood, this uses the same machinery used to generate the assurances we provide as part of our binary patching framework, as described in our previous post.

Contec Patch Analysis Summary

We compared the Contec Medical Systems (Contec) firmware binary monitor with MD5 1ff255bbe1704f3ad4f995e0ea2a60a5 to a patched binary Contec submitted to the FDA for approval with MD5 969ecec0da23646221eae82ffca9ef17. Our findings:

• Using CodeHawk’s automated memory safety analysis, we can verify that Contec’s patched binary fixes the critical vulnerability we reported as part of our ARPA-H DIGIHEALS research.
• The provided vendor binary has structural modifications, including semantically changed and newly added functions, and moved and new global variables.
• Employing deeper analysis of the changeset, we found several functionality additions and modifications beyond the fix for the critical vulnerability. The modified functionality includes possibly addressing a number of CVEs affecting this device, including  CVE-2022-38100, CVE-2022-3027, and CVE 2022-38069.
• Importantly, we found a potential vulnerability which we are in the process of validating.

CVE-2024-12248 Patch Verification

Vulnerability in Original Binary

As we discussed in the first post in this series, the critical vulnerability discovered in the original Contec monitor binary was a global array access with unchecked tainted data, which could lead to buffer overflow or underflow. The output we get from CodeHawk’s C Analyzer for the relevant code in what we have termed the parsing function is the following:

    g_data_array[(data->token_1 - 1)].field_0 = 1;
----------------------------------------------------------------------------
         index-lower-bound(((*data).token_1 - 1):int) (safe)
          condition index-lowerbound(((data->token_1 - 1):int) delegated to the api
         index-upper-bound(((*data).token_1 - 1):int,bound:64) (safe)
          condition index-upperbound(((data->token_1 - 1):int,64) delegated to the api
----------------------------------------------------------------------------
    g_data_array[(data->token_1 - 1)].field_4 = data->token_2;
----------------------------------------------------------------------------
         index-lower-bound(((*data).token_1 - 1):int) (safe)
          condition index-lowerbound(((data->token_1 - 1):int) delegated to the api
         index-upper-bound(((*data).token_1 - 1):int,bound:64) (safe)
          condition index-upperbound(((data->token_1 - 1):int,64) delegated to the api
----------------------------------------------------------------------------
    strcpy(g_data_array[(data->token_1 - 1)].buffer, data->token_3);
----------------------------------------------------------------------------
         index-lower-bound(((*data).token_1 - 1):int) (safe)
          condition index-lowerbound(((data->token_1 - 1):int) delegated to the api
         index-upper-bound(((*data).token_1 - 1):int,bound:64) (safe)
          condition index-upperbound(((data->token_1 - 1):int,64) delegated to the api
----------------------------------------------------------------------------
   memcpy(&(g_data_array[(data->token_1 - 1)].field_2c), &(data->dest_addr), 16);
----------------------------------------------------------------------------
         index-lower-bound(((*data).token_1 - 1):int) (safe)
          condition index-lowerbound(((data->token_1 - 1):int) delegated to the api
         index-upper-bound(((*data).token_1 - 1):int,bound:64) (safe)
          condition index-upperbound(((data->token_1 - 1):int,64) delegated to the api
----------------------------------------------------------------------------

The vulnerable part in all of these four statements is the use of data->token_1 (decremented by 1) as the index in the global array g_data_array. The proof obligations in the output above state that the index value, data->token_1 - 1 must be non-negative (index-lower-bound condition) and must be less than 64, the size of the global array (index-upper-bound condition). No local information in the function is present that can prove that these requirements are met, because there are no bounds checks anywhere. However, with invariants, it is established that the value of data->token_1 is entirely determined external to this function, by the caller that passes the data argument to this function. Thus, the proof obligations are transferred to the calling function, which we call the listener function.

The listener function receives data from the network, parses the data into fields in a structure, and then passes the data structure to the function with the global array accesses. In the original binary, no checks are performed on the data received from the network; thus, the value of data->token_1 is entirely determined by the sender of the data. CodeHawk’s C analysis highlights the problem by showing potential violations at the call to the parsing function:

----------------------------------------------------------------
  parses_data_from_5001(&(parsed_data));
----------------------------------------------------------------
     index-upper-bound(((*&(parsed_data)).token_1 - 1):int,bound:64) (violation)
      return value from atoi may be tainted:
      choose value: 2147483647 to violate safety constraint:
     index-lower-bound(((*&(parsed_data)).token_1 - 1):int) (violation)
      return value from atoi may be tainted:
      choose value: -2147483648 to violate the zero lower bound

Patched Function

The result of CodeHawk’s syntactic relational analysis shows that of the two functions involved in the vulnerability, only the listener function was changed. When we perform CodeHawk’s relational semantic analysis on both functions, we see the same lifting and proof obligations for the parsing function, further confirming the syntactic relational analysis results.

For the listener function things are very different. Looking at the lifting comparison, we can see that the vendor chose to patch the vulnerability by adding comprehensive checks to the data received from the network in the listener function. For example:

  r0_18 = atoi(str);
  if ((r0_18 > 0)) {
    if ((r0_18 <= 64)) {
      parsed_data.token_1 = r0_18;
    } else {
      continue;
    }
  } else {
    continue;
  }

Furthermore, we can see that if an invalid packet is received, the vendor’s fix is to drop it by continuing the iteration of the listener’s function infinite loop. This was one of the strategies we discussed (and chose) during the development of our micro-patch.

When we look at the side-by-side comparison of the output from the C Analyzer we get full confirmation that the added checks are effective and the vulnerability no longer exists. In the output we can see that the proof obligations at the call site to the parsing function are now proven valid:

    parses_data_from_5001(&(parsed_data));
--------------------------------------------------------------------------------
<L>     index-lower-bound(((*&(parsed_data)).token_1 - 1):int) (safe)
           index: 0 satisfies constraint: (0 >= 0)
<L>     index-upper-bound(((*&(parsed_data)).token_1 - 1):int,bound:64) (safe)
           index: 63 and bound: 64 satisfy constraint: (63 < 64)
--------------------------------------------------------------------------------

Here, the <L> prefix indicates that the proof obligations guaranteeing that the accesses to the data array are safe have been proven with local invariants, which come from the added checks.

Additional Fixes

The semantic analysis of the listener function reveals that the vendor added several more checks to the parsed data, including checks for missing fields that would lead to segmentation faults. We believe these additional checks address CVE-2022-38100, but we cannot verify this because the CVE report does not provide enough information on the location of the vulnerability.

Caveat

Note that the above analysis demonstrates that the patch guarantees that a bounds violation in the parse function is fully blocked if the listener function is the only function that calls the parse function. There are no other direct calls to the parse function in our disassembly of the binary. Of course, we cannot guarantee that we found all the code or that there isn’t an indirect call to the parse function. However, our analysis and argument provide strong, formal evidence that the vulnerability has been correctly patched.

Structural Comparison

The vendor’s process for generating the patched binary introduced changes that affected the whole binary. Using CodeHawk’s Relational Binary Analysis capabilities, we created a structural mapping between the functions in the two binaries. As described above, this process identifies functions to target for deeper analysis, namely functions that changed in size or were newly introduced.

The syntactic relational analysis succeeded at constructing a complete mapping between the functions in the original binary, which has 3257 functions, and the patched binary, which has 3266 functions. For 28 functions, the number of basic blocks and/or instructions changed. Furthermore, the patched binary has 9 new functions compared to the original binary. The following two sections give a more detailed description of the modified and newly introduced functions.

Details on Modified Functions

Modifications to existing functions can roughly be categorized into four groups:

1. Two functions exhibit the largest changes, and both involve inserting new checks into the code. One of these functions is the listener function, which we have detailed above. The second function was modified with checks for the presence of substrings in a particular string, perhaps to block a directory traversal attack or mitigate CVE 2022-3027. At the low level, the changes to these functions represent, for the listener function, the addition of 34 new basic blocks with 140 instructions. For the second function, 4 new basic blocks are added, with 28 instructions added.
2. Four other functions have changes that collectively appear to be aimed at replacing the storage of plaintext passwords on file with hashed passwords. We hypothesize that this is a fix for CVE 2022-38069. At the low-level, these changes are not extensive, resulting in the addition of 1 basic block for two of the functions, and the addition of 6 to 14 instructions across each of four functions.
3. A set of four functions are modified to remove one or more calls to printf. At the low-level no basic block changes happen, and a range of 5 to 13 instructions are removed across each of the four functions.
4. Finally, a group of 18 functions are modified to insert a call to a newly introduced function. Our analysis shows that all of these modified functions are called within a newly created thread that writes data to a peripheral. The analysis shows the newly added function writes additional data to the peripheral.

Details on Added Functions

The patched binary includes nine new functions. Eight of these functions are concerned with password hashing, which we theorize mitigates CVE 2022-38069. As mentioned above, the ninth one is involved in additional writes to a peripheral on the device. Most of the password hashing functions contain a single basic block, and range in size from ~10 to ~70 instructions. However, one of them is complex, consisting of 16 basic blocks and more than 300 instructions. Our analysis suggests that it implements the core hashing functionality, although it does not seem to be an implementation of any standard hashing algorithm.

Other modifications

Besides the function modifications described above, the overall layout of the binary was also modified. Half of the ELF sections had modifications to their size, their starting address, or both. Importantly, the starting virtual address of the text section has shifted by 48 bytes, causing all functions to move. Since this code is not position-independent, absolute offsets have been changed for all functions. Furthermore, the .rodata section, .data section, and .bss sections have all changed their relative position to the text section, thereby changing all data offsets from the code to these sections.

Conclusion

Our analysis of Contec’s patch for CVE-2024-12248 illustrates the value of applying CodeHawk’s structured, semi-automated reasoning to vendor firmware updates. Using CodeHawk’s binary relational and semantic analysis tools, we verified (with caveats) that the patch effectively mitigates the critical buffer overflow vulnerability through added bounds checks. We also uncovered several other changes, including password hashing improvements and added peripheral functionality, highlighting how vendor security updates often go well beyond the stated single-issue remediation.

CodeHawk enables organizations and regulators to go beyond trust-based assumptions by providing concrete understanding of what has (and hasn’t) changed in a firmware update, and how those changes could affect users. If you are a device manufacturer, hospital system, or regulator and need an independent assessment of vendor patches, contact us at [email protected].