LiquidHaskell:

Verification of Haskell Code with SMTs

Niki Vazou

(UC San Diego)



Follow online http://goto.ucsd.edu/~nvazou/presentations/cufp16/01-index.html










LiquidHaskell: Verification of Haskell with SMTs




Motivation: Why verification?





















Well-Typed Programs Can Go Wrong























The Heartbleed Bug.

Heartbleed is a security bug in the OpenSSL cryptography library (April 2014).

The HEartbleed Bug.





















The Heartbleed Bug in Haskell

λ> :m +Data.Text Data.Text.Unsafe
λ> let text = pack "Niki"
λ> :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 6 extra characters...
λ>  takeWord16 10 text
"Niki\33624\5479\SOH\NUL\60480\5115"











Partial Functions

λ> :t head
head :: [a] -> a

λ> head "CUFP"
'C'


λ> head []
*** Exception: Prelude.head: empty list













Functional Correctness


λ> fib 1 <= fib 42
False
λ> mapReduce 42 sum (+) [1..20]
0 













Goal: Extend Type System



  • To prevent wider class of errors

  • To enforce program specific properties













Plan


Follow online http://goto.ucsd.edu/~nvazou/presentations/cufp16/01-index.html


  1. Refinements Types
  2. Data Types
  3. Termination
  4. Reflection
  5. Structural Induction
  6. Case Study: MapReduce














Evaluation


  • Diverse Code Bases

  • 10KLoc / 56 Modules

  • Memory Safety, Termination, Functional Correctness


Inference is Crucial










Evaluation

  • Specifications: 1 / 10 LOC (ok)

  • Compile Time: 1s / 10 LOC (not ok!)









Conclusion


Refinement Types: Automated Dependent Typing via SMT


Properties: Predicates + Types
Proofs: SMT Solvers + Subtyping
Inference: Abstract Interpretation + Hindley-Milner













Thank You!



cabal install liquidhaskell
http://www.refinement-types.org
online demo @ http://goto.ucsd.edu/liquidhaskell