AI & AgentsSecurity tooling · Hackathon

Hemostat

Repair a binary you have no source for — offline — and prove the repair

Status: Hackathon prototype
Year: 2026
Rooms: AI & Agents, ML & Impact

$ ./demo.sh
stack_overflow   unbounded strcpy  (CWE-121)   PROVEN    0x401190
off_by_one       i <= n loop bound (CWE-193)   PROVEN    0x401228
format_string    printf(user_input)(CWE-134)   BOUNDED   —

FIND+READ 13.9s   WRITE 0.1s   SPLICE 3.2s   PROVE 2.9s   TOTAL 20.2s
remote connections: 0 (strace-verified)   disk: 8.6 GB

Problem

Air-gapped Linux machines run vendor binaries without source. When one has a memory-safety bug, online AI tools, source-level linters and antivirus can't fix it.

Approach

The Sanjeevani pipeline takes a stripped ELF binary and nothing else: fuzz it to a crash, lift the faulting function back to C, write a fix, splice it into the binary, and prove the bug is gone while behaviour elsewhere is unchanged.

Engineering decisions

Fully offline after a one-time model download; zero remote connections, verified with strace.
Template repairs first, a local Qwen2.5-Coder model only when a template doesn't fit.
Symbolic verification with angr + Z3 reports PROVEN or BOUNDED — it never overstates.

What it does

FIND · AFL++ (QEMU mode)
READ · gdb + Ghidra
WRITE · templates / local Qwen
SPLICE · Patcherex2
PROVE · angr + Z3

Stack

Python
AFL++
Ghidra
Patcherex2
angr
Z3
llama.cpp

My part

Built with Purvesh Mhatre and Pranav Shripannavar for Terrier Cyber Quest 2026 (AI Kavach track); 14 of 16 commits are mine.

Team: Sahil Karande, Purvesh Mhatre, Pranav Shripannavar

Limits, stated plainly

Demonstrated on three planted bug classes in demo binaries, on one machine without a GPU.
The format-string case is bounded verification, not a full proof.

Evidence

Hemostat README: results table and per-binary timings