We gave a frontier language model a stripped ARM binary and the annotated disassembly of one function, and asked it to patch a real stack buffer overflow. It produced a compact in-place patch along with a detailed rationale for why that patch is correct. This post covers what we did next: using CodeHawk to independently verify that the overflow is closed and that nothing else in the binary changed.

Our position at Aarno Labs is that AI proposes and formal methods verify. Generative models produce candidates: a plausible patch, a type mapping, a rewrite rule. Sound analysis is what turns a candidate into a conclusion. This post applies that to a single vulnerability, and then looks at what a wider analysis of the surrounding code turned up.

The experiment

We took a binary from the corpus we work on under our Hawkeye project (ARPA-H, UPGRADE program): the httpd web server from a Tenda AC18 router (US_AC18V1.0BR_V15.03.05.05_multi_TD01) — ARM32, EABI5, dynamically linked against uClibc, and stripped. It contains CVE-2018-18732, a stack-based buffer overflow.

We gave Claude Sonnet 5 two inputs:

• the original binary, and
• CodeHawk's annotated disassembly of the single vulnerable function, fromSetSysTime.

No source code, no headers, and no description of the bug beyond what CodeHawk's listing already carried. CodeHawk had done the discovery and localization, flagging address 0x8ba00 as a stack buffer overflow. We asked the model for an in-place patch to the offending strcpy call and nothing more. The session cost $4.74 and 16 minutes of API time.

The division of labor: CodeHawk found and localized the bug, the model produced a fix, and CodeHawk then verified that fix independently.

The vulnerability

fromSetSysTime handles the device's time-synchronization endpoint. When the request's timeType is "sync", the function reads several CGI parameters — including ntpServer (default "time.windows.com") — and copies the attacker-supplied ntpServer string into a fixed-size stack buffer with an unbounded strcpy:

0x8b9ec  LDR  R3, [R11,-0x20]     ; R3 = ntpServer value (attacker-controlled) 
0x8b9f0  SUB  R2, R11, #0x248 
0x8b9f4  ADD  R2, R2, #0xc        ; R2 = &dest buffer 
0x8b9f8  MOV  R0, R2              ; R0 = dest 
0x8b9fc  MOV  R1, R3              ; R1 = src (ntpServer) 
0x8ba00  BL   0xf72c              ; call strcpy(dest, src)   <-- no length check

CodeHawk reconstructed the stack layout and put the destination's capacity at 260 bytes. There is no length check anywhere on the path, so an ntpServer value of 260 bytes or longer runs off the end of the buffer, through the adjacent locals, and into the saved R11/LR slots that the function epilogue pops directly into R11/PC, overwriting the saved return address and giving an attacker control of execution. CodeHawk's block-write proof obligation for the copy at 0x8ba00 was reported open: the analyzer could not bound the write, because the source length is unconstrained. That open obligation is how the vulnerability appears in the analysis output.

What the model produced

An in-place patch is a tight constraint: same code size, no relocation of any other instruction, no new code cave or trampoline, and ideally no new imports, because moving anything means fixing up everything that points at it.

The patch satisfies all of these. It retargets the copy from strcpy to strncpy and supplies a length bound, and it makes room for the new third argument without adding an instruction. The basis is a small redundancy in the original register setup:

• ADD R2, R2, #0xc computed the destination address into R2, which the next instruction (MOV R0, R2) then copied into R0. The model collapsed the two: change the first to ADD R0, R2, #0xc, landing the destination directly in R0, where the call needs it.
• That frees the now-redundant MOV R0, R2 slot, which becomes MOV R2, #0x100 — the length argument, 256.
• The final BL is retargeted from strcpy (0xf72c) to strncpy (0xf1ec), which the binary already imports through a PLT jump-slot in the same style, so no new import is needed.

Three instruction words change, twelve bytes, and the call becomes strncpy(dest, src, 0x100). Two of the five words in the sequence are left byte-for-byte identical.

