Liquid Haskell:
Verification of Haskell Code

Niki Vazou

(University of Maryland)




http://goto.ucsd.edu/~nvazou/presentations/shonan17/01-index.html










Liquid Haskell: Verification of Haskell Code




Motivation: Why verification?





















Software bugs are Everywhere

“Airbus A400M crashed due to a software bug.”

— May 2015

Plane























Software bugs are Everywhere

“Heartbleed: a security bug in the OpenSSL cryptography library.”

— April 2014

The Heartbleed Bug.























How The Heartbleed Bug Works

How The Heartbleed Bug Works





















Goal: Make Bugs Difficult to Express



Using Modern Programming Languages (e.g., Haskell, Scala, Ocaml, F#).



Because of Strong Types & Lambda Calculus.

















Via compile-time sanity checks

Lambda Man.























Fact Check: Haskell VS. Heartbleed

Haskell vs Heartbleed























The Heartbleed Bug in Haskell

λ> :m +Data.Text Data.Text.Unsafe
λ> let text = pack "hat"
λ> :t takeWord16
    takeWord16 :: Int -> Text -> Text





















True is a bad argument

λ> takeWord16 True text

<interactive>:5:12:
    Couldn't match expected type ‘Int’ with actual type ‘Bool’
    In the first argument of ‘takeWord16’, namely ‘True’
    In the expression: takeWord16 True text






But, 10 is a good argument


Reveal 7 extra characters... 
λ>  takeWord16 10 text
"hat\33624\5479\SOH\NUL\60480\5115\5479"











More Bugs: Program Equivalence


λ> sum  [1..1000]
500500

λ> psum [1..1000]
0













More Bugs: Information Flow


λ> do {submitPaper;  ask "Who else submitted?"}

Current Submissions:
1. N. Vazou et. al. Liquid Things 
2. ...













Goal: Extend Type System



  • To prevent wider class of errors

  • To enforce program specific properties













Plan


  1. Refinements Types
  2. Data Types
  3. Termination
  4. Refinement Reflection
  5. Case Study: Verification MapReduce
  6. Information Flow Security Policies