Liquid Haskell:
Verification of Haskell Code


Niki Vazou
(University of Maryland)

Liquid Haskell: Verification of Haskell Code


Motivation: Why verification?

Liquid Haskell: Verification of Haskell Code


Motivation: Why verification?

In class motivation: programs may diverge or crash.

*** Exception: Prelude.head: empty list


But the goal is more ambitious ...

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

How The Heartbleed Bug Works

How The Heartbleed Bug Works

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 :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: Functional Correctness


λ> sort [4,3,2,1] [4,3,2,1]

More Bugs: Program Equivalence


λ> sum [1..1000] 500500 λ> psum [1..1000] 0

Goal: Extend Type System


  • To prevent wider class of errors

  • To enforce program specific properties

Plan



Coming up:

  • 4. Termination
  • 5. Proving Laws
  • 6. Natural Deduction

Installation & Resources