The language of formal reasoning is often used in applied computer science to characterize the properties of engineered systems. In a recent post, I described how the Internet’s Transport Control Protocol (TCP) is typically described as “reliable” when in fact it only reduces the occurrence of certain kinds of error. Treating TCP as if it were completely reliable simplifies network programming by ignoring the consequences of error. This is just one example of the widespread use of the reassuring, but misleading, formal language.
Any formal proof tells us that, if its assumptions are valid, and the rules of the logic are sound, then its consequences will hold. Since any engineered system will differ from the formal model on which such a proof is based, direct application of its predictions in the real world is necessarily fallacious. To understand the fallacy, we must find which element of the proof fails.
Some striking examples of such fallacies stem from proofs of fault tolerance. It is a well-known formal result that a reliable distributed system cannot be implemented using one that has no limits on the number and type of communication errors that can occur. There is a whole category of fault-tolerant algorithms that make the reasonable-seeming assumption that there is a fixed bound on the number of errors that will occur during its execution. This may be justified by pointing out an assumption commonly made in probabilistic reasoning, namely the independence of errors. If errors are independent, then the probability of there being more than some (possibly large) number of errors N during the execution of an algorithm will be very small.
The problem with algorithms based on such bounds is that they fail when more than the assumed limit of N errors occurs. This can happen when the occurrence of errors is not in fact independent due to any of a number of real-world considerations. These include common software (such as Linux) used in many computer systems, hardware design flaws, and the presence of malicious actors. The formal proof provides a roadmap of assumptions, some of which the real world will violate.
Lest the reader think that this criticism is purely academic, I point out that the widely used distributed consensus algorithm used in implementing blockchain has several vulnerable assumptions, including:
- 51% Attack (a victim node is overwhelmed by malicious neighbors)
- Integer Overflow (the victim ignores an unexpected error mode)
- Routing Attacks (messages are maliciously delayed, misdirected, or dropped)
Consider an analogy. Ice hockey is a dangerous game due in part to the use of a dense, fast-moving puck. It is important that the organizers of the game be seen to protect the players. A Mad magazine hockey primer1 described the padding which protects every inch of the goalie’s body except “1½ inches of his neck.” It then goes on to explain:
“What is the object of the game of Ice Hockey?
To hit the Goalie
With the Puck
In the neck.”
In any application of a formal proof to the real world, unrealistic assumptions are the gaps which leave the neck of the application exposed to attack.
Another example of the use of formal language to mischaracterize practical systems concerns deadlock in concurrency control. Operating system textbooks explain to students the proof that there are four conditions which must hold for a system to be in deadlock:
- Mutual Exclusion (a lock can be held by at most one process at a time)
- Hold-and-Wait (a process which has exclusive use of one resource can wait for access to another)
- Non-revocation (access to a resource, once granted, cannot be rescinded)
- Circular waiting (a cycle exists in the graph of waiting processes).
The processes involved in circular waiting will never stop waiting and so can never make any progress.
The problem with this proof is that there are almost no practical systems where non-revocation actually holds. If a deadlock does occur in a real system and it becomes partially or completely unresponsive, the universal solution (perfected by the users of Microsoft Windows) is to turn it off and then back on again. This has the effect of revoking all locks and regenerating all processes. In POSIX-like operating systems, a deadlock can usually be broken by the receipt of a signal which wakes a waiting process.
The reality of deadlock is that it is a condition that holds as long as the four conditions listed all apply. During that time, no progress will be made by the circularly waiting processes. Temporary deadlock can be used in the correct design of a system when the factors that can end (by revoking a lock or killing a process) are part of that design. This fact greatly complicates the analysis of deadlock and is not generally taught. Instead, we teach a simple proof based on a model of process management which predates interactive computing. Because we like to teach students about proofs, and it makes the field of operating systems seem more rigorous.
The misuse of formal language so permeates applied computer science that it is impossible to convince practitioners to speak in more realistic terms. Examples of reality-based observations include:
- No archive is permanent. Even a highly durable storage medium is connected through interfaces and protocols with limited lifetimes (some as short as five years).
- Computation is not accurate. Every wire, gate, and storage cell has a non-zero probability of error, and software is much less stable.
- No system is secure. Every physical behavior leaks information through some side channel, and every program makes an assumption or has a logic error that can be a vulnerability.
In all such cases, application developers are trained to make assumptions which contradict the truth, and which result in unanalyzed vulnerabilities to error and malicious exploitation.
1. The Goalie, The Mad Ice Hockey Primer, Mad Magazine #125 March, 1969. Written by Larry Siegel. Illustrated by Jack Davis
Micah D. Beck (mbeck@utk.edu) is an associate professor at the Department of Electrical Engineering and Computer Science, University of Tennessee, Knoxville, TN, USA.