New Year's Eve-Proofing Your Specifications

This post explores the benefits of explicitly listing invariants as part of a specification.

On an unsuspecting New Year’s Eve, the few lines of C code shown below nearly crippled the Internet, raking up half a billion dollars in damages.

The heartbleed bug

The code in question implements a new “Heartbeat” specification for the TLS encryption protocol, aiming to solve an important bottleneck: establishing a new TLS connection is expensive. The specification proposes that the sender post an arbitrary “heartbeat” message to the recipient. The recipient interprets this as a signal to keep the connection alive and confirms by echoing the message back to the sender.

Neat. But the code had a fatal flaw: it trusts that the sender reports correct length of the message.

The recipient didn’t check.

This gives the sender an opportunity to blatantly lie about the message length, tricking the recipient into leaking extra information from memory back to the sender.

The now infamous bug, cleverly named Heartbleed, lets a malicious sender peek behind the TLS curtain and expose contents from memory. In a twist of cosmic irony, it often reveals exactly the information that TLS is designed to protect—such as private keys or login credentials.

Here is an exploited memory dump with sensitive information exposed:

Interestingly, the specification casually notes to “silently discard” this edge case:

Could we better nudge implementation do what it says on the tin?

More unit tests? Yes.

No deployments on New Year’s Eve? A necessary sacrifice, sure.

But the why is rather hidden in plain sight. Throughout a specification, we bury its structural integrity—its invariants—in easy to miss normative prose.

What if we didn’t?

First-class spec invariants

Fortunately, Ethereum’s specs are executable (see: consensus specs & execution specs), which adds to their robustness. But there are compelling advantages to having explicitly defined invariants as part of the specs.

First, we get standardized errors for free. Currently, errors are a fragmented mess across clients.

For instance, consider the following excerpt from EIP-7623:

Any transaction with a gas limit below 21000 + TOTAL_COST_FLOOR_PER_TOKEN * tokens_in_calldata or below its intrinsic gas cost (take the maximum of these two calculations) is considered invalid. This limitation exists because transactions must cover the floor price of their calldata without relying on the execution of the transaction. There are valid cases where gasUsed will be below this floor price, but the floor price needs to be reserved in the transaction gas limit.

For the exact same spec, geth has two errors, while the testing framework has just one.

Plus, in the absence of standard error codes, the testing framework falls back on client-specific error messages to detect errors:

A typo or slight change in the client error message can lead to outcomes ranging from a benign false positive to a gaping security hole. The mechanism is so abysmally delicate that you can almost hear it creaking.

First-class invariants in specs eliminate the guesswork:

The outcome is a precise protocol-wide violation. Its testable - across clients, across versions, across decades.

Second, explicitly defined invariants in both the specs and their executable versions make formal verification simpler, helping spot conflicts as the protocol grows complex. Hopefully, implementation teams will keep enriching specs with any new invariants they find along the way—it’s a win-win.

Specs shouldn’t whisper invariants. They should yell them.

Thanks to Dan, Guillaume, Ignacio, Justin, Kev, and Pari for discussions and feedback.

References

• Diagnosis of the OpenSSL Heartbleed Bug
• Heartbleed, Bruce Schneier
• Critical crypto bug exposes Yahoo Mail, other passwords Russian roulette-style
• Relevant xkcd