Introducing
Your new presentation assistant.
Refine, enhance, and tailor your content, source relevant images, and edit visuals quicker than ever before.
Trending searches
Thanks to:
x86, LLVM, Linux, Browser APIs, POSIX interfaces
"Exhaustively testable pseudo-code"
[Using Formal Methods at Amazon Web Services]
seL4, CompCert, FSCQ, certiKOS, Rocksalt, Nucleus, QUARK
Secure essential infrastructure & contain the rest.
QUARK, Verve/Nucleus, Rocksalt
Rocksalt, Ivory/Tower, SpiralGen, BilbyS
Facebook INFER; UC-KLEE, Rockwell Collins Workbench; mCertiKOS
Tactic libraries and SMT/SAT solver integration
FSCQ, Nucleus, mCertiKOS
seL4 Microkernel
Available open source.
CompCert Verifying C Compiler
7% slower than gcc -O1,
12% slower than gcc -O2
All verified to be functionally correct!
Formal Method Based Tools
What are "Formal Methods"?
Functional
Correctness
Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals ... to problems in software and hardware specification and verification.
Understanding Formal Methods, Jean-Francois Monin, 2003
No Run-Time
Errors
"I know it when I see it" —Justice Potter Stewart
Strength of Guarantee
Characteristics:
Type
Safety
Automatic/Unlimited
PhD Years/Kloc
Level of User Effort/Scalability
Notional graph
Using Formal Methods to produce more secure vehicles.
Been there, tried that, wasn't impressed.
Survey Results on Using Formal Methods
Source: Formal Methods: Practice and Experience, ACM Computing Surveys, October 2009
Formal methods can help with other security challenges as well:
Ex: Amazon Web Services use of TLA+
Ex: NICTA analysis of seL4
Today
many things are networked computers.
Phoenix Exploit Kit, 2010
Enabling the masses to launch pernicious attacks at scale.
And attackers take control with distressing ease.
and essentially all computers are networked.
Astrée
Symbolic Execution
(FuzzBALL, KLEE)
Verified code is not intrinsically slower, but verifying faster code can be more time consuming.
Significant overhead in terms of lines of code/proof, but level of effort is becoming a reasonable investment for certain kinds of software.
10K LoC, 480K LoP; 13(8) person years
42K LoC+P; 3 person years
24K LoC+P; <5 person years
3K LoC, 18.5K LoP; 1 person year
407 LoC, 14.4K LoP; not reported
100 LoC, 10K LoP; <2 person years
6K LoP+C; 0.75 person years
5.5K LoP+C; 0.5 person years
206 vs 227 cycles in 1-way IPC fastpath
2x speed of gcc-O0, 7% slower than gcc -O1, 12% slower than gcc -O2
Performance roughly 80% of xv6 file system.
<2x slowdown on most lmbench benchmarks
Performance equal to OpenSSL 0.9.1c (March 1999)
1M instructions/second; faster than Google's checker
“competitive performance on macro-benchmarks when compared to native garbage collection.”
24% overhead wrt WebKit baseline on the top 10 Alexa Web sites
Source: Formal Methods: Practice and Experience, ACM Computing Surveys, October 2009
Keeping Up
The Fine Print
Time to produce a proof can be serious impediment to adoption.
All proofs come with assumptions.
Violate those assumptions and all bets are off.
(Many of the artifacts we've considered lack features.)
John Regehr et al found 325 bugs in various C compilers, including CompCert [PLDI 2011].
CompCert bugs were in:
Facebook's INFER sound static analyzer processes millions of lines of code and thousands of diffs per day.
But, proves only the absence of null pointer exceptions and resource leaks.
"The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. ...CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task."
Source: Moving Fast with Software Verification, NASA Formal Method Symposium, 2015
Source: Finding and Understanding Bugs in C Compilers, PLDI 2011
Type systems (C, Java, Haskell, ...)
Comprehensive Formal Verification of an OS Microkernel, ACM Transactions on Computer Systems, February 2014.
http://www.wired.com/2015/07/hackers-remotely-kill-jeep-highway/
Xavier Leroy, Formal certification of a compiler back-end, POPL 2006