ANT FARM

What this is

A deterministic semantic model of AegisGenera's routing rules. The gateway acts as a reference monitor⁶: every message is checked against Passport's edge and verb maps, delegation is checked against the origin's rights⁵, replies must answer a real request, and hop limits, rate limits⁷, a message deadline and revocation by epoch apply. Routing is either plain shortest paths, which can deadlock², or Autonet's up*/down* routing¹, which provably cannot.

The agents follow simple rules, which is enough to surface emergent failure, the way simple traffic models reproduce real stop-and-go jams³. Every agent here obeys its rules, and the colony can still fail, like an ant mill⁴. It is not a throughput benchmark and not the proved build. The same engine runs headless under a fuzzer that checks every invariant.

AegisGenera is being built to enforce these rules on real agent traffic, with a formally proved policy core. Learn more →

Andon states

Pulling an Andon cord⁸ on a road closes it: nothing new enters, and routing recomputes around it. The policy decides what happens to messages already on that road:

Hold. The message stops where it is and keeps its place. When the cord is released it carries on. Nothing is lost; only time.
Drain. Messages already on the road clear it, then follow the new routes. Nothing new enters. The road empties without losing work.
Reject. The message is removed and its sender is told it was refused. Nothing waits; the sender decides whether to retry.

A message whose destination is cut off entirely (an isolated neighbourhood, or Andon all) is set aside at the junction under Hold and Drain, so it doesn't block traffic behind it, and refused under Reject. Under Autonet routing¹, no combination of pulled cords has produced a deadlock in 300 seeded runs; under shortest paths, about 4 in 10 did. Timing matters: isolating a neighbourhood half a second after a storm starts contains it completely; at six seconds most of it is contained; after fourteen seconds it has escaped and the rest of the colony slows down.

Trusted and outside agents

Inside agents are trusted: each holds a key and every message it sends carries its signature. The three outside agents (X, lower right, behind the dashed fence) are unsigned and stay outside the graph. Passport gives them exactly one edge each, to the border agent (B). The border does not forward their messages. It asks inside under its own name, using discovery to pick a responder, then maps the inside reply back to the outsider's request. An outside identity never travels inward, so no inside agent ever has to decide whether to trust an outsider.

In ten seeded runs of the Outside flood vs inside storm recording, a flood from all three outside agents cost the interior about 4% of its useful work (4.9 vs 5.1 per second). The border's own rate budget is what the flood meets, so outsiders are answered at about 1 per second and every other request gets a definite "no feasible responder". A single compromised trusted agent did far more damage: messages in flight rose from about 16 to 88. Revoking it made things worse for a while (useful work fell to 3.1 per second against 4.3), because the alarms it had already started kept relaying through agents that were each authorized to relay. The hop limit is what drained them.

One test: the Feasible Execution Set

Every check the gateway makes is one term of a single predicate. A request is accepted only if the plan it belongs to is in the feasible set right now:

F(t) = { p ∈ Plans(q) | A(p,t) ∧ B(p,t) ∧ R(p,t) ∧ E(p,t) ∧ ¬H(p,t) }

E, evidence: signed, and not revoked. B, boundary: the perimeter (outside agents reach only the border; the border answers them only with replies; no outside identity is carried in) and isolation. A, authority: Passport's edge and verb map, the confused-deputy check⁵, and reply tracking. R, resources: hop limit, rate limits, queue space and the deadline. H, halt: Andon. The gateway tests the terms in that order and denies on the first that fails, so the denial panel groups every refusal by the term that caused it. Two properties hold by construction: pulling a cord can only shrink F(t), never grow it; and every request ends in a definite outcome (delivered, denied with a reason, refused, expired, or "no feasible responder"), never silence. The fuzzer checks the parts that can go wrong in code: nothing enters a pulled road, nothing outside crosses the perimeter, and every answer discovery gives passes the gateway.

Capability discovery