The model bounded the copy at 256 rather than the full 260-byte capacity, for a specific reason. strncpy does not guarantee NUL-termination: if the source is at least n bytes, it writes exactly n bytes and no terminator. The buffer was zero-filled by an earlier memset, so bounding the copy at 256 leaves bytes 256–259 untouched, and therefore still zero, which means the result is always NUL-terminated regardless of input and safe for anything downstream that reads it as a string. (259 would give the same guarantee with a tighter margin, but 0x103 is not encodable as a single ARM immediate; 0x100 is, which keeps the patch at three words.)

The model also wrote the patch tool: a Python script that verifies each target site matches the expected original bytes before writing, backs up the original, and applies the twelve-byte change, refusing to touch a binary that does not match.

This is careful work, and it arrives with a clear explanation of why the model considers it correct.

Plausible is not proven

We have written before about a frontier model that analyzed a disclosed CVE and produced a technically detailed, plausible, and wrong conclusion about exploitability: a conclusion our DIODE engine settled with a concrete proof-of-vulnerability input. We have also written about verifying an opaque vendor patch, where "the vendor says it is fixed" is not on its own an assurance argument for a device in a hospital. In each case, a detailed and confident rationale was not what established whether the output was safe to deploy.

The same applies to an AI-authored binary patch, which edits machine code in a stripped firmware image its operators cannot rebuild. That the model was confident, and that its reasoning reads as correct, is not an assurance argument for a fleet of deployed devices. Two questions have to be answered independently of whatever produced the patch:

1. Does the patch close the vulnerability?
2. Does it change anything else?

Neither is answered by the model's own explanation. Both are answered by CodeHawk's binary relational analysis, which analyzes the patched binary and compares its invariants against the original's.

Verifying the patch with CodeHawk

The relational analysis includes a run of CodeHawk's memory-safety analysis on the patched binary. No knowledge of the model's rationale was carried over; the analyzer reads the new bytes and reasons about them.

The vulnerability is closed. At the copy site 0x8ba00, the block-write proof obligation that was previously open is now discharged:

Original binary:
  0x8ba00: block-write(char, (SP_in - 0x240), (xf_ntpos rtn_sub_2b884))   (open) 
  
Patched binary:
  0x8ba00: block-write(char, (SP_in - 0x240), 0x100)
           (safe, buffer size 256 fits in available space of 260 bytes)

The result is expressed in the same formal terms that expressed the problem. CodeHawk proves the write is bounded to 256 bytes into a 260-byte region, for any input rather than only for inputs a test happened to cover.

A note on scope. Four other proof obligations at this call site — concerning the source string (null-terminated, not-null, initialized-range, and a source-side buffer obligation) — remain open in both the original and the patched analysis. This follows from how narrow we made the experiment: the analysis was run bare, with no header files and no supplied user data. CodeHawk therefore has no information about the helper that produces the ntpServer pointer, including its return value's properties and its signature. With that information absent, the analyzer can confirm what the bytes themselves establish, which is that there is no write overflow, and everything else stays as it was. We state this explicitly because which obligations are discharged and which are not is itself the assurance argument, and deserves careful review. Every piece of software should ship with one.

Nothing else changed. Closing the hole is half of a deployable patch; the other half is a guarantee that the fix did not alter how the device behaves. CodeHawk's relational analysis compares the invariants of the original and patched binaries across the whole function:

CodeHawk Relational Analysis:  invariant comparison
  Invariants lost:            0
  Invariants lost/modified:   8 
  Invariants not modified:    8854  (in 332 locations)

No invariants were lost. The eight modified invariants are all at the patch site, and they are the changes the patch intends: the destination address now flows through R0 instead of R2, R2 now holds the constant 0x100, and the return-value register reflects a call to strncpy instead of strcpy. The remaining 8,854 invariants, across 332 locations, are untouched. The comparison establishes that the register shuffling introduced by the patch produces no semantic change downstream of the call.

