Miller’s 7±2

George A. Miller, “The Magical Number Seven, Plus or Minus Two” (Psychological Review, 1956): working memory can hold approximately 7 ± 2 independent chunks at a time. The result is one of the most-cited findings in cognitive psychology, though modern refinements (Cowan 2001: ~4 chunks) suggest Miller’s estimate was generous.

The implication for system and language design: interfaces, specifications, and protocols that require a reader to track many independent elements simultaneously will be misread. A developer cannot hold in working memory every possible control-flow path of a Solidity contract when there are implicit behaviours (Fallback Method, Delegatecall) lurking at the call site.

House on Rock - LangSec in Ethereum Classic invokes 7±2 alongside Processing Fluency to argue that the EVM’s contract model overruns the developer’s cognitive budget — hidden state changes, implicit sends, and reentrancy opportunities cannot all be tracked simultaneously, so bugs slip through.

Tags

#cognitive-psychology #working-memory #usability

Backlinks

House on Rock - LangSec in Ethereum Classic line 44

Linked Pages

Processing Fluency

The subjective ease with which information is cognitively processed (Reber, Winkielman, Schwarz and others, cognitive psychology ~1990s–2000s). Fluent stimuli — familiar words, simple shapes, rhymes, short sentences — are judged as more true, more likeable, more trustworthy, and more probable than dis-fluent ones, even when the underlying evidence is identical. This is the truth effect and its many cousins.

Processing fluency is the cognitive mechanism behind several security-relevant failure modes: phishing pages that mimic the visual “look” of legitimate sites exploit fluency; dense legalese in smart-contract ToS reduces fluency and thereby perceived risk; and — more subtly — fluent LLM prose is judged more credible than equally-reliable but less fluent text (Epistemia, Epistemological Fault Lines Between Human and Artificial Intelligence).

House on Rock - LangSec in Ethereum Classic invokes processing fluency to explain why Solidity code that looks like JavaScript is trusted more than its semantic hazards warrant: the fluency of the surface syntax imports misplaced confidence.

Tags

#cognitive-psychology #ui #security

House on Rock - LangSec in Ethereum Classic

Reference: Meredith L. Patterson (2017). How to Build a House That Doesn’t Fall Apart (talk). Ethereum Classic Summit, Hong Kong, November 2017. YouTube

Summary

A LangSec critique of Ethereum aimed at the Ethereum Classic community, framed around the parable of the wise and foolish builders and Philip K. Dick’s “reality is that which, when you stop believing in it, doesn’t go away.” Patterson argues Ethereum was built on sand — an ad-hoc, non-executable yellow-paper semantics; a hand-rolled Solidity parser; a test suite with no coverage for delegatecall or invalid opcodes; a design culture that scorned formal methods until hundred-million-dollar losses forced the issue.

The central technical argument is that the gas mechanism does not do what the yellow paper claims it does. Gavin Wood’s stated purpose — “sidestep the inevitable issues stemming from Turing completeness” — confuses a resource bound (a non-semantic, decidable property) with a safety guarantee (a semantic property that Rice’s theorem makes undecidable in general). Gas cannot show a contract “does nothing malicious”; it can only show it eventually halts. Worse, gas creates an adversarial economic game with direct monetary reward for tricking the accounting, and a perverse incentive for honest developers to omit runtime sanity checks because conditionals cost gas.

Patterson’s prescription for Ethereum Classic: standardise on KEVM (an executable operational semantics in the K framework), fix the VM test suite’s gaps, build languages that don’t hide implicit behaviour (method visibility defaults, fallback methods, delegatecall as naked eval), and invest in developer tools — IDEs, live debuggers, verification — that surface what a contract can actually do. “Code is law” requires the meaning of the code to be unambiguous, executable, and visible.

Key Ideas

