Transcript Slides - Purdue College of Engineering

NATURAL PROOFS FOR
STRUCTURE, DATA,
AND SEPARATION
XIAOKANG QIU
ANDREI STEFANESCU
PRANAV GARG
P. MADHUSUDAN
UNIVERSITY OF ILLINOIS AT URBANA-CHAMPAIGN
PLDI 2013, SEATTLE, WA
MOTIVATION
Don’t know
Automatic Deductive Software Verification
int f(int x){
assume x>0;
…
inv x < y;
…
assert y>0;
}
VC-Generator
no
"x, y.(x > 0 Ù...
Þ y > 0)
Verification Condition
yes
SMT Solver
Annotated Program
Success stories: Hypervisor (MSR), ExpressOS (Illinois), etc.
using tools like Boogie, VCC, etc.
Challenge: dynamically modified heap
• Structure (e.g., “p points to the root of a tree”)
• Data (e.g., “the integers stored in a list is sorted”)
• Separation (e.g., “the procedure modifies only elements
reachable using the next field”)
EXAMPLE: MEMORY ISOLATION
PID: 12
PID: 30
PID: 19
Start Addr
Start Addr
Start Addr
End Addr
End Addr
End Addr
Prev Next
Prev Next
Prev Next
Verify invariants in ExpressOS [@UIUC, ASPLOS’13]
- “Every two assigned memory chunks are disjoint“
- “The start addresses are sorted along the doubly-linked list”
- “The memory allocator modifies only this doubly-linked list”
Structure, Data,
and Separation
are mixed
Key Challenge:
Expressive logics
to specify complex
data structures
UNDECIDABLE
Automated reasoning
with these
sophisticated logics
HEAP VERIFICATION
Expressive
Expressive
Logics:
Separation logics,
HOL, Matching
logic, etc.
keep
expressiveness
Natural
Proofs
give up decidability
sound but incomplete
preserve automaticity
Decidable Logics:
Strand, LISBQ,
CSL, etc.
Automatic
NATURAL PROOFS: IN A NUTSHELL
• Handle a logic that is very expressive
(inevitably undecidable)
• Retain automaticity at the same level as
decidable logics
• Identify a class of natural proofs N such that
• N includes natural proof tactics used in
human proofs
• Many correct programs can be proved using
a proof in class N
• The class N is effectively searchable
(checking if there is a proof in N is efficiently
decidable)
All Proofs
N
MORE GENERAL
NATURAL PROOFS
• Natural Proofs for Trees [POPL’12]
• only for trees (can’t say “x points to a tree and y points into the
tree”)
• only functional recursion (no while-loops, too weak for loop
invariants)
• only classical logic (no frame reasoning)
• In this work: Natural Proofs for Separation Logic
• A wide variety of structures, and their combination (trees,
doubly-linked lists, cyclic lists, etc.)
• Iterative and Recursive (pre, post, and loop-inv.)
• Separation Logic (frame reasoning is natively supported)
CONTRIBUTION
• Dryad: a dialect of separation logic that is amenable to natural
proofs
- No explicit quantification, but supports recursive definitions
- Admits a translation to quantifier-free classic logic with recursion
• Automatic VC-generation for Dryad-annotated programs
• Develop natural proofs using decision procedures (powered by
SMT solvers)
Two proof tactics for handling recursive defs [Suter et al., 2010] :
- Unfold across the footprint
- Formula abstraction
These two tactics form the class of natural proofs!
BINARY SEARCH
TREE
IN
DRYAD
Base case:
right subtree:
left subtree:
emptya BST
the
a BST
heaplet
root
def
bst(x) = (x = nilÙ emp) Ú
the union of the
keys stored in the
left,right,key
*
(x
l, r, k) *Base
bst case:
(l)Ù keys(l) £root
k *and
( bst(r)Ù
the k < keys(r))
empty set
left/right subdef
keys(x) = (x = nil: Æ ;
trees
root
left,right,key
(
)
(x
l, r, k)* true:
{k}È keys(l)È keys(r) ;
default:
Æ ) predicate
Recursive
Recursive
function
yinv º bst(root) Ù (bst(curr)* true)
Separating
Conjunction
Ù (k Î keys(root) « k Î keys(curr)* true)
(loop invariant for “bst-search”:
curr
root points to a BST and curr points into the BST;
k is stored in the BST iff k is stored under curr)
k
WHY DRYAD?
The heaplet semantics is not supported by automatic theorem
provers
Solution:
x
next
y
translated to
next(x) = yÙG = { x}
Capture the scope (heaplet required) of a formula using setvariables?
• Empty heap emp :
• Singleton heap x
y
:
• Separating Conj. t * t’ :
Æ
{x}
scope(t)Èscope(t¢)
• Recursive definition Pl,r* (x) : reach
? l,r(x)
*
Dryad:
the Logic:
scope isThe
exactly
the reachable
locations
fromfix
x using
l and
Separation
semantics
of P (x)
is arbitrary
point of
ther
(only
difference
between
Dryad
and classic
Logic)
recursive
definition,
and
the scope
is notSeparation
syntactically
determined
TRANSLATING
HEAPLETS TO SETS
• The heaplet required for a Dryad formula can be syntactically
determined
• the scope can be modeled as a set of locations, and the heaplet
semantics can be expressed using free set variables
def
Example: treeleft,right (x) = x
left,right
(l, r) * tree(l) * tree(r)
def
translated to
tree _ global(x, G) = left(x) = l Ù right(x) = r Ù
(still quantifier-free)
tree _ global(l) Ù tree _ global(r) Ù
reach left,right (l)Ç reach left,right (r) = Æ Ù
x Ï reach left,right (l)È reach left,right (r)
{x}È reach left,right (l)È reach left,right (r) = G
def
reachleft,right (x) = ITE ( x = nil, Æ, {x} È reachleft,right (l) È reachleft,right (r))
NATURAL PROOFS FOR DRYAD
We consider programs with modular annotations
• A simple heap-manipulating language
(supports memory allocation/deallocation, destructive pointer/data
updates, and function calls)
• Pre/post-conditions and loop invariants written in Dryad
• Footprint: dereferenced locations (x is in footprint if y := x.next
)
Natural Proofs:
Verify programs
in 4 steps
Two proof
tactics
1. Translateinspired
Dryad to
by classic logic with recursion
human proofs
2. VC-Generation (compute strongest-post)
3. Unfold recursive defs across the footprint (still precise; explained
later)
4. Formula Abstraction
(recursive definitions uninterpreted, becomes sound but incomplete)
1ST PROOF TACTIC:
UNFOLDING ACROSS THE FOOTPRINT
The verification condition ψVC involves recursive definitions that can be
unfolded ad infinitum.
æ (u = nilÙreach(u) = Æ) Ú
ö
ç
÷
æ (u = nilÙ reach(u) = Æ) Úö
(ul
=
nilÙreach(ul)
=
Æ)
Ú
(tree(ull)Ùtree(ulr)...
)
ç
÷ « ...
tree(u) « ç
÷«ç
(ur = nilÙ reach(ur) = Æ) Ú (tree(url)Ùtree(urr)... )÷
è (tree(ul)Ùtree(ur)Ù... ) ø
ç
÷
èÙ...
ø
Where to stop?
• In most cases: unfold only across the footprint (locations get
dereferenced in the program).
…
y = x.l;
z = x.r;
z.l = y;
…
Footprint: {x, z}, then assert
tree(x) = …
tree(z) = …
Non-footprint: {y}, then assert
tree(y) /\ NoMod(y) ==> tree’(y)
1ST PROOF TACTIC:
UNFOLDING ACROSS THE FOOTPRINT
Unfold only
Formally, we capture this proof tactic using a set across
ofApply
conjuncts:
the
the
frame
rule for
footprint
non-footprint
locations
Theorem
• ψVC is valid iff ψ’VC is valid.
2ND PROOF TACTIC:
FORMULA ABSTRACTION
Natural Proofs in two steps:
unfold
¢
yVC Þ yVC
formula
abstraction
abs
Þ y VC
Formula Abstraction
• replace each recursive definition rec with uninterpreted U
abs
• when a proof for yVC is found, we call it a natural proof for yVC
(sound but incomplete)
abs
yVC
is expressible in the decidable theories
(theory of sets/arrays, maps, uninterpreted functions and integers)
and is solvable using modern SMT solvers.
USER-PROVIDED AXIOMS
Proof tactics cannot effectively find the relationship between data
structures
Meta-level axioms for structures (independent of program verified)
• Relating simpler data structures and more sophisticated ones, e.g.,
"x. bst(x) Þ tree(x)
• Relating partial data structures and complete ones, e.g.,
"x, y. lseg(x, y) * list(y) Þ list(x)
Instantiated at all non-footprint locations
Still automatic?
• Axioms are program-independent, defined once and for all
• Can be encoded in the verifier
NATURAL PROOFS FOR DRYAD
Program
+
Recursive
defs
+
Annotations
in
Dryad
Translate
Program
+
Recursive
defs
+
annptations
in
Classicallogic
VCGen
no
Encode
Don’t know
yes
SMT Solver
Formula in a
dec. logic
over sets:
Does a
natural proof
exist?
Verification
Conditions
N
Two proof
tactics for
recursive
defs
EXPERIMENTAL EVALUATION
A prototype verifier with Z3 as the backend solver
(more details at http://web.engr.illinois.edu/~qiu2/dryad/)
Inductive data structures
singly-linked list, sorted list, doubly-linked list, cyclic list, maxheap, BST, Treap, AVL tree, red-black tree, binomial heap, …
Data structures from open source programs
• Glib library: singly/doubly-linked list
• OpenBSD library: queue
• Linux kernel: VMA for virtual memory management
ExpressOS: a secure mobile platform
• Structures for memory management
WE VERIFIED …
106 Dryad-annotated programs
•
•
•
•
•
insert, delete, search, reverse, rotate, … (recursive & iterative)
Quicksort, Schorr-Waite algorithm for trees, etc.
VMA: virtual memory operations
ExpressOS: operations memory isolation
full-functional, partial correctness (e.g., data structure invariants,
expected set-of-keys, …)
All the VCs were automatically proved by our tool！
• 69 verified within 1 sec
• 96 verified within 10 sec
• 104 verified within 100 sec
“RBT-delete_iter” spent 225 secs, “binomial-heap-merge_rec” spent 153 secs
(To the best of our knowledge)
First terminating automatic mechanism that can prove such a wide
variety of data-structure manipulating programs full-functionally correct
RELATED WORK
Natural proofs
• [Suter et al., POPL’10]: Proof tactics for functional programs
• [Madhusudan et al., POPL’12]: Imperative programs, only trees,
no while-loops, no frame reasoning
Separation Logic
• Verifast, Bedrock, etc.: proof tactics provided by the user per
program
• Implicit Dynamic Frames: also using sets for heaplet, not
syntactically determined, not quantifier-free
• HIP/Sleek: search for a class of proofs, but not in any decidable
theory
Classical Logic
• Dafny, VCC, etc.: require significant ghost annotations
• Jahob: often relies on complex provers, e.g., Mona or Isabelle
CONCLUSION
Dryad
•
•
an expressive, tractable dialect of separation logic
A translation to QF classical logic with recursion
Established a natural proof scheme
•
•
•
Algorithmically search for a subclass of proofs
Automatic, sound but incomplete
Formalized two proof tactics for inductive data structures
All Proofs
Natural
proofs
A verifier that handles Hoare-triples automatically using SMT solvers
Future work
•
More proof tactics for natural proofs
(non-inductive structures, e.g., graphs)
•
Natural Proofs for C
(incorporate natural proofs into existing verifiers, e.g., VCC)
•
Natural Proofs for concurrent programs (Rely-Guarantee + Dryad)