This was provable here for a specific reason. The registers the model repurposed are dead by the time the call returns, because the call itself clobbers them, so nothing the rearrangement did to them can persist past it. That is a property of this patch rather than a general guarantee: when a rearrangement touches registers that are still live after the call, establishing the same result is harder and depends on how those registers are used downstream. Our Hawkeye patching methodology keeps changes in this regime — one call site, minimal scope — so that the assurance argument stays tractable.

Together these give two results the model's own explanation could not: the vulnerability is closed, and the rest of the function's behavior is unchanged.

A second question: is the buffer ever read?

That settles the patch. A separate line of inquiry is the code around it: not whether the fix is sound, but what the function it sits in is actually doing. That is reverse engineering rather than patch assurance, and what it turned up says more about the state of the binary than about the patch. So we re-ran the analysis with more context — a hand-written header supplying the signatures and data structures the bare analysis had lacked, plus the rest of the device's firmware rather than one function in isolation — and asked whether the overflowed buffer is ever read.

CodeHawk's stack-layout reconstruction shows the buffer is a field inside a 296-byte struct that the function hands to a routine named send_msg_to_netctrl. That routine is an imported symbol: its implementation is not in the httpd binary, so the question cannot be answered from the binary we had been analyzing. We found it in the firmware's shared library, libcommon.so, where it appears byte-identical to the same routine in a different Tenda model — common internal code, reused unchanged across product lines.

The implementation treats its argument as a C string: it takes the argument's strlen, rejects it if too long, and formats it with %s into a short message string. The struct's first field is a four-character ASCII opcode, "op=3", written by an unrelated sprintf and NUL-terminated at offset 4. strlen and %s stop there. The ntpServer field, the destination of the vulnerable strcpy, sits at offset 36, more than thirty bytes past that terminator, and this is the struct's only consumer. It is never read.

If the value is discarded, why does configuring it in the router's UI have any effect? The answer is a few lines above the vulnerable copy:

SetValue("sys.timentpserver", ntpServer);   // 0x8b974  <-- persisted here 
CommitCfm();                                // 0x8b978 
... 
strcpy(msg.ntpServer, ntpServer);           // 0x8ba00  <-- same string, copied again

The attacker-supplied value is consequential, but through a different mechanism: it is written to the device's configuration store and committed one statement earlier. The vulnerable strcpy is a redundant second copy of already-persisted data into a struct whose only consumer ignores it — consistent with an older design that did carry configuration to a back-end daemon, later simplified without anyone removing the marshaling code from the caller.

Two things follow. The overflow is still real: the write still reaches the saved return address. That the bytes are never read does not affect exploitability, because the damage is done by the write rather than by any subsequent read. And a patch that removed the call entirely would have been equally effective — replacing the BL with a NOP closes the vulnerability at one changed instruction instead of three, with nothing of value lost.

This also puts the model's reasoning about the 256-byte bound in a different light: that choice was made to guarantee NUL-termination for whatever reads the buffer downstream, and nothing reads it. The reasoning was not defective. NUL-termination is the right property to preserve when you cannot see who consumes a buffer, and the model had no way to see, because we had supplied nothing it could use to look. A conclusion is only as good as the context it is drawn from; the limitation here was the context, not the reasoning applied within it.

Two valid fixes

With the full picture, two fixes were available: bound the copy, or delete it. Both close the vulnerability, and the one produced with the least context is the more conservative of the two.

Bounding the copy preserves the original semantics for any consumer the analysis might have missed. Deleting the call relies on "never read" being exhaustively true, and as we noted in our vendor-patch analysis, you cannot fully guarantee that you have found all the code or that no indirect call reaches a path from somewhere you did not look. Our conclusion here is well-supported, but it is an argument about the code we analyzed rather than a guarantee about every deployed configuration.

