# An antibotty defensive testbed to protect network services *2026-08-01 — idea* The mean time to exploit a vulnerability is now [negative](https://anil.recoil.org/notes/rumour-is-the-exploit), 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](https://anil.recoil.org/papers/2025-internet-ecology) 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_. ## Outline ### 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](https://anil.recoil.org/ideas/nqsb-tls) that can be replayed over captured traces to check that an implementation and a specification agree. Prior work includes [Bouncer](https://doi.org/10.1145/1294261.1294274) that generated input filters from symbolic execution of the vulnerable path, and [Vigilante](https://doi.org/10.1145/1455258.1455259) 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\! ### 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. ### 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](https://anil.recoil.org/notes/internet-immune-system) 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. ## 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. ## Background Reading - [Just a rumour of a bug is enough to find a security exploit these days](https://anil.recoil.org/notes/rumour-is-the-exploit) and [The Internet needs an antibotty immune system, stat](https://anil.recoil.org/notes/internet-immune-system) for the motivation, and [Steps towards an Ecology for the Internet](https://anil.recoil.org/papers/2025-internet-ecology) for the antibotty network the gateway would join. - [LLM Agents can Autonomously Exploit One-day Vulnerabilities](https://arxiv.org/abs/2404.08144), Fang et al, 2024. - [Demystifying the Mythos or Disrupting Bugonomics?](https://arxiv.org/abs/2605.24632), Pesoli et al, 2026, on where defender capacity actually runs out. - [Bouncer: securing software by blocking bad input](https://doi.org/10.1145/1294261.1294274), Costa et al, SOSP 2007. - [Vigilante: End-to-end containment of Internet worm epidemics](https://doi.org/10.1145/1455258.1455259), Costa et al, TOCS 2008. - [Not-Quite-So-Broken TLS](https://anil.recoil.org/papers/2015-usenixsec-nqsb) for the dual-role specification-as-implementation style, and [Unikernels: library operating systems for the cloud](https://anil.recoil.org/papers/2013-asplos-mirage) for the unikernel the gateway is built from. Status: Available Level: MPhil Year: 2026 Project: Unikernels Supervisors: Anil Madhavapeddy ## Related - [Just a rumour of a bug is enough to find a security exploit these days](https://anil.recoil.org/notes/rumour-is-the-exploit) (note, 2026-08-22) - [The Internet needs an antibotty immune system, stat](https://anil.recoil.org/notes/internet-immune-system) (note, 2026-04-08) - [Steps towards an Ecology for the Internet](https://anil.recoil.org/papers/2025-internet-ecology) (paper, 2025-08-01) - [Not-Quite-So-Broken TLS](https://anil.recoil.org/papers/2015-usenixsec-nqsb) (paper, 2015-08-01) - [Not-quite-so-broken TLS in OCaml](https://anil.recoil.org/ideas/nqsb-tls) (idea, 2014-01-01) - [Unikernels: library operating systems for the cloud](https://anil.recoil.org/papers/2013-asplos-mirage) (paper, 2013-03-01) --- Canonical: https://anil.recoil.org/ideas/antibotty-testbed Type: idea Tags: security, mirageos, ocaml, formal, ai