Jean Yang on An Axiomatic Basis for Computer Programming

Our lives now run on software. Bugs are becoming not just annoyances for software developers, but sources of potentially catastrophic failures. A careless programmer mistake could leak our social security numbers or crash our cars. While testing provides some assurance, it is difficult to test all possibilities in complex systems--and practically impossible in concurrent systems. For the critical systems in our lives, we should demand mathematical guarantees that the software behaves the way the programmer expected.

A single paper influenced much of the work towards providing these mathematical guarantees. C.A.R. Hoare’s seminal 1969 paper “An Axiomatic Basis for Computer Programming” introduces a method of reasoning about program correctness now known as Hoare logic. In this paper, Hoare provides a technique that 1) allows programmers to express program properties and 2) allows these properties to be automatically checked. These ideas have influenced decades of research in automated reasoning about software correctness.

In this talk, I will describe the main ideas in Hoare logic, as well as the impact of these ideas. I will talk about my personal experience using Hoare logic to verify memory guarantees in an operating system. I will also discuss takeaway lessons for working programmers.

Transcript

1. An Axiomatic Basis for Computer Programming Jean Yang Papers We Love #10 / 11.18.14
2. An Axiomatic Basis for Computer Programming Jean Yang Ph.D. student, MIT CSAIL November 18, 2014
7. Good thing there is such a thing as inspection!
8. But How Do We Measure Software?
9. Testing I looked in the mirror five times. I confirmed that I look good. I am Ryan Gosling. I am wearing a suit. Ryan Gosling looks good in a suit. Q.E.D. Logical reasoning vs.
10. Axioms. The set of facts we have to work with. Ingredients Theorems. Built from our axioms based on deduction rules.
11. Deductive Logic: Detachment → Am Ryan Gosling → Look good Am Ryan Gosling Look good
12. → → Am Ryan Gosling → Great hair Great hair → Look good Am Ryan Gosling Look good Deductive Logic: Syllogism
13. Deductive Logic: Contrapositive → ¬ ¬ Am Ryan Gosling → Look good Do not look good Am not Ryan Gosling
14. But How to Apply to Programs?
15. Previous Work: Characterizing Program State = 3 > ( ≠ 0) ⇒ ( + = ) = ∈1… [] ∀ ∈ 1 … . > [ − 1] Slide borrowed from Jonathan Aldrich, who borrowed slides from Rustan Leino.
16. Characterizing Programs Using the Hoare Triple Precondition Program Postcondition
17. Example Hoare Triples ∶= 5 = 5 = { ∶= + 3} = + 3 > 0 { ∶= ∗ 2} > −2 = < 0 ℎ ∶= − = || { ∶= 3} = 8 {ℎ ≔ + 1} … Looks good Any program Looks good
18. Example: Assignment ? ≔ + 1 ≤ Assignment axiom schema 0 ≔ where is a variable identifier; is an expression; 0 is obtained from by substituting for all occurrences of .
19. Example: Assignment + 1 ≤ ≔ + 1 ≤ 0 ≔ where is a variable identifier; is an expression; 0 is obtained from by substituting for all occurrences of . Assignment axiom schema
20. Bringing This Back to Ryan Gosling + = ≔ + = ?
21. 1 1 1 2 1 ; 2 Composition > 1 ≔ + 1 > 2 > 2 ≔ + 1 > 3 > 1 ≔ + 1; ≔ + 1 > 3 > 1 ≔ + 1 > 2 > 0 ≔ − < 0 > 1 ≔ + 1; ≔ − ?
22. → → Consequence > 1 ≔ + 1 > 2 > 2 → > 0 > 0 ≔ − < 0 > 1 ≔ + 1; ≔ − < 0
23. Consequence with RG + = ≔ + = = ≔ + = = → + = →
24. Iteration ∧ conjunction ¬ negation ∧ < 10 ≔ + 1 < 10 ≔ + 1 ≥ 10 ∧ > 0 ∧ < 10 ≔ + 1 > 0 > 0 < 10 ≔ + 1 ≥ 10 ∧ > 0 ∧ ¬ ∧
26. Automated Tools Based on Hoare Logic
27. Verified Type-checked Verve, a Type-Safe OS Safe to the Last Instruction / Jean Yang • Verify partial correctness of low- level Nucleus using Hoare logic based on a hardware spec. • Verify an interface to typed assembly for end-to-end safety. Nucleus File System Drivers Applications Microkernel Hardware specification Interface specification 27 [Yang and Hawblitzel, PLDI 2010]
29. “Load” Specification procedure Load(ptr:int) returns (val:int); requires memAddr(ptr); requires Aligned(ptr); modifies Eip; ensures word(val); ensures val == Mem[ptr]; Safe to the Last Instruction / Jean Yang 29
30. Boogie to x86 implementation ReadKeyboard(){ call KeyboardStatusIn8(); call eax := And(eax, 1); if (eax != 0) { goto proc; } call eax := mov(256); return; proc: call KeyboardDataIn8(); call eax := And(eax, 255); return; } Safe to the Last Instruction / Jean Yang ReadKeyboard proc in al, 064h and eax, 1 cmp eax, 0 jne ReadKeyboard$proc mov eax, 256 ret ReadKeyboard$skip: in al, 060h and eax, 255 ret 30
31. The Verve Nucleus Safe to the Last Instruction / Jean Yang 31 Verified Type-checked Nucleus File System Driver s Applications Microkernel Hardware specification Interface specification Verified Interface specification x86 instructions Memory bounds Devices GC Heap Allocator and GC [POPL 2009] Stacks Interrupt table Interrupt/error handling Interface specification
32. Ideas to Take Home
33. Always think about correctness.
34. Choose a language that helps you reason.
35. Read Papers You Love!
36. Play with Research Tools Coq
37. M-MAYBE IT BECAME ILL AND COULDN’T PRINT AN OUTPUT ! Be Patient with Research
38. Pop Quiz! • What main issues did this paper address? • Why do we want to prove programs correct? • What were Hoare’s contributions to software verification? • What should we be doing when we leave here?
39. Hoare Logic, Since 1969 1. Define a way to characterize programs and properties. 2. Build tools to automatically check program properties. 3. Profit.