This is the practical case for minimal behavioral change: it is the safer choice when knowledge is incomplete. CodeHawk's relational result, with no invariants lost, is the instrument that certifies how little was disturbed. The verification does more than confirm the patch works; it measures the property that matters when there are things you have not seen.

One vulnerability closed is not one device secured

We want to be clear about what this case study does and does not claim.

The unread buffer points at a broader problem in how this firmware is built: the binary's model of the shared library it calls does not match what that library actually does. The caller marshals a 296-byte structure; the callee reads a short string and discards the rest. This is a misuse of the library's API, and it persisted because nothing forces it to surface. It does not crash, it does not fail functional testing, and it produces no visible symptom, until one of the unnecessarily populated fields is filled by an attacker with more data than it can hold. The overflow we patched is less a bug in the time-synchronization logic than a consequence of an interface contract nobody was checking.

It is also not the only instance. Tracing this one path surfaced a second misuse of the same kind, on an unrelated path further down the chain — a more serious one, in library code shared across product lines. It is not reachable from the handler we patched, and we are not detailing it here pending further analysis and disclosure. But we found two contract mismatches while tracing a single strcpy.

Neither was findable from source-level reasoning about fromSetSysTime, and neither is catchable by a compiler. C's separate-compilation model, compounded by dynamic linking, means the compiler building the httpd never sees the library's implementation, only a declared signature, which may come from a long-lived internal header reused across years and models. "The callee only reads the first five bytes of what you are handing it" is a semantic, cross-binary data-flow property, and there is no diagnostic for it. Confirming it required disassembling the shipped shared library and tracing the data flow.

So we closed one vulnerability, in one function, in one binary, and we proved that we closed it. We are not claiming this firmware is now secure. On this evidence it very likely is not. Where one API contract is abused this way, others usually are, and each is a candidate vulnerability waiting for the right field to be attacker-controlled. Our assessment after this investigation is that this represents a small fraction of what is present in this binary, and that finding the rest is a matter of looking.

That framing is also the point of the exercise. This is a step toward binary patching and verification at scale: a repeatable workflow that can run across hundreds of call sites and dozens of binaries, in which the analysis supplies the context, the model proposes the candidate, and the proof decides what ships. The economics support that — the two sessions behind this post cost $8.24 and about 30 minutes of model time combined. The bottleneck is not generating fixes. It is knowing which ones can be trusted, and knowing what has not yet been examined.

Why this matters

DARPA's AI Cyber Challenge showed autonomous systems finding 86% of the synthetic vulnerabilities planted in its final round and patching 68% of them, at an average of about $152 and 45 minutes per task. That result moves the bottleneck to the question we work on: which machine-generated fixes can you trust enough to deploy? Cheap, fluent patch generation makes the verification layer more important, not less.

Both halves of this work followed the same division of labor. In the first session the model proposed and CodeHawk verified. In the second, the model was an effective investigative partner because CodeHawk supplied ground truth at each step: the stack layout, the struct reconstruction, the cross-library disassembly, the invariants. The model was useful in both directions, and in both it is the analysis underneath that makes the output trustworthy.

This is a small version of our Hawkeye work under ARPA-H's UPGRADE program, where machine intelligence proposes remediations for firmware that cannot be rebuilt and sound analysis proves each one eliminates the vulnerability while preserving device behavior. The model wrote a good patch. The verification is what makes it deployable.

If your organization is adopting AI code generation, AI-assisted triage, or automated patching, we work on exactly this: measuring where the models are reliable, and building the verification layer that makes their output safe to ship on systems that matter. Start the conversation at [email protected].

Appendix: the patch, byte for byte

The ELF LOAD segment satisfies file_offset = VA - 0x8000. The complete change is three instruction words:

Result: strncpy(R0=dest, R1=src, R2=0x100) — the copy can never write past the 260-byte buffer, regardless of the length of the attacker-supplied ntpServer string.