liquidhaskell-0.7.0.0: docs/blog/2014-05-28-pointers-gone-wild.lhs
---
layout: post
title: "Pointers Gone Wild"
date: 2014-05-28
comments: true
external-url:
author: Eric Seidel
published: true
categories: benchmarks, text
demo: TextInternal.hs
---
A large part of the allure of Haskell is its elegant, high-level ADTs
that ensure[^compilercorrectness] that programs won't be plagued by problems
like the infamous [SSL heartbleed bug](http://en.wikipedia.org/wiki/Heartbleed).
[^compilercorrectness]: Assuming the absence of errors in the compiler and run-time...
However, another part of Haskell's charm is that when you really really
need to, you can drop down to low-level pointer twiddling to squeeze the
most performance out of your machine. But of course, that opens the door
to the #heartbleeds.
Can we have have our cake and eat it too?
Can we twiddle pointers and still get the nice safety assurances of high-level types?
<!-- more -->
To understand the potential for potential bleeding,
let's study the popular `text` library for efficient
text processing. The library provides the high-level
API Haskellers have come to expect while using stream
fusion and byte arrays under the hood to guarantee
high performance.
Suppose we wanted to get the *i*th `Char` of a `Text`,
\begin{code} we could write a function[^bad]
charAt (Text a o l) i = word2char $ unsafeIndex a (o+i)
where
word2char = chr . fromIntegral
\end{code}
which extracts the underlying array `a`, indexes into it starting
at the offset `o` and casts the `Word16` to a `Char`, using
functions exported by `text`.
[^bad]: This function is bad for numerous reasons, least of which is that `Data.Text.index` is already provided, but stay with us...
\begin{code}Let's try this out in GHCi.
ghci> let t = pack ['d','o','g']
ghci> charAt t 0
'd'
ghci> charAt t 2
'g'
\end{code}
\begin{code}Looks good so far, what happens if we keep going?
ghci> charAt t 3
'\NUL'
ghci> charAt t 100
'\8745'
\end{code}
Oh dear, not only did we not get any sort of exception from Haskell,
we weren't even stopped by the OS with a segfault. This is quite
dangerous since we have no idea what sort of data we just read!
To be fair to the library's authors, we did use a function that
was clearly branded `unsafe`, but these functions, while not
intended for *clients*, pervade the implementation of the *library*.
Wouldn't it be nice to have these last two calls *rejected at compile time*?
In this post we'll see exactly how prevent invalid memory accesses
like this with LiquidHaskell.
<div class="hidden">
\begin{code}
{-# LANGUAGE BangPatterns, MagicHash, Rank2Types,
RecordWildCards, UnboxedTuples, ExistentialQuantification #-}
{-@ LIQUID "--no-termination" @-}
module TextInternal (test, goodMain, badMain, charAt, charAt') where
import qualified Control.Exception as Ex
import Control.Applicative ((<$>))
import Control.Monad (when)
import Control.Monad.ST.Unsafe (unsafeIOToST)
import Data.Bits (shiftR, xor, (.&.))
import Data.Char
import Foreign.C.Types (CSize)
import GHC.Base (Int(..), ByteArray#, MutableByteArray#, newByteArray#,
writeWord16Array#, indexWord16Array#, unsafeCoerce#, ord,
iShiftL#)
import GHC.ST (ST(..), runST)
import GHC.Word (Word16(..))
import qualified Data.Text.Lazy.IO as TIO
import qualified Data.Text as T
import qualified Data.Text.Internal as T
import Language.Haskell.Liquid.Prelude
{-@ aLen :: a:Array -> {v:Nat | v = (aLen a)} @-}
{-@ maLen :: a:MArray s -> {v:Nat | v = (maLen a)} @-}
new :: forall s. Int -> ST s (MArray s)
unsafeWrite :: MArray s -> Int -> Word16 -> ST s ()
unsafeFreeze :: MArray s -> ST s Array
unsafeIndex :: Array -> Int -> Word16
copyM :: MArray s -- ^ Destination
-> Int -- ^ Destination offset
-> MArray s -- ^ Source
-> Int -- ^ Source offset
-> Int -- ^ Count
-> ST s ()
{-@ memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO () @-}
memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO ()
memcpyM = undefined
--------------------------------------------------------------------------------
--- Helper Code
--------------------------------------------------------------------------------
{-@ shiftL :: i:Nat -> n:Nat -> {v:Nat | ((n = 1) => (v = (i * 2)))} @-}
shiftL :: Int -> Int -> Int
shiftL = undefined -- (I# x#) (I# i#) = I# (x# `iShiftL#` i#)
pack :: String -> Text
pack = undefined -- not "actually" using
assert b a = Ex.assert b a
data Text = Text Array Int Int
{-@ tLength :: t:Text -> {v:_ | v = (tLen t)} @-}
tLength (Text _ _ n) = n
\end{code}
</div>
The `Text` Lifecycle
--------------------
`text` splits the reading and writing array operations between two
types of arrays, immutable `Array`s and mutable `MArray`s. This leads to
the following general lifecycle:
The main four array operations we care about are:
1. **creating** an `MArray`,
2. **writing** into an `MArray`,
3. **freezing** an `MArray` into an `Array`, and
4. **reading** from an `Array`.
Creating an `MArray`
--------------------
The (mutable) `MArray` is a thin wrapper around GHC's primitive
`MutableByteArray#`, additionally carrying the number of `Word16`s it
can store.
\begin{code}
data MArray s = MArray { maBA :: MutableByteArray# s
, maLen :: !Int
}
\end{code}
It doesn't make any sense to have a negative length, so we *refine*
the data definition to require that `maLen` be non-negative.
\begin{code}
{-@ data MArray s = MArray { maBA :: MutableByteArray# s
, maLen :: Nat
}
@-}
\end{code}
\begin{code} As an added bonus, the above specification generates **field-accessor measures** that we will use inside the refined types:
{-@ measure maLen :: MArray s -> Int
maLen (MArray a l) = l
@-}
\end{code}
We can use these accessor measures to define `MArray`s of size `N`:
\begin{code}
{-@ type MArrayN a N = {v:MArray a | (maLen v) = N} @-}
\end{code}
and we can use the above alias, to write a type that tracks the size
of an `MArray` at the point where it is created:
\begin{code}
{-@ new :: forall s. n:Nat -> ST s (MArrayN s n) @-}
new n
| n < 0 || n .&. highBit /= 0 = error "size overflow"
| otherwise = ST $ \s1# ->
case newByteArray# len# s1# of
(# s2#, marr# #) -> (# s2#, MArray marr# n #)
where !(I# len#) = bytesInArray n
highBit = maxBound `xor` (maxBound `shiftR` 1)
bytesInArray n = n `shiftL` 1
\end{code}
`new n` is an `ST` action that produces an `MArray s` with `n` slots each
of which is 2 bytes (as internally `text` manipulates `Word16`s).
The verification process here is quite simple; LH recognizes that
the `n` used to construct the returned array (`MArray marr# n`)
the same `n` passed to `new`.
Writing into an `MArray`
------------------------
Once we have *created* an `MArray`, we'll want to write our data into it.
A `Nat` is a valid index into an `MArray` if it is *strictly less than*
the size of the array.
\begin{code}
{-@ type MAValidI MA = {v:Nat | v < (maLen MA)} @-}
\end{code}
We use this valid index alias to refine the type of `unsafeWrite`
\begin{code}
{-@ unsafeWrite :: ma:MArray s -> MAValidI ma -> Word16 -> ST s () @-}
unsafeWrite MArray{..} i@(I# i#) (W16# e#)
| i < 0 || i >= maLen = assert False $ error "out of bounds"
| otherwise = ST $ \s1# ->
case writeWord16Array# maBA i# e# s1# of
s2# -> (# s2#, () #)
\end{code}
Note that, when compiled with appropriate options, the implementation of
`text` checks the bounds at run-time. However, LiquidHaskell can statically
prove that the error branch is unreachable, i.e. the `assert` **cannot fail**
(as long as the inputs adhere to the given specification) by giving `assert`
the type:
\begin{code}
{-@ assert assert :: {v:Bool | (Prop v)} -> a -> a @-}
\end{code}
Bulk Writing into an `MArray`
-----------------------------
So now we can write individual `Word16`s into an array, but maybe we
have a whole bunch of text we want to dump into the array. Remember,
`text` is supposed to be fast! C has `memcpy` for cases like this but
it's notoriously unsafe; with the right type however, we can regain safety.
`text` provides a wrapper around `memcpy` to copy `n` elements from
one `MArray` to another.
`copyM` requires two `MArray`s and valid offsets into each -- note
that a valid offset is **not** necessarily a valid *index*, it may
be one element out-of-bounds
\begin{code}
{-@ type MAValidO MA = {v:Nat | v <= (maLen MA)} @-}
\end{code}
-- and a `count` of elements to copy.
The `count` must represent a valid region in each `MArray`, in
other words `offset + count <= length` must hold for each array.
\begin{code}
{-@ copyM :: dest:MArray s
-> didx:MAValidO dest
-> src:MArray s
-> sidx:MAValidO src
-> {v:Nat | (((didx + v) <= (maLen dest))
&& ((sidx + v) <= (maLen src)))}
-> ST s ()
@-}
copyM dest didx src sidx count
| count <= 0 = return ()
| otherwise =
assert (sidx + count <= maLen src) .
assert (didx + count <= maLen dest) .
unsafeIOToST $ memcpyM (maBA dest) (fromIntegral didx)
(maBA src) (fromIntegral sidx)
(fromIntegral count)
\end{code}
Again, the two `assert`s in the function were in the original code as
(optionally compiled out) run-time checks of the precondition, but with
LiquidHaskell we can actually *prove* that the `assert`s **always succeed**.
Freezing an `MArray` into an `Array`
------------------------------------
Before we can package up our `MArray` into a `Text`, we need to
*freeze* it, preventing any further mutation. The key property
here is of course that the frozen `Array` should have the same
length as the `MArray`.
Just as `MArray` wraps a mutable array, `Array` wraps an *immutable*
`ByteArray#` and carries its length in `Word16`s.
\begin{code}
data Array = Array { aBA :: ByteArray#
, aLen :: !Int
}
\end{code}
As before, we get free accessor measures `aBA` and `aLen` just by
refining the data definition
\begin{code}
{-@ data Array = Array { aBA :: ByteArray#
, aLen :: Nat
}
@-}
\end{code}
so we can refer to the components of an `Array` in our refinements.
Using these measures, we can define
\begin{code}
{-@ type ArrayN N = {v:Array | (aLen v) = N} @-}
{-@ unsafeFreeze :: ma:MArray s -> ST s (ArrayN (maLen ma)) @-}
unsafeFreeze MArray{..} = ST $ \s# ->
(# s#, Array (unsafeCoerce# maBA) maLen #)
\end{code}
Again, LiquidHaskell is happy to prove our specification as we simply
copy the length parameter `maLen` over into the `Array`.
Reading from an `Array`
------------------------
Finally, we will eventually want to read a value out of the
`Array`. As with `unsafeWrite` we require a valid index into the
`Array`, which we denote using the `AValidI` alias.
\begin{code}
{-@ type AValidI A = {v:Nat | v < (aLen A)} @-}
{-@ unsafeIndex :: a:Array -> AValidI a -> Word16 @-}
unsafeIndex Array{..} i@(I# i#)
| i < 0 || i >= aLen = assert False $ error "out of bounds"
| otherwise = case indexWord16Array# aBA i# of
r# -> (W16# r#)
\end{code}
As before, LiquidHaskell can easily prove that the error branch
is unreachable, i.e. is *never* executed at run-time.
Wrapping it all up
------------------
Now we can finally define the core datatype of the `text` package!
A `Text` value consists of three fields:
A. an `Array`,
B. an `Int` offset into the *middle* of the array, and
C. an `Int` length denoting the number of valid indices *after* the offset.
We can specify the invariants for fields (b) and (c) with the refined type:
\begin{code}
{-@ data Text
= Text { tArr :: Array
, tOff :: {v:Nat | v <= (aLen tArr)}
, tLen :: {v:Nat | v+tOff <= (aLen tArr)}
}
@-}
\end{code}
These invariants ensure that any *index* we pick between `tOff` and
`tOff + tLen` will be a valid index into `tArr`.
As shown above with `new`, `unsafeWrite`, and `unsafeFreeze`, we can type the
top-level function that creates a `Text` from a `[Char]` as:
\begin{code}
{-@ pack :: s:String -> {v:Text | (tLen v) = (len s)} @-}
\end{code}
Preventing Bleeds
-----------------
Now, let us close the circle and return to potentially *bleeding* function:
\begin{code}
charAt' (Text a o l) i = word2char $ unsafeIndex a (o+i)
where
word2char = chr . fromIntegral
\end{code}
Aha! LiquidHaskell flags the call to `unsafeIndex` because of course, `i` may fall
outside the bounds of the given array `a`! We can remedy that by specifying
a bound for the index:
\begin{code}
{-@ charAt :: t:Text -> {v:Nat | v < (tLen t)} -> Char @-}
charAt (Text a o l) i = word2char $ unsafeIndex a (o+i)
where
word2char = chr . fromIntegral
\end{code}
That is, we can access the `i`th `Char` as long as `i` is a `Nat` less
than the the size of the text, namely `tLen t`. Now LiquidHaskell is convinced
that the call to `unsafeIndex` is safe, but of course, we have passed
the burden of proof onto users of `charAt`.
Now, if we try calling `charAt` as we did at the beginning
\begin{code}
test = [good,bad]
where
dog = ['d','o','g']
good = charAt (pack dog) 2
bad = charAt (pack dog) 3
\end{code}
we see that LiquidHaskell verifies the `good` call, but flags `bad` as
**unsafe**.
Enforcing Sanitization
----------------------
EDIT: As several folks have pointed out, the #heartbleed error was
due to inputs not being properly sanitized. The above approach
**ensures, at compile time**, that proper sanitization has been
performed.
To see this in action, lets write a little function that just shows the
character at a given position:
\begin{code}
{-@ showCharAt :: t:_ -> {v:Nat | v < (tLen t)} -> _ @-}
showCharAt t i = putStrLn $ show $ charAt t i
\end{code}
Now, the following function, that correctly sanitizes is **accepted**
\begin{code}
goodMain :: IO ()
goodMain
= do txt <- pack <$> getLine
i <- readLn
if 0 <= i && i < tLength txt
then showCharAt txt i
else putStrLn "Bad Input!"
\end{code}
but this function, which has insufficient sanitization, is **rejected**
\begin{code}
badMain :: IO ()
badMain
= do txt <- pack <$> getLine
i <- readLn
if 0 <= i
then showCharAt txt i
else putStrLn "Bad Input!"
\end{code}
Thus, we can use LiquidHaskell to block, at compile time, any serious bleeding
from pointers gone wild.