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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

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

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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

`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
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

But, `10` is a good argument

Reveal 7 extra characters...

λ>  takeWord16 10 text
"hat\33624\5479\SOH\NUL\60480\5115\5479"
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX

More Bugs: Functional Correctness

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

More Bugs: Program Equivalence

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

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

Online Server: http://goto.ucsd.edu:8090/index.html
cabal install liquidhaskell
From github
Further Reading: Blog, Manual, Github.

Recap

Refinements: Types + Predicates
Subtyping: SMT Implication
Measures: Specify Properties of Data
Termination: Use Logic to Prove Termination

Evaluation

Diverse Code Bases
20KLoc
Memory Safety, Termination, Functional Correctness, Program Equivalence
Specifications: 1 / 10 LOC

Evaluation

Library	LOC	Specs	Time
`XMonad.StackSet`	256	74	27s
`Data.List`	814	46	26s
`Data.Set.Splay`	149	27	27s
`Data.Vector.Algorithms`	1219	76	89s
`HsColour`	1047	19	196s
`Data.Map.Base`	1396	125	174s
`Data.Text`	3128	305	499s
`Data.Bytestring`	3505	307	294s
Total	11512	977	1336s

Conclusion

Liquid Types: Automated Verification via SMT

Properties:	Predicates + Types
Proofs:	SMT Solvers + Subtyping

Thank You!

https://github.com/ucsd-progsys/liquidhaskell

http://www.refinement-types.org

online demo @ http://goto.ucsd.edu/liquidhaskell

Liquid Haskell: Verification of Haskell Code

Niki Vazou (University of Maryland)

Liquid Haskell: Verification of Haskell Code

Liquid Haskell: Verification of Haskell Code

Software bugs are Everywhere

Software bugs are Everywhere

How The Heartbleed Bug Works

How The Heartbleed Bug Works

How The Heartbleed Bug Works

Goal: Make Bugs Difficult to Express

Via compile-time sanity checks

Fact Check: Haskell VS. Heartbleed

The Heartbleed Bug in Haskell

True is a bad argument

But, 10 is a good argument

More Bugs: Functional Correctness

More Bugs: Program Equivalence

Goal: Extend Type System

Plan

Installation & Resources

Recap

Evaluation

Evaluation

Conclusion

Thank You!

Liquid Haskell:
Verification of Haskell Code

Niki Vazou
(University of Maryland)

`True` is a bad argument

But, `10` is a good argument