Software Specification: Separation Logic
Software Specification, MEIC @ IST, 2020/21
@jff https://joaoff.comDynamic memory
- Reasoning about programs that manipulate dynamic memory is challenging
- There have been several formalisms proposed
- A very successful proposal is separation logic, an extension of Hoare Logic
Frame Rule
The so-called frame rule $$\ione{Frame}{\ht{F \wedge P}{C}{F \wedge Q}}{\ht{P}{C}{Q}}$$ is known to fail in standard Hoare Logic. Example: $$\ione{Frame}{\ht{y=0 \wedge x=0}{x := 2}{y=0 \wedge x=2}}{\ht{x=0}{x:=2}{x=2}}$$ Not valid because $y$ could alias $x$ (i.e. point to the same memory cell)
Separation Logic
- Separation logic is an extension of Hoare logic, which employs novel logical operators, most importantly the separating conjunction $\ast$ (pronounced "and separately") when writing assertions.
- It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang drawing upon early work by Rod Burstall.
Frame Rule
The so-called frame rule $$\ione{Frame}{\ht{F \ast P}{C}{F \ast Q}}{\ht{P}{C}{Q}}$$ is valid in Separation Logic, provided that C does not modify variables mentioned in the "frame" F. $$\ione{Frame}{\ht{y{\mapsto}0 \ast x{\mapsto}0}{[x] := 2}{y{\mapsto}0 \ast x{\mapsto}2}}{\ht{x{\mapsto}0}{[x] := 2}{x{\mapsto}2}}$$ Valid because $y$ cannot alias $x$ (i.e. they point to different memory cells)
Frame Rule
The frame rule is the key to the principle of local reasoning in separation logic: reasoning and specifications should concentrate on the resources that a program accesses (the footprint), without mentioning what doesn’t change.Separation Logic
Learning material:
- Peter O'Hearn. 2019. Separation logic. Commun. ACM 62, 2 (January 2019), 86-95. [Recommended]
- Peter O'Hearn, Lecture 1: Basics, Fluency [Essential]
- Peter O'Hearn, Lecture 2: Foundations [Essential: Proof Rules for Programs]
- Peter O'Hearn, Lecture 3: Cooking a Program Analyzer
- Peter O'Hearn, Lecture 4: A New Recipe from East London
- An Introduction to Separation Logic, John C. Reynolds
Programming Language
The programming language is extended with new commands for the manipulation of mutable shared data structures:
States
Semantics (by example)
Semantics (by example)
Assertions
Assertions
Simple sharing patterns
Simple sharing patterns
Partial Correctness
Frame Rule
Inference rules
Inference rules
Inference rules
Inference rules
Example
Example
Example
Example
Example
Example
Example (Lists)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
Example (List Reversal)
FreeRTOS: Scheduling Tasks
FreeRTOS: Scheduling Tasks
The verification system used was HIP/Sleek, which supports sets, bags, etc.
FreeRTOS: Scheduling Tasks
For small case studies such as FreeRTOS, it is possible to annotate the code with contracts. However, manual annotation is not scalable!
Verifast
Based on separation logic. Uses symbolic execution.
Case Study: Belgian e-ID card
Case Study: Belgian e-ID card
Case Study: Belgian e-ID card
Case Study: Linux network management software
Case Study: Linux network management software
Case Study: Linux network management software
(2017, uses Verifast)
Verified NAT
Scalable verification
- One of the main obstacles blocking application of verification tools to programs in the millions of LOC is the need for the human to supply annotations.
- Bi-abduction is a technique that can be used to infer pre- and postconditions
- Bi-abduction: given A and B, find $\text{?frame}$ and $\text{?anti-frame}$ such that $$A \ast \text{?anti-frame} \vdash B * \text{?frame}$$ where $\vdash$ is read 'entails' or 'implies.'
- See Peter O'Hearn's Lecture 4 for more details.
Monoidics founded in 2009 and acquired in 2013 by Facebook
FB Infer
In deployment at Facebook where it catches thousands of bugs per month before code reaches production in products used daily by over one billion people.
FB Infer
- The compositional nature of Infer turned out to be a remarkable fit for Facebook's software development process: a codebase with millions of lines is altered thousands of times per day in "code diffs" submitted by the programmers.
- Instead of doing a whole-program analysis for each diff, Infer analyzes changes (the diffs) compositionally, and reports regressions as a bot participating in the internal code review process.
- Using bi-abduction, the frame rule picks off (an approximation of) just enough state to analyze a diff, instead of considering the entire global program state.
Separation Logic: Insights
- Separation logic supports in-place updating of facts as we reason, in a way that mirrors in-place update of memory during execution, and this leads to logical proofs about imperative programs that match computational intuition
- Separation logic supports scalable reasoning by using an inference rule (the frame rule) that allows a proof to be localized to the resources that a program component accesses (its footprint).
- Concurrent separation logic shows that modular reasoning about threads that share storage and other resources is possible
Dissertation Topics
If you are interested in working on projects around software reliability, feel free to get in touch!
Topics include: verification, automated bug finding, program synthesis, quantum software engineering, smart contracts and blockchain, software security, ...