Fact Check: Haskell VS. Heartbleed

How The Heartbleed Bug Works

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

λ>  takeWord16 10 text
"HAT\33624\5479\SOH\NUL\60480\5115\3267"

More Bugs: Partial Functions

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

λ> head "Hawai'i"
'H'

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

More Bugs: Termination

λ> fib 4
5

λ> fib 42
...

Goal: Extend Type System

• To prevent wider class of errors

• To enforce program specific properties

Plan

1. Refinements Types
2. Data Types
3. Termination

Recap

1. Refinements: Types + Predicates
2. Subtyping: SMT Implication
3. Measures: Specify Properties of Data
4. Termination: Use Logic to Prove Termination
   
   
   
   
   
   
   
   
   
   
   
   

Evaluation

• Diverse Code Bases

• 20KLoc

• Memory Safety, Termination, Functional Correctness, Program Equivalence

• Specifications: 1 / 10 LOC

Conclusion

Liquid Types: Automated Verification via SMT

Thank You!

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

http://www.refinement-types.org

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