Reading
We will read and discuss 5 papers this quarter. Several of the readings are relatively non-technical; they're intended to foster discussion and get us thinking about the "big picture" for software reliability and verification.
Please submit reading reflections via the 505 Gradesope. See the 505 Overview section on readings for more information on how to write reflections as well as grading and discussion details.
Reading 1 : Reflections on Trusting Trust
Paper: Reflections on Trusting Trust - Ken Thompson - 1984
Reflection Due: April 2 by 5pm PT
When we try to reason about and guarantee the reliability of a computer system, we must start by assuming the reliability of at least some basic components. These components are generally known at the Trusted Computing Base (TCB). If any component in our TCB is not reliable, then any of our guarantees may be arbitrarily violated. In his brief 1984 Turing Award acceptance speech, Ken Thompson vividly illustrates how trusting the TCB may involve a long chain of assumptions. This chain of trust can go back many years through many versions of basic components whose reliability we typically take for granted, e.g., the compiler. This raises interesting questions like: Is there such a thing as an undetectable backdoor? (Note: Some of the figure labels in this transcript are incorrect.)
[OPTIONAL] If you liked this paper, you may also be interested in:
Reproducible Builds: Increasing the Integrity of Software Supply Chains - Lamb, Zacchiroli - 2021
Bootstrapping with T-Diagrams and Reflections on Trusting Trust
Short Computerphile videos overviewing how compilers can build themselves and discussing "Trusting Trust".
What is a coder's worst nightmare?
A (perhaps apocryphal?) story of a "Trusting Trust" style attack uncovered in the wild.
Reflections on Trusting Trust Revisited - Spinellis - 2003
This brief CACM article provides an update 20 years after the original Trusting Trust paper showing that folks were still working on many of the same issues.
Cory Doctorow also wrote a bit on Trusting Trust this in 2020 discussing the same issues -- nearly 40 years after the original talk!
Fully Countering Trusting Trust through Diverse Double-Compiling (DDC) - Wheeler - 2009
In his PhD thesis, David Wheeler developed a countermeasure to "Trusting Trust" style attacks.
Bruce Schneier wrote a short blog post summarizing the high-level ideas in Wheeler's DDC defense.
Sometimes the compiler is buggy! See the Delphi case and subtle floating point + concurrency issues.
How can we gain confidence proof assistants are correct? See the de Bruijn Criteria and work on verifying (parts of) proof assistants IN proof assistants.
Even if we could trust our compilers, should we trust our hardware?
Reading 2 : Social Processes and Proofs of Theorems and Programs
Paper: Social Processes and Proofs of Theorems and Programs - DeMillo, Lipton, Perlis - 1979
Reflection Due: April 16 by 5pm PT
Is proving the correctness of a program the same as proving a mathematical theorem? Why do we even believe in the correctness of proofs? In this classic paper, DeMillo et al. argue that formal verification of programs is NOT like mathematics at all and that the very notion of proving programs is a sort of category error. The authors go on to argue that, even if we could formally verify programs, the nature of software engineering means that verification will never be an effective technique in practice. (Note: this paper unfortunately exhibits some problematic gender norms.)
[OPTIONAL] If you liked this paper, you may also be interested in:
Proof of a Program: FIND - Tony Hoare - 1971
This seems to be the flavor of verification that DeMillo et al. are arguing against.
How Did Software Get So Reliable Without Proof? - Tony Hoare - 1996
Decades later, Hoare reflects on how software engineering practices (e.g., design for test) have enabled reliability without verification.
Counterexample to Euler's Conjecture on Sums of Like Powers - Lander, Parkin - 1966
Perhaps the shortest paper ever published in a math journal?
Open source communities develop extensive social processes to improve reliability.
But, they do rely on good-faith contributions. Some research on the Linux kernel shows how this might go wrong.
Checking a Large Routine - Alan Turing - 1949
Even earlier considerations toward checking software correctness!
Social Processes, Program Verification, and All That - Asperti, Geuvers, Natarajan - 2009
A retrospective response to DeMillo et al.
More Debate, Please! - Moshe Vardi - 2010
A CACM article still sparked debate between Vardi and DeMillo on these topics 40 years after Social Processes was first published!
See also the flood of letters to the editor of CACM when the paper was first published in 1979.
Titans of Mathematics Clash Over Epic Proof of ABC Conjecture
In 2012, a famous Arithmetic Geometer (Shinichi Mochizuki) published a series of massive papers, difficult to read even by mathematicians in the field, claiming to prove the famous ABC conjecture. This article discusses how the social process of mathematics has yet to conclude whether the proof is valid or not.
Proving Theorems with Computers - Kevin Buzzard - 2020
Kevin Buzzard gives a view of how proof assistants are starting (and may continue) to influence the math community.
Reading 3 : Use of Formal Methods at Amazon Web Services
Paper: Use of Formal Methods at Amazon Web Services - Newcombe, Rath, Zhang, Munteanu, Brooker, Deardeuff - 2014 (CACM version)
Reflection Due: April 30 by 5pm PT
Testing is a critical, highly effective technique for improving software reliability. However, it requires engineers to come up with tests that exercise all the tricky corner cases of a system. This requirement makes testing highly concurrent, fault-tolerant programs like distributed systems very difficult: messages can be dropped, duplicated, or delivered out of order and nodes in the system may crash and/or reboot at any time. In this paper, Newcombe et al. describe how using the TLA+ model checker helped design correct, efficient distributed within the Amazon Web Services group. Additionally, they discuss the important social aspects of convincing already-oversubscribed colleagues to adopt a formal methods approach.
[OPTIONAL] If you liked this paper, you may also be interested in:
Formal Reasoning about the Security of Amazon Web Services - Byron Cook - 2018
In this talk, Byron highlights some of the ways he's helped lead broader adoption of formal methods across Amazon.
In related article in IEEE Software (2019), Byron and others promote the rise of "one click formal methods".
Formal Methods at Facebook
Debugging Designs using Exhaustively Testable Pseudo-code - Chris Newcombe - 2011
This talk transcript gives a bit more background on the work, in particular the back story on engineers working "nights and weekends on personal time" to learn TLA+.
The Evolution of Testing Methodology at AWS: From Status Quo to Formal Methods with TLA+ - Tim Rath - 2015
This talk gives a great overview of some popular testing techniques and the path to formal methods using TLA+ in AWS.
Reading 4 : BP: Formal Proofs, the Fine Print, and Side Effects
Paper: BP: Formal Proofs, the Fine Print, and Side Effects - Murray, Oorschot - 2018
Reflection Due: May 14 by 5pm PT
When we try to formally verify systems, we often slightly (or significantly) tweak them in order to facilitate proving their correctness. But what does that really mean? Did we still truly "verify the system" if we had to change it to get a proof to go through? Are there different kinds of changes that have different consequences? In this thought-provoking paper, Murray and Oorschot raise such big questions and explore some of the consequences of their potential answers.
[OPTIONAL] If you liked this paper, you may also be interested in:
Techniques for Program Verification - Greg Nelson - 1981
In the first two sections of Chapter 1 from his PhD thesis, Greg Nelson discusses software verification broadly and specifically focuses on how users should interpret the results when their prover says "Verified"; his conclusion is that we should change these messages to "Sorry, can't find any more errors!" đŸ˜„
Nelson's thesis also formed the basis for all modern SMT solvers used in automated theorem proving and synthesis. His work on the Denali system also laid the foundation for equality saturation, which has lead to recent breakthroughs in tools like egg.
Reading 5 : Finding and Understanding Bugs in C Compilers
Paper: Finding and Understanding Bugs in C Compilers - Yang, Chen, Eide, Regehr - 2011
Reflection Due: May 28 by 5pm PT
We often reason about programs at the "source level", but of course machines do not directly run programs in higher-level languages. Instead we trust the compiler to correctly translate our programs down to assembly. But are mainstream compilers correct? How could we empirically evaluate compiler correctness? In this groundbreaking paper, Yan et al. demonstrate how differential fuzzing can be applied to uncover thousands of bugs in mainstream C compilers. They even test CompCert C compiler which is formally verified in Coq... the results may surprise you!
[OPTIONAL] If you liked this paper, you may also be interested in:
Subtleties of the ANSI/ISO C Standard - Krebbers, Wiedijk - 2012
Who cares about undefined behavior in C? It's trickier than you might expect!
Formal Verification of a Realistic Compiler - Xavier Leroy - 2009
This paper describe the formally verified (in Coq!) CompCert C Compiler which was a MASSIVE breakthrough in applying proof assistants for verifying "real systems". This lead to massive research efforts like the DeepSpec project (CACM article).
A Minimalistic Verified Bootstrapped Compiler - Magnus O. Myreen - 2021
A very nice recent paper on formally bootstrapping formally verified compilers. Ties back to our very first reading on "Trusting Trust"!
Compiler Validation via Equivalence Modulo Inputs - Vu Le, Mehrdad Afshari, Zhendong Su - 2014
This paper advances the techniques pioneered by Csmith to find even more bugs in mainstream C compilers.
Valdiating SMT Solvers via Semantic Fusion - Domini Winterer, Chengyu Zhang, Zhendong Su - 2020
This paper shows techniques for finding bugs in SMT solvers (used in automated theorem proving)
