Transcript Formal methods, Trusting trust attack, and

SWE 681 / ISA 681
Secure Software Design &
Programming
Lecture 10: Miscellaneous –
Formal Methods,
Trusting Trust Attack/ DDC
Dr. David A. Wheeler
2015-03-29
Outline
• Formal methods
• Open proofs
• Malicious tools / trusting trust attack
– Countering using diverse double-compiling (DDC)
• Vulnerability disclosure
Some portions © Institute for Defense Analyses
(the OSS and open proofs sections), used by permission.
This material is not intended to endorse particular suppliers
or products.
2
Formal methods (FM)
3
Formal methods (FM)
• Introduction
• Notations
• Tools
– Specifications
– Verification (general & for proving programs)
4
Formal methods (FM)
• Formal methods (FM) = the use of
“mathematically rigorous techniques and tools
for the specification, design and verification of
software and hardware systems.”
– Can be applied to spec, actual software, or model
• Mathematically rigorous = “specifications are
well-formed statements in a mathematical logic
and that the formal verifications [if any] are
rigorous deductions in that logic”
Source: “What is Formal Methods?” by Ricky W. Butler
http://shemesh.larc.nasa.gov/fm/fm-what.html
5
Why formal methods (FM)?
• Imagine it’s critical that software meet some
requirement
– E.G., “Never give secret information to unauthorized
personnel”
– So important that it’s a disaster if requirement not met
• FM spec language can reduce requirement ambiguity
• You cannot get truly high confidence with just:
– Dynamic analysis (e.g., testing) – only tiny % of inputs
– Vulnerability scanners – only reports some defects
• In contrast, FM can prove “always” or “never” (!!!)
– Given some assumptions (& you decide what those will be)
6
Applying formal methods to
security issues
• To apply FM in general:
– Describe requirements using FM-based spec language
– If will verify, choose & apply FM verification approach(es)
• Thus, to directly apply FM to security:
– Must describe security requirements using FM-based spec
language (and verify if applicable)
– Verification tool may predefine requirement (“no race
condition”) - simplifies use, but limits usage & claim
– Verification must usually prove no undefined situation
occurs, which by itself can reveal potential issues
• Some FM technologies can be “repurposed”
7
The idea of using logic to
determine truth is an old one!
“The only way to rectify our reasonings is to
make them as tangible as those of the
Mathematicians, so... when there are disputes...
we can simply say: Let us calculate... to see who
is right.”
– Gottfried Leibniz, The Art of Discovery (1685)
• Already achieved in certain areas
• Limitations exist, both in theory & practice
• A little history will help…
8
Advances in logic & formalized
(mathematical) reasoning
•
•
•
•
•
•
Artistotle’s Organon, esp. “Analytica Priora” (Prior Analytics) – first work on logic
Euclid’s Elements — oldest extant axiomatic deductive treatment of mathematics
Non-Euclidean geometry (Lobachevsky 1829, János Bolyai 1831, Gauss)
George Boole’s “An Investigation of the Laws of Thought…” (1854) — founded
boolean algebraic logic (much work since)
Gottlob Frege’s Begriffsschrift… (1879) — added more-general mechanisms to
handle functions & “quantified” variables (all & there-exists)
Bertrand Russell discovers “Russell’s paradox” in 1901 (mailed to Frege 1902)
– Shows that naïve set theory leads to paradox, must fix somehow
– Let R be the set of all sets that are not members of themselves… is R a member of itself?
•
Whitehead & Russell release Principia Mathematica (1910-1913)
– Goal: Describe axioms & inference rules from which all mathematical truths could in
principle be proven (“logicism” school: Base all math on logic)
– Notation shift since (see Linsky’s “The Notation in Principia Mathematica”)
– Russell’s paradox solution (a hierarchy of types) unwieldy; today most fundamental
math work based on Zermelo–Fraenkel set theory, often with the axiom of choice (ZFC)
•
Intuitionism/Constructivism (Brouwer & Heyting) & Formalism (Hilbert*)
* Hilbert was not a strict formalist,
as he & many other formalists believed
there was meaning and truth in mathematics
The “foundational crisis of mathematics” - the early 20th century search
for the proper foundations of mathematics – is dramatized in Logicomix:
An Epic Search for Truth by Apostolos Doxiadis & Christos Papadimitriou
9
Most of modern mathematics is built on a
small set of rules of reasoning & axioms
Mathematicians identify
rules of reasoning, axioms
(assumptions), and derive
proofs using them
Theories about numbers can
be derived from lower-level axioms,
then used as building blocks*
Second/higher-order
predicate logic
(variables can be functions)†
Axiom of Choice (AC) †
(some controversy!)
First-order predicate logic
(variables can be objects)
Zermelo-Fraenkel (ZF)
Classical propositional logic
(variables are true or false)
Zermelo
Logic
•
•
•
Numbers
Set Theory
* Like physics,
mathematics has been
“reverse engineering”
math concepts into
more elemental
components; numbers
turn out to be derivative
ZFC
(most math
uses this as
its basis)
†
Less commonly used
The division between “logic” & “set theory” isn’t as strict as implied by this figure
Other axioms are sometimes added, e.g., Tarski's axiom, continuum hypothesis (CH)
10
Different logics & axioms are in use, e.g., intuitionism subsets classical logic & rejects AC
Gödel’s incompleteness theorems
•
David Hilbert’s retirement address at 1930 Königsberg conference concluded with:
– “For the mathematician there is no Ignorabimus… in my opinion… there is no unsolvable
problem. In contrast to the foolish Ignoramibus, our credo avers: We must know. We shall
know!” (“Wir müssen wissen. Wir werden wissen!”)
•
Gödel’s incompleteness theorems proved this is impossible:
– Two theorems proven & published by Kurt Gödel in 1931*
– First one was announced by Gödel at the same 1930 conference!
– Establishes fundamental limitations of mathematics
•
First incompleteness theorem:
– No consistent system of axioms whose theorems can be listed by an “effective procedure”
(e.g., computer program or algorithm) can prove all truths about the relations of the natural
numbers (arithmetic)
– I.E.: There will always be statements about the natural numbers that are true but unprovable
within a consisten system
•
Second incompleteness theorem:
– Such a system cannot demonstrate its own consistency
•
Note: Gödel proved a different “completeness theorem” in 1929 (as dissertation)
– In first-order logic (limited), all logically valid formulas can be formally proved in finite steps
– Not the same thing!
* In “On Formally Undecidable Propositions in
Principia Mathematica and Related Systems I”
(second part never written) as Theorems VI and XI 11
Halting Problem
• Halting problem: Given a description of an
arbitrary computer program, decide whether the
program finishes running or continues to run
forever (for some input)
– Alan Turing proved in 1936 that a general algorithm to
solve the halting problem for all possible programinput pairs cannot exist
– Proof similar to Gödel’s incompleteness theorems
– Fundamental limit on computation
But within these theoretical limits,
a lot can be accomplished.
12
This is only a partial summary of
formal methods
• This is a summary; many important things omitted
– Have been decades of research (more than we can cover)
– Active research area (so expect changes/new approaches!)
• Presentation goal: awareness of key portions of field
– Omit details on how they work, but some info necessary to
understand their capabilities & limitations
– Too many know little, & some courses only explain 1 tool
– Assume you know already how to develop software
• Especially note open source software & no-cost tools
– Identify things you can try & experiment with right now
• If you’re interested, whole classes & careers in this field
– Need math, especially discrete math & logic
13
Making formal methods affordable
• Formal methods costly to apply today in many cases
• Many backoff approaches exist to limit costs:
– Level 0: Formal specification created, then program informally
developed from it. “Formal methods lite”
– Level 1: Level 0, + prove some select properties or formal refinement
from specification towards program
– Level 2: Fully prove claims, mechanically checked
– Any of the above can apply to a subset of components or properties
• E.G., specialized analysis tool to determine one specific (important) property.
Narrow properties can be relatively affordable on big systems
• Tool support typically needed to scale up
– Different tools good for different things (combining may help)
– Choose specific toolsuite that meets goal, e.g., use weakest language
• Improvements: Increasing CPU power, improved algorithms, & OSS
(speeding research, distribution, and multi-approach integration)
• We’ll discuss basics of FM notations, then tools/approaches
14
Formal methods: Notations
15
Quick review: Set notation
• Set: a collection of elements or members
–
–
–
–
–
–
–
Given sets S = {1, 2, 3} ; T = {1, 2}; R = {1, 5}; L = {a, b}
Is member of: 1  S is true, 7  S is false, 7  S is true
Is subset of: T  S is true, R  S is false
Union: S  R is {1,2,3,5}
Intersection: S ∩ R is {1}
Set difference: S \ R = S – R = {2,3}
Cartesian Product: R x L = {(1,a),(1,b),(5,a),(5,b)}
• Common predefined sets (sometimes with blackboard bold):
–
–
–
–
–
–
∅ or {}: Empty set
N: natural numbers {1, 2, 3, …} or {0, 1, 2, …}; ISO 31-11 includes 0
Z: integers (from Zahl, German for integer) {…, -2, -1, 0, 1, 2, …}
Q: rational numbers (from quotient)
R: real numbers
C: complex numbers
Many whose “N” includes 0 may also append “*” superscript to any of the above letters to
mean “except zero” [ISO 31-11; Gullberg, Mathematics: From the Birth of Numbers]
16
Set builder notation
• Sets can be defined using set builder notation. A common format:
{ expression-using-variable | variable  set ∧ condition}
• Can omit “variable  set” if understood (e.g., pre-stated “universe”)
• Pronounciation:
– | is “where” or “such that”
–  is “in” or “member of” (in Z notation, “:” used instead)
– ∧ is “and” (some notations use “&” or “,” instead)
• E.g., set1 = {x | x  A ∧ p(x)}
– “set1 is the set of elements in A for which the proposition p(x) is true”
• List comprehensions of Python & Haskell are similar
– Python: [(x, y) for x in [1,2,3] for y in [3,1,4] if x != y]
– Haskell: [(k, x) | k <- ks, x <- xs, p x]
17
Many different languages for
mathematical logic
• Various math logic notations (weakest…strongest):
– Predicate logic (just boolean variables)
– First-order logic (FOL) (“all X..”, non-booleans, functions,…)
• Can add “theories” about integers, real numbers, etc. to FOL
– Higher-order logics (HOL) (+ functions can vary/be objects)
• Again, can add “theories” about integers, etc. to HOL
• Stronger logic notations provide more capability
– But tend to be harder to automatically analyze
– Often want “weakest” language that meets needs
• Can add “temporal logic” (“X will happen eventually”)
– Often computation tree logic (CTL) or linear temporal logic (LTL)
• These traditional math notations can be used directly or be
part of a larger specification language
18
Predicate logic
• Predicate logic – define expressions with just:
– Boolean variables
– Operators and, or, not
– Parentheses allowed
• Predicate logic too limited for many problems
– Useful in some cases, e.g., dependency analysis
– Can be used to implement more sophisticated
systems
19
First-order logic (FOL)
• FOL widely used mathematical logic
– Aka “first-order predicate logic” or “first-order predicate calculus”
– Basis of most FM software languages for specs
– Including “higher-order” logics that relax FOL restrictions
– May add “theories” to describe integers, real numbers, etc.
• In traditional FOL, every expression is either a:
– Term (an object / “non-boolean”): a variable, a constant, or a function
f(term1, term2, …)
Typically there’s a “domain of discourse” (aka “universe”), the set of entities over
which variables may range. E.G., “integers” or “real numbers”
– Formula (a truth value / “boolean”): see next slide, includes predicates
(“functions” that return truth value)
• Can have variables & constants (must distinguish)
– Prolog convention: Variable if begin with uppercase, else constant
– Math convention: Variables begin with w, x, y, z
– In FOL, functions & predicates can’t be variables
20
FOL formula notation
Traditional
Notation
Alternate Meaning
Notation
¬A
-A, ~A
Not A. In classical (not intuitionist) logic, ¬¬A = A
A∧B
A&B
A and B. True iff both true
A∨B
A|B
A or B. True iff at least one true
A→B
A -> B
A implies B. Aka “if A then B” (1-arm)
Classically same as ¬A ∨ B
p(T1, T2, …)
Predicate p true when given those terms
T1 = T2
Term is equal to term. Not in traditional FOL but
is a common FOL extension
∀X…
forall X … For all X, … is true
∃X…
exists X … There exists an X where … is true
A and B are formulas; X is a term variable; T1 & T2 are terms; iff = if and only if
21
Conventional FOL example
• ∀ X man(X) → mortal(X)
“For all X, if X is a man, then X is mortal”
I.E., “All men are mortal”
This uses Prolog naming convention (uppercase vars)
• man(socrates)
“Socrates is a man”
• mortal(socrates)
“Socrates is mortal”
This can be proven from the first two statements with
appropriate rules for reasoning
22
More FOL examples
•
–
•
–
•
–
•
–
•
–
•
–
∃ X (bird(X) ∧ ¬fly(X))
“At least one bird can’t fly”
∀ X ∀ Y (mother(X, Y) → younger(Y, X))
“All children are younger than their own mother”
∀ X ∀ Y ((mother(X) ∧ child(Y)) → younger(Y, X))
“All children are younger than all mothers” (FALSE!)
∃ X (brother(X, bob) ∧ likes(alice, X))
“Bob has a brother that Alice likes”
∀ X (brother(X, bob) → likes(alice, X))
“Alice likes all of Bob’s brothers”
∀ X (man(X) → X = socrates)
“All men are Socrates” (FALSE!)
(Most of these examples are based on Huth & Ryan “Logic in Computer Science” 2006)
23
Bugs possible in formal methods
specifications!
• English “and” & “or” often don’t translate exactly
– “Or” may mean inclusive (either-or-both) or exclusive (only-one)
• Common mistake: Empty sets used with forall
– ∀ X martian(X) → green(X)
• Means “All Martians are green”
– ∀ X martian(X) → ¬green(X)
• Means “All Martians are not green”
– If there are no Martians, both expressions are true
• Different from non-expert expectations & Aristotelian logic
• Though there are good reasons for it
– Can easily fix “empty sets” issue once you know about it, e.g.:
• (∃ X martian(X)) ∧ (∀ X martian(X) → green(X))
• Some notations make this easier & less error-prone
• Common mistake: ∃…→… (usually wrong, use ∧ not →)
– ∃ X (a(X) → b(X)) means ∃ X (¬a(X) ∨ b(X)). Instead try ∃ X (a(X) ∧ b(X))
24
Tips on how to create accurate
translations to math notations
• “Translation Tips” by Peter Suber
http://www.earlham.edu/~peters/courses/log/tr
anstip.htm
• “First-Order Logic” by C. R. Dyer
http://pages.cs.wisc.edu/~dyer/cs540/notes/fopc
.html
• “Guide to Axiomatizing Domains in First-Order
Logic” by Ernest Davis
http://cs.nyu.edu/faculty/davise/guide.html
• “Logic in Computer Science” by Michael Huth and
Mark Ryan (Cambridge University Press)
25
FOL extensions
• “Traditional” FOL comes from mathematics
• Many notations in practice add extensions:
– Equality (“=”) is extremely common
– Notation for constant “true” & “false”
– If-then-else: ite(condition, true-term, false-term)
• Traditionally functions can’t accept formulas (booleans)
• Various work-arounds exist, but nicer to have it
– Allow formulas (booleans) as parameters
– F1 ↔ F2, an abbreviation of ((F1 → F2) ∧ (F2 → F1))
• Add types/sorts (integers, reals, etc.)
• Add “Theories” (e.g., about integers, etc.)
– Resulting notations are still first-order
• Ways to structure/organize groups of statements
26
Beyond FOL
• “Second-order” logics & “Higher-order” logics
– Enable functions & predicates to themselves be
variables
• More flexible as a notation…
• But harder to automatically verify
– Support tools tend to be interactive
27
Some approaches for analyzing
programs using logic
• Hoare logic
• Predicate transformer semantics (including
weakest precondition)
• Separation logic
28
Hoare logic (aka Hoare-Floyd logic)
• Created by Sir C.A.R. “Tony” Hoare, based on Floyd
• Hoare triples: {P} C {Q}
– P=precondition, C=Command/code, Q=postcondition
• Examples of rules:
Key:
Premises
Conclusion
P is
“loop invariant”
29
Predicate transformer semantics
(weakest preconditions)
• Dijkstra “Guarded commands, nondeterminacy
and formal derivation of programs”
• Assign every language statement a “predicate
transformer” from one predicate to another
– Weakest-precondition for statement S maps any
postcondition to a (weakest) precondition. Go
backwards
– Strongest-postcondition, map precondition to
postcondition. Go forwards
– Actual transformers based on Hoare logic
– E.G., wp(if E then S1 else S2 end, R) =
(E → wp(S1, R)) ∧ (¬E → wp(S2, R))
30
Separation logic
• Extension of Hoare logic developed by John C. Reynolds, Peter O'Hearn,
Samin Ishtiaq and Hongseok Yang
• Describes “states” consisting of a:
– store (“stack-oriented variables”) and a
– heap (“dynamically-allocated objects”)
• Defines a set of operations about them
• “Frame rule” enables local reasoning
– A program that executes safely in a small state can also execute in any bigger
state and that its execution will not affect the additional part of the state
when certain conditions proved
• E.G., Coq “Ynot” library implements separation logic
• Can apply separation logic concepts using traditional FOL
– E.g., Jessie; see Francois Bobot and Jean-Christophe Filliatre. “Separation
Predicates: a Taste of Separation Logic in First-Order Logic”. 14th International
Conference on Formal Engineering Methods (ICFEM), Nov 2012
31
Beware of math vs. real world
• Mathematical models are not the real world
– They are simplified models of the real world
• Common issue: Math numbers ≠ computer numbers
– In math, infinite number of integers & reals
– Computers always finite; cannot exactly represent all
numbers, and integers/reals often fixed size
• Common issue: Assumptions or goals are wrong
– Wrong assumptions can lead to wrong conclusions
– If you didn’t ask for it, you might not get it
– Testing, inspection, & peer review can help
• Models can be vitally useful
– Be wary of their limitations
32
Formal Methods: Tools
33
Types of formal methods tools
• Formal specification tools
– Without necessarily verifying
• Verification tools
– Major verification approaches include:
•
•
•
•
Theorem-provers: Automated & interactive
Satisfiability (SAT) solvers: Boolean-only or modulo theories
Model-checkers
Abstract interpretation / symbolic execution (for programs)
– First discuss in general (e.g., verifying models)
– Then, how to verify program meets spec (some dups)
• Formalizing & verifying mathematical theorems (not code)
• This is just my grouping & is approximate
• Active research areas, annual competitions
34
Formal specifications of systems
(e.g., for level 0)
• Any FM-based language can be used for specification
– Including PVS, Isabelle/HOL, Coq, ACL2, & many others (we’ll see later)
• Many formal specification languages often used for specification
without (significant) verification
– Language examples: Z, Object-Z (Z+classes), VDM, B, Unified Modeling
Language (UML) Object Constraint Language (OCL), Alloy
• There’s an ISO standard for Z, but “the version described in Mike Spivey’s book
continues to be the most popular” [Jackson]
– Each has various tools to help write specs
– Goal is often to eliminate unintentional ambiguity
• “Alloy” OSS tool is unusual & interesting (Daniel Jackson, MIT)
– Relatively easy & unique spec language
• Parts loosely based on Z, includes “transitive closure” operator
– Includes “checker” to quickly find counter-examples
• Not a prover, but easy-to-use & much more rigorous than just reviewing text
– Could send to theorem prover (Kelloy->KeY, Prioni->Athena/Otter)
35
Z example (birthday book)
Schemas
(state space & operation)
Source: The Z Notation: A Reference Manual, Second Edition
by J. M. Spivey (University of Oxford)
36
Alloy: Sample Screenshot
Source: https://commons.wikimedia.org/wiki/File:Screenshot_of_Alloy_Analyzer.png
37
Alloy: File system example
File System Model (I)
// A file system object in the file system
sig FSObject { parent: lone Dir }
// A directory in the file system
sig Dir extends FSObject { contents: set FSObject }
// A file in the file system
sig File extends FSObject { }
// A directory is the parent of its contents
fact { all d: Dir, o: d.contents | o.parent = d }
// All FSOs are either files or directories
fact { File + Dir = FSObject }
// There exists a root
one sig Root extends Dir { } { no parent }
// File system is connected
fact { FSObject in Root.*contents }
Source: Alloy tutorial,
http://alloy.mit.edu/alloy/tutorials/online/frame-FS-1.html
•
•
// The contents path is acyclic
assert acyclic { no d: Dir | d in d.^contents }
// Now check it for a scope of 5
check acyclic for 5
// File system has one root
assert oneRoot { one d: Dir | no d.parent }
// Now check it for a scope of 5
check oneRoot for 5
// Every fs object is in at most one directory
assert oneLocation { all o: FSObject | lone d:
Dir | o in d.contents }
// Now check it for a scope of 5
check oneLocation for 5
Alloy notation ~subset of Z, not as pretty or rich
– But its special closure operators useful
Can compute & display counter-example(s);
“refuter” not “prover”
38
You’ve already
done this
manually in
high school
Geometry…
Theorem provers
• Theorem prover
– Accepts assumptions (“givens”) & goal in some notation
– Tries to produce proof of goal, starting from assumptions…
– Using only a sequence of allowed inference rules & theorems
• Many different possible inference rules, e.g.:
Modus ponens:
P, P→Q
Q
Modus tollens:
Premises
P→Q, ¬Q
¬P
Conclusion
• Formal proof: Every step fully justified by accepted rule
– “Proof checker” can verify proof - easy to build, enabling
separate third-party verification. Supports “Proof carrying code”
• Theorem proving tools may be either:
– Automated
– Interactive (“proof assistant”)
39
Automated theorem provers
• Automatically prove goal, given assumptions
–
–
–
–
Often like chess programs; try many options & guided by algorithm/heuristics
Many let humans provide guiding “hints”
Many good theorem provers for traditional FOL
Harder to do as add theories or move to a HOL
• Annual CADE ATP System Competition (CASC)
– Uses subsets of TPTP Problem Library
• Example automated theorem provers for traditional FOL with equality:
– Prover9 (William McCune, University of New Mexico) (GPLv2).
– E theorem prover (aka “Eprover”) (Stephan Schulz, TU Munich) (GPLv2)
• Other examples of automated theorem provers:
– Princess: FOL, linear + integer arithmetic (no general multiplication) (GPLv3)
– gappa: Tool to analyze numerical calculation bounds (CeCILL or GPL)
• Uses interval arithmetic and forward error analysis to bound math expressions
• Generates a theorem and its proof for each verified enclosure
– Satallax: HOL (Church's simple type theory+ extensionality + choice) (MIT)
40
Prover9
• Created by William McCune, University of New Mexico
– Descended from “Otter” prover
• Supports FOL with equality, plus list operations
• Approach:
– Starts with assumptions & negated goal
– Transitively generates all facts it can
– If it finds a contradiction, reports that chain as a proof
• Also supports:
– mace4 (tries to find counter-example)
– ivy - proof-checker (checks output—counters tool error)
41
Prover9 example – prove square
root of 2 is irrational
formulas(assumptions).
1*x = x.
x*1 = x.
x*(y*z) = (x*y)*z.
x*y = y*x.
(x*y = x*z) -> y = z.
% Note: Universe = integers > 0, “forall” assumed
% identity
% associativity
% commutativity
% cancellation (0 is not allowed, so x!=0).
% divides(x,y) true iff x divides y. E.G., divides(2,6) is true because 2*3=6.
divides(x,y) <-> (exists z x*z = y).
divides(2,x*y) -> (divides(2,x) | divides(2,y)). % If 2 divides x*y, it divides x or y.
2 != 1. % Original author almost forgot this. Wheeler thinks needing it is a bug.
% Now, assert that we can have a rational fraction for sqrt(2), reduced
% to lowest terms (this will fail, and that's the point of the proof):
a*a = (2*(b*b)).
% a/b = sqrt(2), so a^2 = 2 * b^2.
(x != 1) -> -(divides(x,a) & divides(x,b)).
% a/b is in lowest terms
end_of_list. % Will show proof by contradiction.
Source: “The Seventeen Provers of the World” compiled by Freek Wiedijk. Otter/Ivy section. Original proof created by Larry Wos,
Michael Beeson, and William McCune. Heavily modified/simplified by David A. Wheeler. Note: Prover9 descends from “Otter”
42
Interactive theorem provers
(proof assistants)
• Humans enter symbol-manipulation commands
to derive goals from assumptions
– Tend to support richer notations, e.g., rich theories
and/or HOL and/or…
– But require expert human guidance proof in nontrivial cases
• Sample tools:
– PVS (by S. Owre, N. Shankar, & J. M. Rushby at SRI)
– LCF-style family (HOL 4, HOL Light, Isabelle/HOL)
– Coq (will discuss later)
43
PVS Example #1
mortality: THEORY
BEGIN
man: TYPE+
mortal(m: man): bool
% The "+" means there's at least one man.
% Returns True if m is mortal.
% Socrates is a man.
Socrates: man
% All men are mortal.
all_men_mortal: AXIOM FORALL (m: man): mortal(m)
% Socrates is mortal.
socrates_mortal: CLAIM mortal(Socrates)
In normal PVS use it'd be better
to omit the axiom and say:
mortal(m: man): bool = true
but this tries to stay close
to the traditional example.
END mortality
Prove using: (rewrite "all_men_mortal") or (grind :rewrites ("all_men_mortal"))
44
PVS Example #2
Phone_4 : THEORY
BEGIN
N: TYPE
% names
P: TYPE
% phone numbers
B: TYPE = [N -> setof[P]]
% phone books
VB: TYPE = {b:B | (FORALL (x,y:N): x /= y => disjoint?(b(x), b(y)))}
nm, x: VAR N
pn: VAR P
bk: VAR VB
FindPhone(bk,nm): setof[P] = bk(nm)
UnusedPhoneNum(bk,pn): bool = (FORALL nm: NOT member(pn, FindPhone(bk,nm)))
AddPhone(bk,nm,pn): VB =
IF UnusedPhoneNumb(bk,pn) THEN bk WITH [(nm) := add(pn, bk(nm))]
ELSE bk
ENDIF
…
Source: PhoneBook Example, John Rushby
http://www.csl.sri.com/papers/wift-tutorial/
45
Logic for Computable Functions
(LCF)-Style
• Family of interactive theorem provers
– Based on concepts of LCF (Robin Milner et al 1972), which
used general-purpose programming language ML to allow
users to write theorem-proving tactics
– Library implements an abstract data type of proven
theorems - new objects of this type can only be created
using the functions which correspond to inference rules
– If these functions are correctly implemented, all theorems
proven in the system must be valid
– Large system can be built on top of a small trusted kernel
with “tactics” that automate many tasks
• Includes HOL 4, HOL Light, Isabelle/HOL
– Isabelle/HOL used to prove seL4 operating system kernel
46
Isabelle/HOL proved a microkernel
• “In 2009, the L4.verified project at NICTA produced the first formal
proof of functional correctness of a general-purpose operating
system kernel: the seL4 (secure embedded L4) microkernel.
– The proof is constructed and checked in Isabelle/HOL and comprises
over 200,000 lines of proof script to verify 8,700 lines of C and 600
lines of assembler.
– The verification covers code, design, and implementation, and the
main theorem states that the C code correctly implements the formal
specification of the kernel.
– The proof uncovered 160 bugs in the C code of the seL4 kernel, and
about 150 issues in each of design and specification.”
Source: Gerwin Klein et al, "seL4: Formal verification of an OS kernel".
22nd ACM Symposium on Operating System Principles. October 2009
47
Isabelle/HOL sample
lemma prime-not-square:
p  prime  (k: 0 < k  m * m ≠ p * (k * k))
apply (induct m rule: nat-less-induct)
apply clarify
apply (frule prime-dvd-other-side; assumption)
apply (erule dvdE)
apply (simp add: nat-mult-eq-cancel-disj prime-nonzero)
apply (blast dest: rearrange reduction)
done
Source: “The Seventeen Provers of the World”
compiled by Freek Wiedijk (Isabelle/HOL script version)
(great for comparing some prover notations!)
48
Coq
• Proof assistant for a higher-order logic (HOL), developed in France
• Can define computational function in special language
– Coq’s spec language is called “Gallina”
– Coq can generate OCaml code from it
• Rich type system
– Uses “calculus of inductive constructions” (a HOL)
• Native support for inductive datatypes + “calculus of constructions” (a higher-order typed
lambda calculus by Thierry Coquand from ~1986)
• Based on intuitionist logic (Brouwer et al) – must be able to construct. In intuitionist
logic, “A ∨ ¬A” (law of excluded middle) is not an axiom. Can import “Classical” library
– 5 is an instance of the type “Z” (math integers)
– Specification is a type for a program
• If prove program of that type, then program meets spec
– Defines a large set of “tactics”
• Successes: Java Card EAL7 certified, CompCert C verified compiler
• Gerard P Huet won 2013 ACM Software System Award for Coq
– http://awards.acm.org/award_winners/huet_1246701.cfm
49
Coq example
Lemma foo : ∀n, ble_nat 0 n = true. (* ∀n : naturals, 0 ≤ n *)
Proof.
intros.
destruct n.
(* Leaves two subgoals, which are discharged identically... *)
Case "n=0". simpl. reflexivity.
Case "n=Sn'". simpl. reflexivity.
Qed.
Source: Benjamin C. Pierce et al., “Software Foundations”
http://www.cis.upenn.edu/~bcpierce/sf/Imp.html
50
Boolean satisfiability (SAT) solvers
• Boolean SAT solvers are automated tools that:
– Given predicate logic expressions (boolean variables, and, or, not)…
– Find variable assignments to make true OR report unsatisfiable
• Proven to be an NP-complete problem (first known example)
– Cook, S.A., 1971, “The complexity of theorem proving procedures”,
Proceedings Third Annual ACM Symp. on the Theory of Computing, pp.
151-158
• But multiple algorithm breakthroughs (e.g., Chaff in 2001) now
make SAT solvers remarkably fast for most real problems
– Many good ones free & available as OSS
– Other tools can be built on these or their approaches
• Annual SAT competition; many use DIMACS CNF input format
• Sample tools: Chaff*, MiniSAT, Sat4j, PicoSAT, … (*=not OSS)
The rise of practical SAT solvers is a key technological breakthrough;
many tools have been rewritten to use SAT solvers.
51
DIMACS CNF format for
Boolean SAT Solvers
•
Every propositional formula can be converted to conjunctive normal form (CNF):
– An expression = 1+ clauses connected by “AND”
– A clause = 1+ non-repeated terms connected with “OR”
– A term = A boolean variable, possibly negated
•
DIMACS CNF represents CNF
– Line-oriented, initial c=comment
– First non-comment line is “problem”: p FORMAT #VARIABLES #CLAUSES
– Lines represent clauses with whitespace-separated terms (number=boolean term)
•
•
For example, given this CNF expression:
(x1 | -x5 | x4) &
(-x1 | x5 | x3 | x4) &
(-x3 | x4).
Its DIMACS CNF form could be:
c Here is a comment.
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0
DIMACS=Center for
Discrete Mathematics &
Theoretical Computer Science,
an NSF S&T center
http://dimacs.rutgers.edu/
More info here:
ftp://dimacs.rutgers.edu/pub/
challenge/satisfiability/doc/
52
Satisfiability Modulo Theories
(SMT) solvers
• SMT solvers are also automated tools
– Given expressions in richer notation beyond predicate logic
• Typically FOL + “theories” (variables may be integers, reals, etc.)
• E.g., (x+y ≥ 0) ∧ (y > 0) is satisfiable with integers x=1,y=2
– Reports satisfiable (“sat”) (maybe with satisfying variables) or
“unsat” or “unknown” (e.g., ran out of time/memory)
– To determine if “X is always true”, supply “not X”… returns unsat
– Some can also provide proof (if can’t, how verify results?)
• Internally similar to SAT solvers, may be built on one
• Tools often theory-specific & restrict input language
– Less flexible & more efficient vs. general theorem provers
• Annual competition SMT-COMP, SMT-LIB input format
• Sample tools: CVC4 (successor to CVC3), alt-ergo, STP,
OpenSMT, Z3, Yices* (*=not OSS)
53
SMT-LIB version 2 example (1 of 2)
> (set-logic QF_LIA)
; Basic arithmetic on integers
> (declare-fun x () Int)
; Functions x & y return Int
> (declare-fun y () Int)
> (assert (= (+ x (* 2 y)) 20)); Assert x+2*y = 20
> (assert (= (- x y) 2))
; Assert x-y = 2
> (check-sat)
; Is this satisfiable?
sat
; Yes, it is.
> (get-value (x y))
; What’s an example?
((x 8)(y 6))
; Here’s one of many examples.
Source: David R. Cok, “The SMT-LIB v2 Language and Tools: A Tutorial”.
The “success” replies are omitted. The initial “>” is a prompt.
54
SMT-LIB version 2 example (2 of 2)
> (set-logic QF_UF)
> (declare-fun p () Bool)
> (declare-fun q () Bool)
> (declare-fun r () Bool)
> (assert (=> p q))
; p -> q
> (assert (=> q r))
; q -> r. This means p-> r.
> (assert (not (=> p r)))
; !(p -> r)
> (check-sat)
unsat ; Not possible given the previous assertions
Source: David R. Cok, “The SMT-LIB v2 Language and Tools: A Tutorial”
The “success” replies are omitted. The initial “>” is a prompt.
55
Model-checkers
(aka property checkers)
• Given a system model, exhaustively check if meets a given requirement
– Requirement is often narrow property, often temporal requirement
– System is represented as a finite-state machine (FSM)
– Exhaustively explore state (conceptually)
• Clever approaches  orders-of-magnitude faster vs. brute force. E.g.:
– Symbolically represent FSM, e.g., using binary decision diagrams (BDDs)
– Abstraction (simplify system for this specific property)
– Bounded model checking - unroll FSM for fixed number of steps (build on SAT)
• Only shows true/false for that many steps!!
– Counterexample guided abstraction refinement (CEGAR)
• Pros: Fully automated & easy-to-use (compared to theorem-provers)
• Cons: Can quickly become infeasible & often limited to narrow properties
– Eventually state explosion can overwhelm clever optimizations
• Model-checkers (excluding code analysis – discuss separately):
– SPIN – verify distributed systems, Promela language (license probably not OSS)
• Gerard Holzmann created of SPIN, won 2001 ACM Software System Award
– DiVinE: Distributed execution, can accept C/C++ too (BSD 3-clause)
– Others include NuSMV 2 (LGPL 2.1)
56
A low-level data structure:
Binary decision diagrams (BDDs)
BDD = data structure, can represent a Boolean function in compressed form
• Can perform operations directly on BDDs
• Easily determine equivalence & combine boolean functions
• Variable order matters, heuristics help determine order
• Some tools use BDDs to compute in reasonable time
• Don Knuth: “one of the only really fundamental data structures that came
out in the last twenty-five years”
Source: Images from Wikipedia. Key paper: Randal E. Bryant. "Graph-Based Algorithms for
Boolean Function Manipulation". IEEE Transactions on Computers, C-35(8):677–691, 1986 (widely cited)
57
Promela: Mars Pathfinder model
• Promela = Notation of the SPIN model-checker
• Next slide shows Promela model of Mars Pathfinder scheduling
algorithm (from SPIN source code)
– Explains recurring reset problem during mission on Mars
• Situation:
– High priority process that consumes data produced by a low priority
process
– Data consumption and production happens under the protection of a
mutex lock
– Mutex lock conflicts with the scheduling priorities, can deadlock the
system if high() starts up while low() has the lock set
– This is called “priority inversion”
• Model has 12 reachable states in the full (non-reduced) state space
- two of which are deadlock states
58
Promela: Mars Pathfinder example
mtype = { free, busy, idle, waiting, running };
show mtype h_state = idle;
show mtype l_state = idle;
show mtype mutex = free;
active proctype high() { /* can run any time */
end: do
:: h_state = waiting;
atomic { mutex == free -> mutex = busy };
h_state = running;
/* critical section - consume data */
atomic { h_state = idle; mutex = free }
od
}
active proctype low() provided (h_state ==
idle) { /* Note scheduling rule */
end: do
:: l_state = waiting;
atomic { mutex == free -> mutex = busy};
l_state = running;
/* critical section - produce data */
atomic { l_state = idle; mutex = free }
od
}
Source: SPIN source Version 6.2.5 (4 May 2013), file Test/pathfinder.pml
59
Abstract interpretation &
symbolic execution
• Abstract interpretation = sound approximation
programs. I.E., a partial execution without
performing all calculations
– In some definitions, must be based on monotonic
functions over ordered sets
– E.G., track “is variable +, 0, or –”… that’s enough
to determine signs from multiplication (without
overflow)
• Symbolic execution = analyze program by
tracking symbolic rather than actual values
60
So you want to prove that a
program meets a specification…
61
So you want to prove that a
program meets a specification…
• Often must write program with that goal in mind
–
–
–
–
Challenges: Pointers & threads
Variable assignment can be handled, but complicates
Loops can be handled, but complicates (loop invariants)
Functional languages common (at least underneath),
including Lisp, ML, OCaml, Haskell
• Various tools exist that can be used to do this
– Already seen tools that can prove programs, including PVS,
HOL4, Isabelle/HOL, HOL Light, Coq
– Following are some tools (and notations) specifically for it
• E.g., ACL2, Toccata/ProVal (Why3), Frama-C + (Jessie or WP), JML
(supported by many tools), SPARK, model-checking
• As with everything else here, omits much
62
ACL2
• Automated theorem-prover (BSD 3-clause)
– But often must guide via lemmas (“waypoints”)
• Models programs in Lisp-based language
– Can be used to model other implementations & hardware
– Specializes in automatic proofs of recursive programs
– “Industrial strength” version of Boyer–Moore theorem
prover NQTHM
• Given large set of proven patterns, repeatedly substitute
• Creators Robert S. Boyer, Matt Kaufmann, & J. Strother Moore won
2005 ACM Software System Award (began in Edinburgh, Scotland,
later at University of Texas, Austin)
• Many successes, esp. hardware / microprocessor
design (division, multiplication, etc.), proof of ivy
63
ACL2 examples (1 of 2)
(defun factorial (n) ; Trivial factorial implementation
(if (zp n)
1
(* n (factorial (- n 1)))))
(thm (> (factorial n) 0)) ; Prove that factorial always produces >0
; Prove that append is associative, that is, that
; (append (append xs ys) zs) equals (append xs (append ys zs))
(thm (equal (append (append xs ys) zs)
(append xs (append ys zs))))
Source: http://tryacl2.org/
64
ACL2 examples (2 of 2)
(defun rev (xs) ; Return list in reverse order
(if (endp xs) nil
(append (rev (rest xs)) (list (first xs)))))
(defthm rev-rev ; Prove reverse(reverse(x))=x
(implies (true-listp xs)
(equal (rev (rev xs)) xs)))
Source: http://tryacl2.org/
65
Toccata (née ProVal) approach
ACSL-annotated C
Frama-C
Plugins
…
WP
Jessie
JML-annotated
Java
Annotated
SPARK Ada
Krakatoa with
Jessie
SPARK 2014
tools
…
WhyML program + spec
WP has short-circuits
for alt-ergo & Coq
Automated
provers
Why3
Why3 can compute goals needed to
prove the code implements spec.
Encodes to & manages tools to prove goals.
Interactive
provers
…
…
Z3
Alt-Ergo
Isabelle/HOL
CVC4
Eprover
Coq
Specialty prover
for floating point
gappa
veriT
PVS
66
Why3 Proof Session Example
Source: “Why3: Shepherd Your Herd of Provers” by Bobot et al.
67
Java Modeling Language (JML)
example
Okay to refer to private data
public class BankingExample{
in publicly-viewable spec
/*@ spec_public */ private Integer balance;
JML uses Hoare-style
//@ invariant balance != null
preconditions, post//@ invariant 0 <= balance && balance <= MAX_BALANCE
//@ ensures this.balance = 0
public BankingExample { balance = 0; }
//@ requires amount != null
//@ requires 0 < amount && amount + balance < MAX_BALANCE
//@ modifies balance
//@ ensures this.balance = \old(this.balance) + amount
public void credit(Integer amount) {...}
conditions, and
invariants. JML supports
the design by contract
paradigm, & builds on
ideas from Eiffel, Larch,
& Refinement Calculus.
}
Many tools support JML, both for dynamic (run-time) checking & formal proofs, including
Krakatoa (with Jessie/Why3), OpenJML, KeY, Sireum/Kiasan, TACO, ESC/Java2..
Source: “Automated Program Verification” 2011,
https://courses.cs.washington.edu/courses/cse331/11wi/lectures/lect20-program-verification.pdf
68
ACSL (C) example: Swap
// File swap.c:
Precondition
/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b) ;
Postconditions
@ ensures B: *b == \old(*a) ;
@ assigns *a,*b ;
@*/
void swap(int *a,int *b)
{
int tmp = *a ;
*a = *b ;
ACSL = “ANSI/ISO C Specification Language”,
created for & used by Frama-C for C.
*b = tmp ;
It’s inspired by the Java Modeling Language (JML)
return ;
used by many tools for Java.
}
Source: http://frama-c.com/wp.html
69
ACSL (C) example: Binary search
/*@ requires n >= 0 && \valid (t+(0..n -1));
@ assigns \nothing ;
@ ensures -1 <= \result <= n -1;
@ behavior success:
@ ensures \result >= 0 ==> t[ \result ] == v;
@ behavior failure:
@ assumes t_is_sorted: \forall integer k1 ,
int k2;
@ 0 <= k1 <= k2 <= n -1 ==> t[k1] <= t[k2];
@ ensures \result == -1 ==>
@ \forall integer k; 0 <= k < n ==> t[k] != v;
@*/
int bsearch ( double t[], int n, double v) {
int l = 0, u = n -1;
/*@ loop invariant 0 <= l && u <= n -1;
@ for failure: loop invariant
@ \forall integer k; 0 <= k < n && t[k] == v
==> l <= k <= u;
@*/
while (l <= u ) {
int m = l + (u-l )/2; // better than (l+u)/2
if (t[m] < v) l = m + 1;
else if (t[m] > v) u = m - 1;
else return m;
}
return -1;
}
Source: Baudin et al, “ACSL: ANSI/ISO C Specification Language Version 1.6” Example 2.23
70
Jessie vs. WP
• Same purpose & general approach
– Accept C+ACSL annotations, create proofs, apply weakest
precondition (WP) approach, use Why/Why3
• Different memory modeling of C in math
– Jessie uses separation predicates inspired by separation
logic
– WP focuses on memory model parameterization
• Different implementation approach
– Jessie translates C directly into Why3’s language
– WP designed to cooperate with other Frama-C plug-ins
such as the value analysis plug-in
• WP presumes there are no run-time errors (RTEs); use a separate
plug-in (e.g., rte generation) to check for RTEs
71
Some key WP options
•
Memory model (how map C memory values to math)
– Hoare model: C variables mapped directly to logical variables. Very efficient,
easy & concise proofs. Can’t use heap or pointer read/write
– Typed model*: Heap values stored in separated, one for each atomic type.
Pointers are indexes into these arrays
– Bytes model: Heap is array of bytes, pointers are memory addresses. Very
precise, but proof obligations hard to discharge automatically
“Use the simpler models whenever… possible, and [use] more involved models
on the remaining more complex parts”
•
Arithmetics models (how to model C arithmetic in math)
– Natural Model*: Integer operations use mathematical integers
– Machine Integer Model: Integer operations performed modulo; proof
obligations hard to discharge
– Real Model*: Floating-point operations have no rounding (unsound)
– Float Model: Floating-point operations are mathematical with rounding,
consistent with IEEE. Most automated provers can’t handle; use gappa
* = Defaults of WP plug-in
72
Sample GUI: Frama-C and WP
Source: “WP 0.8” on Frama-C website
73
SPARK (Ada)
•
Designed for high-reliability applications
– Originally targeted at highly constrained run-time environments
•
Pre-2014 version was subset/superset of Ada. Pre-2014 version:
–
–
–
–
•
No dynamic memory allocation
Until recently, no threads (has added Ravenscar)
Adds specification language in comments
Developed by Bernard Carré and Trevor Jennings; much done by Rod Chapman, principal
engineer of Altran
Exploits Ada’s subtyping to automate many proofs
– Ada’s strict typing & additional information on ranges makes proof automation easier than for
some alternative implementation languages; often can enumerate all cases
•
•
•
Speed of C, but its strong typing counters errors & simplifies proofs
Successes reported, “Tokeneer” public, US lunar project “CubeSat”
SPARK 2014 version changes & relaxes many restrictions
– Uses Ada 2012 aspect notation (instead of specially formatted comments)
– Integrates with testing - contracts be proved, or they can be compiled and executed as runtime assertations
– Bigger subset: Adds bounded types with dynamic bounds, recursion, etc.
– SPARK 2014 has switched to Why3/Toccata approach – multi-prover support
Source: http://www.spark-2014.org
74
SPARK 2014 Example Spec (1 of 2)
pragma SPARK_Mode;
package Search is
type Index is range 1 .. 10;
type Element is new Integer;
type Arr is array (Index) of Element;
type Search_Result (Found : Boolean := False) is record
case Found is
when True =>
At_Index : Index;
when False =>
null;
end case;
end record;
function Value_Found_In_Range(A : Arr;
Val : Element; Low, Up : Index) return Boolean
is (for some J in Low .. Up => A(J) = Val);
75
SPARK 2014 Example Spec (2 of 2)
function Linear_Search(A : Arr; Val : Element) return Search_Result
with
Pre => Val >= 0,
Post => (if Linear_Search'Result.Found then
A (Linear_Search'Result.At_Index) = Val),
Contract_Cases =>
(A(1) = Val =>
Linear_Search'Result.At_Index = 1,
A(1) /= Val and then Value_Found_In_Range (A, Val, 2, 10) =>
Linear_Search'Result.Found,
(for all J in Arr'Range => A(J) /= Val) =>
not Linear_Search'Result.Found);
end Search;
76
SPARK 2014 Example Body
pragma SPARK_Mode;
package body Search is
function Linear_Search(A : Arr; Val : Element) return Search_Result is
Pos : Index'Base := A'First;
Res : Search_Result;
begin
while Pos <= A'Last loop
if A(Pos) = Val then
Res := (Found => True, At_Index => Pos);
return Res;
end if;
pragma Loop_Invariant(Pos in A'Range and then not Value_Found_In_Range(A, Val, A'First, Pos));
pragma Loop_Variant (Increases => Pos);
Pos := Pos + 1;
end loop;
Res := (Found => False);
return Res;
Source for SPARK 2014 example: SPARK 2014 Tutorial,
end Linear_Search;
http://docs.adacore.com/spark2014-docs/html/ug/tutorial.html
end Search;
77
Some other toolsuites
• Dafny (Microsoft Research)
–
–
–
–
Programming language with built-in specification constructs
Dafny verifier is run as part of the compiler to verify functional correctness
Dafny compiler produces code for .NET platform
Appears to be OSS: Dafny & underlying Boogie are Microsoft Public License;
Z3 is MIT license
• KeY (http://www.key-project.org/)
– Proofs of Java programs annotated with JML
– OSS (GPL)
• OpenJML (http://jmlspecs.sourceforge.net/)
– Proofs of Java programs annotated with JML
– Translates into SMT-LIB format, passes to backend SMT solvers
– OSS (GPLv2)
• KIV system
– Specs can refine down to Java
– Proprietary, free for noncommercial use
78
Model-checking FM tools for
programs (code analysis)
• Model-checking can be applied to code, too:
– In practice, often limited to looking for specific properties/defects
(e.g., TOCTOU, temp files)
– Approximations – can be sound (always finds problem under certain
assumptions) but with false positives
• Java PathFinder (NASA)
– State software model checker for Java™ bytecode
– Weird NASA license
• MOPS – Analyze for very specific security vulnerabilities
– For C, has analyzed Linux kernel & even Linux distro!
– [Benjamin Schwarz et al, “Model Checking An Entire Linux Distribution
for Security Violations” – 6 vulnerability patterns]
• DiVinE (BSD 3-clause; accepts C/C++, builds on LLVM)
• Other tools: BLAST, CPAchecker (Apache 2.0), Microsoft SLAM*, …
79
MOPS – Checking a Linux
distribution
• “Model Checking An Entire Linux Distribution for Security
Violations”
– by Benjamin Schwarz, Hao Chen, David Wagner, Geoff Morrison*,
Jacob West*, Jeremy Lin, Wei Tu (*=Fortify, rest are UC Berkeley);
ACSAC 2005
– Did software model checking for security properties on big scale
– Entire Linux distro, 839 packages, 60 million LOC
– Discovered 108 exploitable bugs
• “MOPS errs on the conservative side: MOPS will catch all the bugs
for a property (… it is sound, subject to certain requirements), but it
[reports] spurious warnings.”
• Looked for: TOCTTOU (filesystem race), Standard File Descriptors,
Temporary Files, strncpy (misuse), Chroot Jails, Format String
80
Abstract interpretation &
symbolic execution
• Example: Kestrell CodeHawk C Analyzer*
– Given targeted (critical) vulnerability types…
– Tries to mathematically prove the absence of those
vulnerabilities in all relevant code, using abstract interpretation
– If cannot prove it, warning issued with remaining proof
obligations
• GrammaTech CodeSonar*
– Has built-in set of (critical) vulnerability types
– Uses symbolic execution engine to explore program paths,
reasoning about program variables & relations
– Dataflow analysis prunes infeasible program paths
– Procedure summaries are refined and compacted as-go
* Proprietary programs
81
Formalizing & verifying
mathematical theorems (not code)
• Mathematicians can make mistakes
– Euclidean geometry: Omission of Pasch's axiom went unnoticed for
2000 years
– Mathematicians normally “sketch” a proof without details
– We can formalize math itself so it’s mechanically proved at every step
• Freek Wiedijk has compiled info on several math formalization tools
– “Formalizing 100 theorems” lists tools used to formalize math, & some
theorems they’ve formalized - http://www.cs.ru.nl/~freek/100/
– “The Seventeen Provers of the World” demos 17 tools in more detail
• Many different tools
– Some tools for formalizing math can also prove programs/specs, e.g.,
HOL Light, Isabelle, Coq, ACL2
– Some specialized for just math proofs, e.g., Mizar & Metamath
• Formalized math can sometimes be a basis for proving
specs/programs
82
Mizar & Metamath
(tools for formalizing math)
•
Mizar (proprietary program, OSS theorems)
– Notation designed to be similar to traditional math notation
– Publish a math journal focused on formalization
•
Metamath (OSS programs, public domain theorems) – (I find this one intriguing!)
– Only 1 built-in logic rule (substitution), ability to define axioms & proofs
•
•
•
•
Tiny kernel (can verify proofs with ~350 lines of Python)
Very general logic system, can then specify axioms & proofs to build up from there
Designed to be easier for non-mathematician (esp. computer-literate) to follow steps
Founded on a Alfred Tarski formalization exactly equivalent to traditional textbook formalization, but
without “proper substitution” and “free variable” (eases mechanization)
– Includes a modern “Principia Mathematica”-like set of proofs that’s easier to read than P.M.
•
•
•
States a very few axioms (sets & logic), e.g., modus ponens
Grows from there, e.g., proves basics about numbers & their properties
Proves 2+2=4 in 10 steps, transitively uses 2,452 subtheorems & 25,933 steps
http://us.metamath.org/mpegif/2p2e4.html
– You can learn a lot about math from its documentation!
•
•
•
Esp. “Metamath” book and “Metamath Proof Explorer” http://us.metamath.org
Both Mizar & Metamath’s set.mm use ZFC + Tarski’s axiom (for category theory)
Both provide little automation for proof creation
– Don’t handle goal change well
– Makes them much less applicable to software, which does change
– But again, some of their math results may be useful in computing
83
General caveats when considering
formal methods
• Many approaches require significant math knowledge
– Education needed (comparable to engineers)
– Some exceptions (e.g., sometimes model-checking &
abstract interpretation, where spec can be pre-canned)
• Typically must apply during development
– To reduce requirements ambiguity – need to apply when
creating requirements
– All tools have limits – write so can easily apply to them
• Only proves what you ask (“it doesn’t answer questions
you don’t ask”†)
• Only as good as their assumptions – are they
justifiable?
† Credit: Paul E. Black, “A Brief Introduction to Formal Methods”
84
Current status of formal methods
• Formal methods already useful & used in some circumstances
• Tool problems (often hard-to-use/outdated UI, lack of
integration/standards, …)
• Handling scale – full “level 2” rigor historically small programs
– Can get larger by only applying at requirement level, analyzing models
(e.g., design), just specialized properties, dropping soundness – useful!
– Improved algorithms, more CPU power, combining algorithms, OSS, &
more research have potential for scaling up in future
• Hybrid approaches seem promising, e.g., the Toccata (ProVal) suite
• You’ve sampled some the FM notations/tools available, e.g.:
– Z, Alloy; Prover9, E theorem prover; Coq, HOL4, HOL Light,
Isabelle/HOL, PVS; CVC4, alt-ergo; SPIN; ACL2, SPARK, Toccata (ProVal)
• Valuable for high-assurance security & in some cases today
– With potential for far larger applications
– Tools/techniques can be repurposed, e.g., to increase assurance
85
Open Proofs
86
What’s slowing FM maturation?
• Much research & some use, but FM tools are often:
– Hard to install, hard to learn to use
– Hard to use, time-consuming, & don’t scale
– Poorly integrate with other tools/existing environments
• Need to mature FM if they’re to be broadly used
– Hard problem, relatively few research $ ... but decades?
• FM maturation hindered by “culture of secrecy”
– Details of FM use often unpublished, classified
– Details of FM tools (& the tools!) often unshared/lost
• Result (broadly stated):
– Researchers/toolmakers receive inadequate feedback
• From developers & other researchers/toolmakers
– Researchers/toolmakers waste time/$ rebuilding tools
– Educators difficulty explaining (esp. without examples)
– Developers don’t understand, uncertain value
– Evaluators/end-users don’t know what to look for
87
Researchers/toolmakers need more
than papers: LIMMAT to NANOSAT
Researchers/toolmakers suffer from lack of information
LIMMAT/NANOSAT developers: “From the publications alone, without
access to the source code, various details were still unclear... what we did
not realize, and which hardly could be deduced from the literature, was
[an optimization] employed in GRASP and CHAFF [was critically
important]... Only [when CHAFF's source code became available did] our
unfortunate design decision became clear... The lesson learned is, that
important details are often omitted in publications and can only be
extracted from source code. It can be argued, that making source code of
SAT solvers available is as important to the advancement of the field as
publications”
- [Biere, “The Evolution from LIMMAT to NANOSAT”, Apr 2004]
88
Need: Working ecosystem
• Researchers/Toolmakers/Educators
– Learn details from others (papers often inadequate) – share code!!
– Build on/experiment with existing tools (vs. rebuilding)
• Developers of implementations to be proved
– Learn from other developers
– Build on/experiment with proven systems/components
– Share issues with toolmakers (so tools can improve)
• Evaluators/End-users
– Evaluate evidence (determine adequacy, give feedback)
– Evaluate other systems based on this experience
Researchers/
Toolmakers/
Educators
Developers
Evaluators/
End-users
89
“Open proof” idea
• “Open proof” (new term):
– Source code, proofs, and required tools: OSS
• Anyone can examine/critique, improve upon, collaborate with others for
improvements
– Not just software, but what’s proved & tools
– Example for training, or as useful component
• Extends OSS idea for high assurance
– Enables legal collaboration
– Similar to mathematics field
– Method for speeding up tech transition
• Encourage/require government-funded results be open proofs
– By default – evaluate exceptions
• Application of “open access” applied broadly
– See: http://www.phdcomics.com/comics/archive.php?comicid=1533
• Goal: Make supplier identity irrelevant
• Don’t need everything to be an open proof
– Examples & building blocks (inc. standards’ API)
90
Some open proofs
• “Tokeneer” (SPARK Ada)
• seL4 microkernel (Isabelle/HOL)
• ACL2 library (ACL2)
More info:
http://www.openproofs.org
91
Countering trusting trust through
diverse double-compiling (DDC)
92
The trusting trust attack:
Disseminating malicious compilers
• Corrupted executable = an executable that does not
correspond to its putative source code
– An executable e corresponds to source code s iff execution
of e always behaves as specified by s when the execution
environment of e behaves correctly
• Trusting trust attack = An attack in which:
– “the attacker attempts to disseminate a compiler
executable that produces corrupted executables,
– at least one of those produced corrupted executables is a
corrupted compiler, and
– the attacker attempts to make this situation selfperpetuating”
Source: Wheeler 2009, “Fully Countering Trusting Trust through Diverse Double-Compiling (DDC)”
93
A maliciously-corrupted compiler
can cause serious damage
Trustworthy
source
code...
can produce
maliciously
corrupted
executables
Critical
program
source
login
Analysis
program
source
Symbolic debugger
Compiler
source
C compiler
Compiler executable
(maliciously corrupted)
Perpetuates
Critical
program
Analysis
program
Compiler
executable
1974: Karger & Schell first described (obliquely)
1984: Ken Thompson. Demo’d.
Fundamental security problem
94
Trusting trust countermeasure:
Diverse double-compiling (DDC)
• Idea created by Henry Spencer in 1998
–
–
Uses a different (diverse) trusted* compiler
Two compilation steps
• Compile source of “parent” compiler
• Use results to compile source of compiler-under-test
–
If result bit-for-bit identical to compiler-under-test cA, then
source and executable correspond
• Testing for bit-for-bit equality is easy
–
–
Source code may include malicious/erroneous code, but
now we can review source instead
Only brief description - didn’t describe in detail, prove it,
or demonstrate it. Didn’t even name it
• David A. Wheeler’s 2009 PhD dissertation
* We will define “trusted” soon
95
Wheeler’s dissertation thesis
The trusting trust attack can be detected and
effectively countered using the “Diverse DoubleCompiling” (DDC) technique, as demonstrated by:
1. a formal proof that DDC can determine if source
code and generated executable code correspond
2. a demonstration of DDC with four compilers (a
small C compiler [tcc], a small Lisp compiler, a
small maliciously corrupted Lisp compiler, and a
large industrial-strength C compiler, GCC), and
3. a description of approaches for applying DDC in
various real-world scenarios
Source: Wheeler 2009, “Fully Countering Trusting Trust through Diverse Double-Compiling (DDC)”
96
Diverse double-compiling (DDC)
DDC Process
Claimed Origin
cGP : executable
(grandparent)
sP: source
ePeffects
(of parent
e1: environment c ?)
eP: env.
o1
P
cT: executable
(trusted compiler)
e1effects
sP: source
(of parent cP?)
1
stage1
sA: source
(of cA?)
2
sA: source
e2effects
e2: environment (of cA?)
stage2: executable;
to run on
eArun: environment
cP
o2
eAeffects
eA: env.
cA: executable; compiler
under test, to run on
eArun: environment
97
Assumptions (informal)
• DDC performed by trusted programs/processes
–
–
Includes trusted compiler cT, trusted environments,
trusted comparer, trusted acquirers for cA, sP, sA
Trusted = justified confidence that it does not have
triggers and payloads that would affect the results of
DDC. Could be malicious, as long as DDC is unaffected
• Correct languages (Java compiler for Java source)
• Compiler defined by sP is deterministic (same
inputs always produce same outputs)
–
Real compilers typically deterministic
• Non-deterministic compilers hard to test & can’t use compiler
bootstrap test
98
DDC does not assume that different
compilers produce identical executables
• Different compilers typically produce different executables
• But given this C source:
#include <stdio.h>
main() {
printf("%d\n", 2+2);
}
• And two different properly-working C compilers:
–
–
Resulting executables will usually differ
Running those executables should produce “4” (modulo text encoding,
& presuming certain other assumptions)
99
Why not always use
the trusted compiler?
• May not be suitable for general use
– May be slow, produce slow code, generate code for a
different CPU, be costly, have undesirable license
restrictions, may lack key functions, etc.
– In particular, a simple easily-verified compiler (with limited
functionality & optimizations) could be used
• Using a different compiler greatly increases confidence
that source & executable correspond
– Attacker must now subvert multiple executables and
executable-generation processes to avoid detection
– DDC can be performed multiple times, using different
compilers and/or different environments, increasing
difficulty of undetected attack
100
Three proofs (using FOL)
• Proof 1: “If DDC produces the same executable as the compiler-under-test
cA, then source code sA corresponds to the executable cA”
(5 assumptions, 19 steps)
(stage2 = cA) -> exactly_correspond(cA, sA, lsA, eArun).
• Proof 2: “Under benign conditions and cP_corresponds _to_sP, the DDC
result stage2 and the compiler-under-test cA will be the same”
(9 assumptions, 30 steps)
stage2 = cA.
• Proof 3: “When there’s a benign environment & a grandparent compiler,
proof 2 assumption cP_corresponds_to_sP is true”
(3 assumptions, 10 steps)
exactly_correspond(cP, sP, lsP, eA).
• Proofs found by prover9, verified by ivy & by multi-person review
101
First DDC demonstration: tcc
• Performed on small C compiler, tcc (ACSAC)
–
Separate runtime library, handle in pieces
–
–
–
x86: Constants -128..127 can be 1 byte (vs. 4)
tcc detects this with a cast (prefers short form)
tcc bug – cast produces wrong result, so tcc compiledby-self always uses long form
• tcc defect: fails to sign-extend 8-bit casts
• tcc junk bytes: long double constant
–
–
Long double uses 10 bytes, stored in 12 bytes
Other two “junk” bytes have random data
• Fixed tcc, technique successfully verified fixed tcc
• Used verified fixed tcc to verify original tcc
It works!
102
Demonstration:
Goerigk Lisp compilers
• Pair of Lisp compilers, “correct” & “incorrect”
–
–
“Incorrect” implemented the trusting trust attack
Ported to Common Lisp
• DDC applied
–
–
“Correct” compiler compared correctly, as expected
Executable based on “incorrect” source code did not
match the DDC results when DDC used the “correct”
source code, as expected
• “Diff” between results revealed that the “incorrect”
executable was producing different results, in particular for a
“login” program
• Tip-off that executable is probably malicious
103
Demonstration: GCC
• GNU Compiler Collection (GCC) is widely-used compiler in
industry – shows DDC scales up
–
Many languages; for demo, chose C compiler
• Used Intel C++ compiler (icc) as trusted compiler
–
Completely different compiler
• Fedora didn’t record info to reproduce executable
• Created C compiler executable to capture all necessary data
& use that as compiler under test
–
–
–
Chose GCC version 3.0.4 as compiler under test
“gcc” is a front-end that runs the real compiler programs; C
compiler is actually cc1
Code outside of GCC (including linker, assembler, archiver, etc.)
considered outside compiler
104
DDC applied to GCC (simplified)
DDC Process
cT: executable : icc
(trusted compiler)
1
sP=sA : source
of GCC 3.0.4 stage1
2
stage2: executable;
to run on
eArun: environment
Claimed Origin
cGP : GCC in
Fedora 9
sP=sA : source
of GCC 3.0.4
o1
cP
o2
cA: executable; compiler
under test, to run on
eArun: environment
105
DDC applied to GCC (continued)
• Challenges:
–
–
–
“Master result” pathname embedded in
executable (so made sure it was the same)
Tool semantic change (“tail +16c”)
GCC did not fully rebuild when using its build
process (libiberty library not rebuilt)
• This took time to trace back & determine cause
• Once corrected, DDC produced bit-for-bit
equal results as expected
106
How can an attacker counter DDC?
Must falsify a DDC assumption, for example:
• Swap DDC result with cA during DDC process (!)
–
Defender can protect DDC environment
• Make compiler-under-test ≠ compiler used
–
–
If environment may provide inaccurate compiler under test, defender can
extract without using environment
If environment may run different compiler, defender can redefine
“compiler” to include environment & apply DDC
• Subvert trusted compiler/trusted environment(s)
–
–
Challenge: Don’t usually know what they’ll be
Defender can use DDC multiple times
• Attacker must subvert them all, while defender only needs to protect
at least one—unusual for defender
107
Guidelines for compiler suppliers
(Appendix D)
1.
2.
3.
Pass the compiler bootstrap test, if applicable
Don’t use or write uninitialized values
Record the detailed information necessary to recompile the compiler and
produce the same bit sequence
4. Don’t include information about compilation process inside files used during
later compilation
5. Encourage the development of alternative implementations of languages. Use or
help develop public specs for computer languages (preferably open standards)
6. Eliminate roadblocks to alternative implementations, particularly patents
7. Make the compiler portable and deterministic
8. Consider using a simpler language subset to implement the compiler
9. Release self-parented compiler executables, if applicable
10. Release the compiler as FLOSS, and choose a FLOSS compiler as its parent.
Alternatively, though less effective, release source to trusted third parties
11. Apply DDC before each release
108
Vulnerability Disclosure
109
Vulnerability disclosure:
The debate!
• Full disclosure
– Disclose vulnerabilities directly to public
– Supplier finds out when the public does
– May include example of exploit
• Coordinated disclosure
– Disclose vulnerabilities only after coordination with supplier
– May automatically disclose to public after period of time (common)
– Also called “responsible disclosure” but this is a highly biased term
• No disclosure
– Often goal is to exploit vulnerability (directly, or to sell to those who will).
Remember: Many people are in this mode!
• Separate issue: “bug bounties”
–
–
–
–
Paying for vulnerability reports, as a reward
Bug bounties can be great, but economics not favorable to defense
I think we should limit whom vulnerability information can be sold to
http://www.dwheeler.com/blog/2013/11/16/#vulnerability-economics
110
Full disclosure
• Crypto-Gram Newsletter by Bruce Schneier, October 15, 2013,
https://www.schneier.com/crypto-gram-1310.html:
– “Among IT security professionals, it has been long understood that the public
disclosure of vulnerabilities is the only consistent way to improve security….
– It wasn't always like this. In the early years of computing, it was common for
security researchers to quietly alert the product vendors about vulnerabilities,
so they could fix them without the "bad guys" learning about them. The
problem was that the vendors wouldn't bother fixing them, or took years
before getting around to it. Without public pressure, there was no rush.
– This all changed when researchers started publishing. Now vendors are under
intense public pressure to patch vulnerabilities as quickly as possible. The
majority of security improvements in the hardware and software we all use
today is a result of this process... Without public disclosure, you'd be much
less secure against cybercriminals, hacktivists, and state-sponsored
cyberattackers.”
•
“We don't believe in security by obscurity, and as far as we know, full
disclosure is the only way to ensure that everyone, not just the insiders,
have access to the information we need.” - Leonard Rose
111
Coordinated disclosure
• Originally called “responsible disclosure”
– “It’s Time to End Information Anarchy” by Scott Culp, October 2001
– Term still used, but it is extremely biased (“framing”)
– Microsoft now calls it “coordinated disclosure” – I recommend that
term instead
• Notion: Tell supplier first, disclose after supplier releases a fix
– That way, attackers who don’t know about it can’t exploit information
• Microsoft has a coordinated disclosure policy with no time limit as
long as the supplier keeps yakking
– http://www.theregister.co.uk/Print/2011/04/19/microsoft_vulnerabili
ty_disclosure_policy/
• But many suppliers never fix non-public vulnerabilities & just stall
– Incorrectly assumes attackers are not already exploiting vulnerability
(when they are, nondisclosure puts public at greater risk)
112
Coordinated disclosure
with time limit
• Common variant (compromise?) of coordinated (“responsible”) disclosure
– Maximum time limit (“embargo”) set for public disclosure
– Purpose of time limit: Supplier might actually fix the vulnerability for a change 
– Suppliers always recommend longer embargo times than everyone else 
• Some examples of public disclosure time limits:
– linux-distros: <7 days preferred, up to 14 days allowed, up to 19 days if Thu/Fri report &
disclosure on Mon/Tue http://oss-security.openwall.org/wiki/mailing-lists/distros
– oCERT: 14 days standard; 7 days if trivial, 30 days if critical/complex, up to 2 months
“extremely exceptional” https://www.ocert.org/disclosure_policy.html
– CERT/CC: 45 days “regardless of the existence… of patches or workarounds…
Extenuating circumstances … may result in earlier or later disclosure... We will not
distribute exploits” https://www.cert.org/vulnerability-analysis/vul-disclosure.cfm
– Google: 60 days “reasonable upper bound” http://googleonlinesecurity.blogspot.com/
2010/07/rebooting-responsible-disclosure-focus.html
• Personal opinion: Coordinated disclosure with ~3 week embargo
– Discuss time with supplier, but attackers are probably exploiting it already
– Don’t bother coordinating with suppliers known to ignore vulnerability reports
113
Disclosure: More information
• “Full Disclosure” by Bruce Schneier (November 15, 2001)
https://www.schneier.com/crypto-gram-0111.html#1
• “Full Disclosure and Why Vendors Hate it” by Jonathan
Zdziarski (May 1, 2008)
http://www.zdziarski.com/blog/?p=47
• “Software Vulnerabilities: Full-, Responsible-, and NonDisclosure” by Andrew Cencini, Kevin Yu, Tony Chan
• “How long should security embargos be?”, Jake Edge,
https://lwn.net/Articles/479936/
• “ Vulnerability disclosure publications and discussion
tracking” https://www.ee.oulu.fi/
research/ouspg/Disclosure_tracking
114
Recommendations for developers –
handling vulnerability reports
• Create an easy way to report vulnerabilities
–
–
–
–
Typically set up email address (“secure” or “security” @ “supplier”)
Make sure this is well-documented & easy to find!
Pre-establish an encrypted channel (e.g., encrypted email or HTTPS page)
Beware: Attackers often try to monitor these channels…
• Monitor for vulnerabilities about your software & libraries embedded in it
(e.g., Google alerts, watch major vulnerability sites) - don’t be last to know
• Have working development environment with CM of all released versions
– So can quickly check out & fix released version(s)
• Have strong automated regression test suite & needed old hardware, set
up to run at a moment’s notice
– If it takes too long to test, you are not ready to release
• Have automated patch release/install system established (with keys)
– So users can quickly & automatically receive fixes (airgap signing keys!!)
• Always credit & thank vulnerability reporter (unless requested otherwise)
115
We’ve covered…
• Formal methods
– General approaches & specific tools available
– How to applying them varies by purpose
• Open proofs
• Malicious tools / trusting trust attack
– Countering using diverse double-compiling (DDC)
• Vulnerability disclosure
116
Released under CC BY-SA 3.0
• This presentation is released under the Creative Commons AttributionShareAlike 3.0 Unported (CC BY-SA 3.0) license
• You are free:
– to Share — to copy, distribute and transmit the work
– to Remix — to adapt the work
– to make commercial use of the work
• Under the following conditions:
– Attribution — You must attribute the work in the manner specified by the
author or licensor (but not in any way that suggests that they endorse you or
your use of the work)
– Share Alike — If you alter, transform, or build upon this work, you may
distribute the resulting work only under the same or similar license to this one
• These conditions can be waived by permission from the copyright holder
– dwheeler at dwheeler dot com
• Details at: http://creativecommons.org/licenses/by-sa/3.0/
• Attribute as “David A. Wheeler and the Institute for Defense Analyses”
117