Loading presentation...

Present Remotely

Send the link below via email or IM


Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.


Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

Using Formal Methods to Eliminate Exploitable Bugs

No description

Kathleen Fisher

on 7 October 2016

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Using Formal Methods to Eliminate Exploitable Bugs

Using Formal Methods to Eliminate Exploitable Bugs
Kathleen Fisher
Tufts University
Original Program Manager, DARPA's HACMS program

Networked computers are

Formal Methods can eliminate many exploitable vulnerabilities.
Been there, tried that, wasn't impressed.
Some Evidence:
Using Formal Methods to produce more secure vehicles.
Formal Methods: An Overview
Within Reach?
Critical parts of critical systems are built out of verified components & their composition is verified.
Buggy software is no longer an easy attack vector.

Black Hat is reduced to non-scalable attack vectors:

Andrew Appel
Adam Chlipala

Darren Cofer

Rockwell Collins
Drew Dean
Dan Guido
Trail of Bits
Joe Hendrix
many things are networked computers.
Why so insecure?
Faulty Design
Buggy Specifications
Implementation Errors
Side-channel leaks
Gullible users
Weak passwords
Malicious insiders
Physical security failures
Reliance on 3rd party software
Faulty/malicious hardware
And the list goes on...
Many Exploitable Vulnerabilities
Exploit Kits leverage software bugs
CVE-2009-0836: Buffer Overflow
CVE-2009-0927: Missing Bounds Check
CVE-2009-1869: Integer Overflow
CVE-2010-0188: Unspecified
CVE-2010-0840: Unspecified
CVE-2010-0842: Invalid Array Index
CVE-2010-1297: Memory corruption
CVE-2010-1818: Unmarshalling bad ptr
CVE-2010-1885: Mishandling escapes
CVE-2010-2883: Buffer overflow
Source: The Exploit Intelligence Project, Dan Guido
Ubiquitous and Pernicious
Remote code execution on
all Windows platforms
(July 20, 2015). Caused by a buffer underflow in the Adobe Type Manager Library.
Missing bounds check in OpenSSL allows theft of secret keys, user names and passwords, instant messages, emails, documents without leaving a trace.
In 2012, 3,436 vulnerabilities had public exploits available. 42% of total number of vulnerabilities.
Source: IBM X-Force 2012 Trend and Risk Report
What software is worth verifying?
Separation Kernel:
seL4 [SOSP 2009, ToCS 2014]
mCertiKOS [POPL 2015]
eChronos [echronos.org]
C Compiler:
CompCert [POPL 2006]
File Systems:
FSCQ [SOSP 2015], BilbyFS [OpSysRev 2014]
Web Browser:
Browser Sandbox:
RockSalt [PLDI 2012]
Crypto Algorithms:
SHA-256, HMAC [USENIX 2015]
AES-128, SHA-384, ECDSA(NIST P-384) [HILT 2013]
Garbage Collector:
Nucleus [PLDI 2010]
Impediments to Using Formal Methods
Why is now a good time to revisit hypothesis?
Faster Hardware. More memory.
More automation
More infrastructure
Source: The Free Lunch Is Over: A Fundamental Turn Toward Concurrency in Software
Source: Daniel Le Berre, The International SAT Solver Competitions
[A] significant part of the effort in existing projects was spent on the further development of verification tools, on formal models for low-level programming languages and paradigms, and on general proof libraries...
Future efforts will be able to build on these tools and reach far-ranging verification goals faster, better, and cheaper.
Gerwin Klein, Formal OS Verification—An Overview

Picking 80 problem point, the best time has dropped from 1000 (2002) to 40 seconds (2010).
The Setup
Program thesis:

FM can yield vehicles less susceptible to remote cyber attack.

Threat model:

No physical access, full knowledge of system and source code.


Hardware assumed to be correct.

Experimental Platforms:

Arducopter and Boeing's Unmanned Little Bird (ULB)