Half of ordinary work, and everything the border asks on an outsider's behalf, names a capability rather than an agent: price (desk), records (data), risk (data and compliance) or audit (compliance). The resolver asks the same FES test about each candidate and offers only responders inside F(t) that a route can reach. Among those it takes the least exposure first (staying inside the requester's own neighbourhood beats crossing out of it), then the least cost (hops plus the responder's queue). Point-to-point requests need no travelling-salesman search: one responder, one route. The fuzzer re-checks every answer the resolver gives against the gateway.

Notes

1. Up*/down* routing (Autonet). M. D. Schroeder, A. D. Birrell, M. Burrows, H. Murray, R. M. Needham, T. L. Rodeheffer, E. H. Satterthwaite and C. P. Thacker, "Autonet: a high-speed, self-configuring local area network using point-to-point links," IEEE Journal on Selected Areas in Communications 9(8):1318–1335, 1991 (DEC Systems Research Center). Build a spanning tree from a root, so every road points "up" toward it or "down" away from it. A legal route climbs zero or more times, then descends, and never climbs again. That rules out circles of waiting, so the network cannot deadlock on any map, at the cost of some longer routes. Here the root is the orchestrator hub.
2. Why circles of waiting matter. W. J. Dally and C. L. Seitz, "Deadlock-free message routing in multiprocessor interconnection networks," IEEE Transactions on Computers C-36(5):547–553, 1987. Fixed routing is deadlock-free exactly when the graph of "this road waits on that road" has no cycles. Shortest paths can create one under load; up*/down* can't. A pure tree, like the Sparse map, has none to begin with.
3. Cars as cells. K. Nagel and M. Schreckenberg, "A cellular automaton model for freeway traffic," Journal de Physique I 2(12):2221–2229, 1992. One car per cell, move when the next cell is free, hesitate now and then: rules that simple reproduce real stop-and-go traffic. This model uses the same idea for messages.
4. The ant mill. T. C. Schneirla, "A unique case of circular milling in ants, considered in relation to trail following and the general problem of orientation," American Museum Novitates 1253, 1944; first described by William Beebe in 1921. Army ants following one another's trail can circle until they die. Every ant follows its rules; the colony fails anyway. The loop pair and alarm storm here are the agent version.
5. Confused deputy. N. Hardy, "The Confused Deputy (or why capabilities might have been invented)," ACM SIGOPS Operating Systems Review 22(4):36–38, 1988. A program acting for someone else uses its own authority instead of theirs. The "deputy" check denies a delegated request the original requester couldn't make itself.
6. Reference monitor. J. P. Anderson, Computer Security Technology Planning Study, ESD-TR-73-51, U.S. Air Force Electronic Systems Division, 1972. A mechanism that checks every access against policy and can't be bypassed or tampered with. AegisGenera's gateway plays that role for agent messages.
7. Token buckets. The standard rate limiter: each sender, and each sender-to-receiver edge, earns tokens at a fixed rate up to a small cap, and every message spends one. Bursts are allowed; sustained floods aren't.
8. Andon. T. Ohno, Toyota Production System: Beyond Large-Scale Production, Productivity Press, 1988 (first published in Japan, 1978). Any worker can pull a cord to stop the line when something is wrong; the problem is fixed at the source instead of being passed downstream. Here the cord stops a road.
9. Changing routes while traffic flows. J. Duato, O. Lysne, R. Pang and T. M. Pinkston, "A theory for deadlock-free dynamic network reconfiguration. Part I," IEEE Transactions on Parallel and Distributed Systems 16(5):412–427, 2005; O. Lysne, T. M. Pinkston and J. Duato, "Part II: A methodology for developing deadlock-free dynamic network reconfiguration processes," ibid. 428–443. Two routing functions that are each deadlock-free can deadlock while a network moves from one to the other. Two of the bugs found while building this model were exactly that.
10. Virus throttling. M. M. Williamson, "Throttling viruses: restricting propagation to defeat malicious mobile code," ACSAC 2002; J. Twycross and M. M. Williamson, "Implementing and testing a virus throttle," USENIX Security 2003. Limit how fast a machine can contact new peers, and spread slows to a crawl while normal traffic barely notices. A natural automatic trigger for an Andon cord.
11. Signcryption. Y. Zheng, "Digital signcryption or how to achieve cost(signature & encryption) ≪ cost(signature) + cost(encryption)," CRYPTO '97, LNCS 1294:165–179, Springer, 1997. Signature and public-key encryption in one logical step, at a cost well below doing both.
12. Macaroons. A. Birgisson, J. G. Politz, Ú. Erlingsson, A. Taly, M. Vrable and M. Lentczner, "Macaroons: cookies with contextual caveats for decentralized authorization in the cloud," NDSS 2014. Bearer tokens built from chained HMACs, which anyone holding one can narrow but nobody can widen.

Research questions

Open questions this work raises, listed for transparency. Each is labelled shown here where the model already demonstrates the effect, partly where it shows part of it, and open where it doesn't yet. None is a claim of novelty; prior art is in the notes.

1	Changing the rules without stopping the traffic. partly Two of our bugs (mixing old and new route plans while a road drains; keeping a car's "already descending" state after the map re-orients) are the transition hazards studied in dynamic network reconfiguration9. Here the network is a policy graph that changes on every Passport update. What is the cheapest transition rule that is still provably deadlock-free?
2	The Feasible Execution Set as a formal object. partly The model has one evaluator, Andon can only shrink F(t), and every request has a definite outcome. Can those be proved, along with a bound on how long a pulled cord takes to stop everything it should? Can F(t) be maintained incrementally when one edge changes?
3	When to pull the cord. partly Isolating half a second after a storm starts contains it; after fourteen seconds it has escaped. Can a cord be pulled automatically from cheap signals, such as the rate of contacts to new peers10, and what does a false pull cost?
4	Failure with every message authorized. shown here Loops and storms bring the colony down while every single message passes every check, and revoking the agent that started a storm doesn't stop it. Which colony-level properties can a per-message reference monitor enforce, and which need something else?
5	Signcryption for agent messages. open The evidence term needs every message authenticated and many of them confidential, at gateway line rate. Signcryption11 does both in one step for less than the cost of signing then encrypting. What do the per-message budget, key management and post-quantum options look like for agent traffic?
6	Answers that cross a boundary. open Re-origination keeps outside identities out, but outsiders still receive answers. What should an answer carry so the outsider can check it came from inside F(t), without learning the interior graph? Zero-knowledge proof obligations are one candidate.
7	Delegation that can only narrow. open The deputy check today looks up the origin's rights in Passport. Attenuable tokens12 carry the narrowing with the request. Can Passport's edge map compile into such caveats and be checked at the gateway for the cost of a few hashes?
8	Discovery that leaks nothing. open The resolver returns only feasible responders, but a requester that probes many capabilities can still map the colony from the answers. How little can discovery reveal, for example using private set intersection, and still pick a good responder?
9	Choosing a plan inside F(t). partly One responder per request, least exposure then least cost. Multi-step work (gather records, then risk, then audit) is a choice among plans, each of which must stay feasible while it runs. What is the right objective, and how does it behave as F(t) shrinks mid-plan?
10	Queues at the gateway. shown here A message whose destination was cut off blocked everything behind it until it was parked aside (virtual output queues). What does a queueing model of the gateway under Andon and isolation predict for latency, and where does it break?
11	A proved core with this model as its oracle. open The production policy core is meant to be written and proved in SPARK. This engine and its fuzzer, which catches each of fourteen deliberate rule breaks, could serve as a differential-testing oracle for it. How far can model-based and proof-based assurance meet?
12	Many colonies. open In production each company runs its own colony, and a marshaller watches many. Deadlock freedom, discovery and Andon across colonies joined only at their borders are all open, as is what the marshaller may see.

Watch a recording

General Reasoning, Inc.