module Intro where
dummy :: Int
dummy = 7
Liquid Haskell:
Verification of Haskell Code
Niki Vazou
(University of Maryland)
Haskell is SAFE!
Fact Check: Buffer Overflows
λ> :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"
Goal: Extend Type System
To prevent wider class of errors
To enforce program specific properties
Plan
Installation & Resources
Online Server: http://goto.ucsd.edu:8090/index.html
cabal install liquidhaskellFrom 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