Bringing Aristo to networking infrastructure correctness

We are expanding Aristo, our verification SDK, to networking. As a first demonstration we aimed it at HTTP libraries. Amongst other results, we found a correctness bug in hyper, a popular Rust HTTP library: a request whose headers end in an uncommon but supported way is accepted when it arrives in one piece, and rejected as incomplete when the same bytes arrive in two. We reported it upstream, and it has since been fixed.

Why networking#

Network protocol code is critical for two key reasons. Firstly, it provides load-bearing guarantees and abstractions that the software infrastructure built above it depends on. Secondly, it is subject to untrusted inputs that come from the outside world. Further, these inputs are highly unpredictable, since how bytes arrive depends on the network path, the current system load, and other conditions nobody controls. In a handwritten test, the input arrives in one write; on a real network, the same bytes can arrive in many pieces. That gap holds a whole class of behavior that example-based test suites cannot reach.

Mistakes here are not always benign either. Protocol code sits at a trust boundary, and when an implementation interprets input differently from the components around it, the disagreement itself becomes attack surface: entire attack classes, request smuggling among them, are built on exactly such disagreements, and differential studies of HTTP implementations keep surfacing new ones. Making protocol code interpret input correctly removes the disagreements these attacks depend on, so verifying its correctness is also a security measure.

Underlying method#

Aristo achieves network verification with the same interface described in our blogpost on the verification loop: an intent (a guarantee written as a plain claim), a model that makes the claim precise, and checks that hold the code to the claim on every input it can reach, with the ability to re-run verification as the code changes.

Consider HTTP framing as an example. The intent is a single sentence:

The messages parsed from a connection depend on the bytes alone, never on how those bytes were split across reads.

Our technique developed a formal model of HTTP/1.1 framing and proved that the model satisfies this claim. We then tested hyper against the same claim, replaying byte streams under every possible split and checking whether the outcomes matched.

The first result#

The outcomes matched on nearly every input. They differed on one: a request with an uncommon but accepted header ending. The result is a refusal in the form of a dropped connection. The cause is a fast-path scan that runs only when a request arrives split: it catches some endings of a header block, but not the one in question. We reported it upstream with this diagnosis, and a community fix was merged that extends the fast-path scan to cover the missing ending.

A model-based test systematically asks questions of the code that ad-hoc reviews and example-based tests alone cannot. For hyper, it took a couple of hours to catch a bug. The bug we found is a correctness issue, but as the smuggling discussion above suggests, protocol code carries security guarantees as well. Aristo checks both the same way: stated precisely, checked under every scenario, and re-checked as the code changes.

Work with us#

Aristo is free and open source. The full service runs this method at depth and continuously as the code changes. If you build proxies, gateways, protocol libraries, or anything that parses bytes off a wire, apply to join, or reach us at hello@aretta.ai.