Source: DYI Drones
Source: Boeing
Baseline Security Assessment
Red Team:
Attacker could crash legitimate ground control station & hijack quadcopter in flight.

Source: Darren Cofer, Rockwell Collins
The Evolving SMACCMCopter
Source: DARPA HACMS program slides
The SMACCMCopter: 18-Month Assessment
What are "Formal Methods"?
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
"I know it when I see it" —
Justice Potter Stewart
Based on math
Capable of proving properties of code and models
But, read the fine print!
Assumptions may be unreasonable.
Guarantees may be too weak.
Formal Method Based Tools
Level of User Effort/Scalability
PhD Years/Kloc
Strength of Guarantee
No Run-Time
Notional graph
Type systems (
C, Java, Haskell, ...
Symbolic Execution
Bind, QEMU
Model Checkers
We have found that testing the code is inadequate as a method to find subtle errors in design, as the number of reachable states of the code is astronomical. So we looked for a better approach.
Use of Formal Methods at Amazon Web Services, 2014
Distributed System Protocols (Amazon)
Device Drivers (Microsoft)
Sound Static Analyzers
Astrée, Frama-C, INFER
Aviation Software (Airbus)
SSL Stack (PolarSSL)
Mobile Applications (Facebook)
Verified Runtime Monitoring
Browser Sandbox (Google)
Automatic Theorem Provers
Alt-Ergo, VCC, Z3
OSEK-Certified Vehicle OS (China)
Nucleus Garbage Collector (Microsoft)
Interactive Proof Assistants
ACL2, Coq
seL4 Microkernal (NICTA)
CompCert (INRIA)
HMAC/SHA-256 (Princeton)
The Problem of Expertise
The Required Level of Effort
Performance Consequences
Lessons Learned
On-Going Research & Challenges
Taking Stock
Survey Results on Using Formal Methods
Source: Formal Methods: Practice and Experience, ACM Computing Surveys, October 2009
Source: Formal Methods: Practice and Experience, ACM Computing Surveys, October 2009
The SMACCMCopter flies:
Stability control, altitude hold, directional hold, DOS detection.
GPS waypoint navigation 80% implemented.

Air Team proved system-wide security properties:
The system is memory safe.
The system ignores malformed messages.
The system ignores non-authenticated messages.
All “good” messages received by SMACCMCopter radio will reach the motor controller.

Red Team:
Found no security flaws in six weeks with full access to source code.

Penetration Testing Expert:
The SMACCMCopter is probably “the most secure UAV on the planet.”

Open source: autopilot and tools available from http://smaccmpilot.org
Keeping Up
seL4 Separation Kernel [SOSP 2009; ToCS 2014]
10K LoC, 480K LoP; 13(8) person years
CompCert Verifying C compiler [POPL 2006]
42K LoC+P; 3 person years
FSCQ File System [SOSP 2015]
24K LoC+P; <5 person years
certiKOS Hypervisor [POPL 2015]
3K LoC, 18.5K LoP; 1 person year
SHA-256/HMAC [USENIX 2015]
407 LoC, 14.4K LoP; not reported
Rocksalt Sandbox [PLDI 2012]
100 LoC, 10K LoP; <2 person years
Nucleus Allocator/Garbage Collector [PLDI 2010]
6K LoP+C; 0.75 person years
QUARK Web Browser [USENIX 2012]
5.5K LoP+C; 0.5 person years
Significant overhead in terms of lines of code/proof, but level of effort is becoming a reasonable investment for certain kinds of software.
seL4 Separation Kernel [SOSP 2009; ToCS 2014]
206 vs 227 cycles in 1-way IPC fastpath
CompCert Verifying C compiler [POPL 2006]
2x speed of gcc-O0, 7% slower than gcc -O1, 12% slower than gcc -O2
FSCQ File System [SOSP 2015]
Performance roughly 80% of xv6 file system.
certiKOS Hypervisor [POPL 2015]
<2x slowdown on most lmbench benchmarks
SHA-256/HMAC [USENIX 2015]
Performance equal to OpenSSL 0.9.1c (March 1999)
Rocksalt Sandbox [PLDI 2012]
1M instructions/second; faster than Google's checker
Nucleus Allocator/Garbage Collector [PLDI 2010]
“competitive performance on macro-benchmarks when compared to native garbage collection.”
QUARK Web Browser [USENIX 2012]
24% overhead wrt WebKit baseline on the top 10 Alexa Web sites
Verified code is not intrinsically slower, but verifying faster code can be more time consuming.
Time to produce a proof can be serious impediment to adoption.
Facebook's INFER sound static analyzer processes millions of lines of code and thousands of diffs per day.
4 hours for full Android/iOS code base
<10 minutes on average for single diffs

But, proves only the absence of null pointer exceptions and resource leaks.
The Fine Print
All proofs come with assumptions.
Violate those assumptions and all bets are off.
John Regehr et al found 325 bugs in various C compilers,
including CompCert
[PLDI 2011].
(Many of the artifacts we've considered lack features.)
Don't verify existing code artifacts
seL4, CompCert, FSCQ, certiKOS, Rocksalt, Nucleus, QUARK
Use static analyzers to eliminate obvious bugs before starting formal verification.
Don't verify all code:
Secure essential infrastructure & contain the rest.
QUARK, Verve/Nucleus, Rocksalt
Use DSLs to generate code and correctness proofs
Rocksalt, Ivory/Tower, SpiralGen, BilbyS
Composition enables scaling
Facebook INFER; UC-KLEE, Rockwell Collins Workbench; mCertiKOS
Automation is essential:
Tactic libraries and SMT/SAT solver integration
FSCQ, Nucleus, mCertiKOS
Source: Finding and Understanding Bugs in C Compilers, PLDI 2011
Source: Moving Fast with Software Verification, NASA Formal Method Symposium, 2015
Producing and validating models of real systems
x86, LLVM, Linux, Browser APIs, POSIX interfaces
Increasing automation
Proof engineering
Integrating with normal development processes
Getting buy-in/adoption & training
"Exhaustively testable pseudo-code"
Using Formal Methods at Amazon Web Services
Handling concurrency
And attackers take control with distressing ease.
Formal Methods:
Not just for implementation bugs!
Formal methods can help with other security challenges as well:
Faulty design
Ex: Amazon Web Services use of TLA+
Buggy specifications
Ex: Rockwell Collins detecting unencrypted comm channel
Side-channel information leaks
Ex: NICTA analysis of seL4
Dependence on 3rd party software
Enabling the masses to launch pernicious attacks at scale.
and essentially all computers are networked.
Phoenix Exploit Kit, 2010
"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."
CompCert bugs were in:
the unverified front end (subsequently fixed & verified)
a hardware model
All verified to be functionally correct!
CompCert Verifying C Compiler
Xavier Leroy, Formal certification of a compiler back-end, POPL 2006
Subset of C used by aviation industry
Implemented and proven correct in Coq.
Size: 42K LoC+P
Time to build: 3 person years
Speed: 2x speed of gcc -O0,
7% slower than gcc -O1,
12% slower than gcc -O2
Poised to become the compiler for Airbus software.
seL4 Microkernel
General purpose, operating system microkernel.
Implemented and proven correct in Isabelle/HOL.
Size: 10K LoC, 480K LoP
Time to build: 13 (8) person years
Speed: 206 vs 227 cycles in 1-way IPC fastpath
Machine-checked theorems include
Access-control enforcement
Compilation to binary
IPC fast-path correctness
Available open source.
Comprehensive Formal Verification of an OS Microkernel, ACM Transactions on Computer Systems, February 2014.
John Launchbury
Gerwin Klein
Gary McGraw
Greg Morrisett
Aaron Tomb
Mike Walker
Thanks to:
Full transcript