Rice’s theorem bounds what gas can mean. Non-trivial semantic properties of arbitrary programs are undecidable; resource bounds are non-semantic. Gas therefore cannot sidestep Turing-completeness-induced safety problems, contrary to the yellow paper.
Gas as adversarial game. The accounting is an attack surface, not a safety property; attackers are paid to win. Honest contract authors are weakly pushed toward removing checks to keep gas costs competitive.
LangSec programmer–machine contract. Inputs must have a formal grammar; two implementations of the same spec must accept/reject identical inputs; semantics must be executable so claims about behaviour can be verified mechanically.
Ad-hoc semantics breeds consensus failures. When the yellow paper and cpp-ethereum disagree, cpp-ethereum wins — the denotational semantics is decorative. Discrepancies between clients have already caused real Ethereum consensus failures.
Test suites are part of software design. Official VM tests have no coverage for invalid opcodes or delegatecall — the exact instruction at the heart of the Parity multisig hacks. “VM tests” is false advertising; downstream VM implementations inherit the blind spot.
Case studies of processing-fluency failure.
- DAO: mutual recursion across a defender/attacker code boundary, missed in reviews because reviewers examine functions one at a time (cf. Leveson: accidents emerge from interactions).
- Hacker Gold: =+ typed instead of += — a hand-rolled recursive-descent parser caught nothing; a Bison grammar would have surfaced a shift/reduce conflict.
- Parity multisig (July 2017): fallback method × delegatecall × public-by-default visibility = naked eval on attacker-controlled payload; $31M drained, $150M saved only by counter-theft.
- Parity multisig (Nov 2017): library contract re-initialised by an outsider then suicided, locking $153M in wallets whose code had vanished — “left-pad for multi-million-dollar table stakes.”
KEVM (K framework operational semantics) gives Ethereum an executable semantics; generated interpreter ~20× slower than cpp-ethereum but usable, and supports reachability-based proof of safety/liveness claims.
Cognitive-science constraint. Miller’s 7±2 bounds how much implicit state a programming language can demand before human reasoning fails. Solidity’s implicit defaults (public methods, fallback dispatch, implicit conversions) exceed that budget.
“Worse is better” is unconscionable in a financial system. Sacrificing correctness and completeness to ship first transfers the cost of undefined behaviour onto users.

Connections

Making Smart Contracts Smarter — same semantic gap diagnosis; OYENTE is the symbolic-execution complement to Patterson’s formal-semantics prescription.
Formalise Blockchain Interoperability Patterns — companion move: formalise what was informal.
Security Applications Of Formal Language Theory — the Sassaman/Bratus/Patterson LangSec manifesto this talk operationalises for smart contracts.
The Halting Problems of Network Stack Insecurity — parallel argument that parser/semantics weakness is the root cause of whole vulnerability classes.
Exploit Programming - From Buffer Overflows To Weird Machines — “weird machines” framing applies directly to contracts driven off-spec via delegatecall.
PKI Layer Cake - Kaminsky Patterson Sassaman — Patterson’s earlier demonstration that grammatical discrepancies between implementations are exploitable (SSL CA forgery); same mechanism, different domain.
A Language-Based Approach To Prevent DDoS — language-theoretic remediation as a general pattern.
Operational Semantics, Denotational Semantics, EVM, Solidity, TheDAO, Reentrancy — background concepts.
An Unsolvable Problem of Elementary Number Theory — Church 1936; LangSec’s undecidability heritage behind the Rice’s-theorem argument against gas-as-safety.
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I — Gödel 1931; the incompleteness ancestor of the semantic-limit arguments.

Conceptual Contribution

Delegatecall

An EVM opcode that invokes code at another address in the caller’s storage context. The called bytecode can read and write the caller’s storage, spend the caller’s Ether, and see the caller’s msg.sender. In effect, delegatecall is a naked eval: whoever controls the target address controls the caller’s state.

The opcode exists to enable library patterns and upgradable proxy contracts, but its semantic reach makes it the sharpest available knife in Solidity. The July 2017 Parity multisig wallet freeze (Parity Multisig) was triggered by an untrusted actor invoking a library’s initializer via delegatecall, taking ownership of the library, and then self-destructing it — rendering every wallet that delegated to it unusable and freezing ~$280M of Ether.

House on Rock - LangSec in Ethereum Classic lists delegatecall with the Fallback Method as examples of implicit behaviour incompatible with LangSec: the call site doesn’t locally express what the code can do.

Tags

#solidity #evm #smart-contracts #langsec

Fallback Method

In Solidity, the unnamed function a contract invokes when it receives a call whose signature doesn’t match any declared method (or when it receives plain Ether). Prior to Solidity 0.6 it was function() { ... }; since 0.6 it is split into fallback() and receive().

Fallback methods are a canonical Solidity foot-gun: they execute code on every unknown call, including calls from untrusted counterparties, and they run in a context where the caller’s identity, the amount of Ether received, and the remaining gas are easy to misreason about. The DAO reentrancy exploit (TheDAO) and several Parity-wallet incidents (Parity Multisig) turned on fallback-method behaviour.

House on Rock - LangSec in Ethereum Classic cites the fallback method as a language design that hides implicit behaviour — the opposite of what a LangSec approach prescribes.

Tags

#solidity #smart-contracts #langsec