Available · MPhil · 2026

An antibotty defensive testbed to protect network services

The mean time to exploit a vulnerability is now negative, as LLM-driven exploitation precedes the publication of a fix. A coding agent needs to be given little more than the class of a bug, and -- combined with the source code -- it can write a working exploit in minutes.

To protect against such fast attacks, we need to find mitigations that are much faster to deploy. We've been proposing antibotty networks to do just this: local, fast-propagating defences that hear about a vulnerability and inoculate their immediate infrastructure within seconds. A filter rule should be smaller and more auditable than a patch, needs no rebuild, and can ship before the fix exists at all.

The research question is whether such antibotty rules can be made trustworthy enough to deploy automatically on somebody else's traffic without a human in the loop.

1 Outline

1.1 A rule language with a proof obligation

The core of this project is a small, total domain-specific language for inoculation rules for network protocols, designed so that the safety properties are either true by construction or discharged to an SMT solver before a rule is allowed near a real network:

  • rejection only. A rule may drop a request or answer it, but never rewrite one into something else.
  • soundness. Every input in the characterised bad set is rejected. The bad set is itself a predicate in the same language, so the rule and the vulnerability it mitigates are written in common.
  • bounded over-blocking. The rule provably rejects nothing outside that set, checked against a captured profile of the traffic it will sit in front of.
  • bounded cost. Linear in the size of its input, so the rule can be on the fast path without becoming a denial of service.

Ideally, the same rules will serve as both the deployed filter and a test oracle that can be replayed over captured traces to check that an implementation and a specification agree.

Prior work includes Bouncer that generated input filters from symbolic execution of the vulnerable path, and Vigilante which proposed self-certifying alerts so that a host could verify a vulnerability claim itself rather than trusting the sender. Neither of these had an LLM on either side though!

1.2 The antibotty gateway

The enforcement point is a MirageOS unikernel doing DHCP, DNS and NAT for a real home network. This is the sort of device that is currently rarely patched. For the sake of experimentation, we assume we can recompile and deploy a fresh unikernel quickly, and using a Linux backend is fine rather than a full Xen or Solo5 one.

1.3 Eval testbed

Evaluation is a contained lab in which two local, open-weight agents race each other from the same starting information. A corpus of real late 2026 vulnerabilities is gathered, and each one reduced to a rumour: one line naming the class of the bug, with no proof-of-concept exploit or patch fix. The attacking agent then turns the rumour into a working exploit while the defending agent turns the same rumour into a candidate antibotty rule.

The key metric is to measure the time-to-exploit vs time-to-verified-mitigation, on the same hardware and from the same rumour set. A "defender win" is a rule that is generated, verified, distributed and blocking the attack before the exploit is deployed. A defender loss is as interesting as a win since it would tell us that the antibotty system needs more rules pre-computed rather than synthesised on demand.

Exploit generation stays inside the virtual lab network at all times, aimed only at the student's own services and using models running locally.

2 Prerequisites

Comfort with or a desire to learn OCaml/Lean4 for the rule language, an interest in lightweight formal methods (SMT for the discharged obligations for example), and a willingness to do gritty systems plumbing in a unikernel.

3 Background Reading