Case Study: Low Level Memory
============================

 {#mem}
-------

<div class="hidden">

\begin{code}
{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--short-names"    @-}
{-@ LIQUID "--diffcheck"     @-}
{-# LANGUAGE ForeignFunctionInterface #-}

module Memory where

import Prelude hiding (null)
import Data.Char
import Data.Word
import Foreign.C.Types
import Foreign.ForeignPtr
import Foreign.Ptr
import Foreign.Storable
import System.IO.Unsafe
import Data.ByteString.Internal (c2w, w2c)
import Language.Haskell.Liquid.Prelude
\end{code}

</div>

"HeartBleed" in Haskell
-----------------------

<br>

**Modern languages are built on top of C**

<br>

<div class="fragment">
Implementation errors could open up vulnerabilities
</div>




"HeartBleed" in Haskell (1/3)
-----------------------------

**A String Truncation Function**

<br>

<div class="hidden">
\begin{spec}
import Data.ByteString.Char8  (pack, unpack)
import Data.ByteString.Unsafe (unsafeTake)
\end{spec}
</div>

\begin{spec}
chop     :: String -> Int -> String
chop s n = s'
  where
    b    = pack s         -- down to low-level
    b'   = unsafeTake n b -- grab n chars
    s'   = unpack b'      -- up to high-level
\end{spec}

"HeartBleed" in Haskell (2/3)
-----------------------------

<img src="../img/overflow.png" height=100px>


Works if you use the **valid prefix** size

<br>

\begin{spec}
λ> let ex = "Ranjit Loves Burritos"

λ> heartBleed ex 10
"Ranjit Lov"
\end{spec}


"HeartBleed" in Haskell (3/3)
-----------------------------

<img src="../img/overflow.png" height=100px>

Leaks *overflow buffer* if **invalid prefix** size!

<br>

\begin{spec}
λ> let ex = "Ranjit Loves Burritos"

λ> heartBleed ex 30
"Ranjit Loves Burritos\NUL\201\&1j\DC3\SOH\NUL"
\end{spec}

Types Against Overflows
-----------------------

<br>

**Strategy: Specify and Verify Types for**

<br>

1. <div class="fragment">Low-level `Pointer` API</div>
2. <div class="fragment">Lib-level `ByteString` API</div>
3. <div class="fragment">User-level `Application` API</div>

<br>

<div class="fragment">Errors at *each* level are prevented by types at *lower* levels</div>

 {#ptr}
=======

1. Low-level Pointer API
------------------------

<br>

Strategy: Specify and Verify Types for

<br>

1. **Low-level `Pointer` API**
2. Lib-level `ByteString` API
3. User-level `Application` API

<br>

Errors at *each* level are prevented by types at *lower* levels




1. Low-Level Pointer API
========================

API: Types
----------

<br>

**Low-level Pointers**

\begin{spec}
data Ptr a
\end{spec}

<br>

<div class="fragment">
**Foreign Pointers**

\begin{spec}
data ForeignPtr a
\end{spec}

<br>

`ForeignPtr` wraps around `Ptr`; can be exported to/from C.
</div>


API: Operations (1/2)
---------------------

<div class="fragment">
**Read**

\begin{spec}
peek     :: Ptr a -> IO a
\end{spec}
</div>

<br>
<div class="fragment">
**Write**

\begin{spec}
poke     :: Ptr a -> a -> IO ()
\end{spec}
</div>

<br>

<div class="fragment">
**Arithmetic**
\begin{spec}
plusPtr  :: Ptr a -> Int -> Ptr b
\end{spec}
</div>

API: Operations (2/2)
---------------------

<div class="fragment">
**Create**

\begin{spec}
malloc  :: Int -> ForeignPtr a
\end{spec}
</div>

<br>

<div class="fragment">
**Unwrap and Use**

\begin{spec}
withForeignPtr :: ForeignPtr a     -- pointer
               -> (Ptr a -> IO b)  -- action
               -> IO b             -- result
\end{spec}
</div>

Example
-------

**Allocate a block and write 4 zeros into it**

<div class="fragment">

\begin{code}
zero4 = do fp <- malloc 4
           withForeignPtr fp $ \p -> do
             poke (p `plusPtr` 0) zero
             poke (p `plusPtr` 1) zero
             poke (p `plusPtr` 2) zero
             poke (p `plusPtr` 3) zero
           return fp
        where
           zero = 0 :: Word8
\end{code}

</div>

Example
-------

**Allocate a block and write 4 zeros into it**

How to *prevent overflows* e.g. writing 5 or 50 zeros?

<br>

<div class="fragment">
**Step 1**

*Refine pointers* with allocated size
</div>

<br>

<div class="fragment">
**Step 2**

*Track sizes* in pointer operations
</div>

Refined API: Types
------------------

<br>

**1. Refine pointers with allocated size**

\begin{spec}
measure plen  :: Ptr a -> Int
measure fplen :: ForeignPtr a -> Int
\end{spec}

<br>

<div class="fragment">
Abbreviations for pointers of size `N`

\begin{spec}
type PtrN a N        = {v:_ |  plen v  = N}
type ForeignPtrN a N = {v:_ |  fplen v = N}
\end{spec}
</div>


Refined API: Ops (1/3)
----------------------

<div class="fragment">
**Create**

\begin{spec}
malloc  :: n:Nat -> ForeignPtrN a n
\end{spec}
</div>

<br>

<div class="fragment">
**Unwrap and Use**

\begin{spec}
withForeignPtr :: fp:ForeignPtr a
               -> (PtrN a (fplen fp) -> IO b)
               -> IO b
\end{spec}
</div>

Refined API: Ops (2/3)
----------------------

<br>

**Arithmetic**

Refine type to track *remaining* buffer size

<br>

<div class="fragment">
\begin{spec}
plusPtr :: p:Ptr a
        -> o:{Nat|o <= plen p}   -- in bounds
        -> PtrN b (plen b - o)   -- remainder
\end{spec}

</div>



Refined API: Ops (3/3)
----------------------

**Read & Write require non-empty remaining buffer**

<br>

<div class="fragment">
**Read**

\begin{spec}
peek :: {v:Ptr a | 0 < plen v} -> IO a
\end{spec}
</div>

<br>
<div class="fragment">
**Write**

\begin{spec}
poke :: {v:Ptr a | 0 < plen v} -> a -> IO ()
\end{spec}
</div>

Example: Overflow Prevented
---------------------------

How to *prevent overflows* e.g. writing 5 or 50 zeros?

<br>

<div class="fragment">

\begin{code}
exBad = do fp <- malloc 4
           withForeignPtr fp $ \p -> do
             poke (p `plusPtr` 0) zero
             poke (p `plusPtr` 1) zero
             poke (p `plusPtr` 2) zero
             poke (p `plusPtr` 5) zero
           return fp
        where
           zero = 0 :: Word8
\end{code}

</div>

 {#bs}
======

2. ByteString API
-----------------

<br>

Strategy: Specify and Verify Types for

<br>

1. Low-level `Pointer` API
2. **Lib-level `ByteString` API**
3. User-level `Application` API

<br>

Errors at *each* level are prevented by types at *lower* levels


2. ByteString API
=================

Type
-------

<img src="../img/bytestring.png" height=150px>

\begin{code}
data ByteString = PS {
    bPtr :: ForeignPtr Word8
  , bOff :: !Int
  , bLen :: !Int
  }
\end{code}


Refined Type
------------

<img src="../img/bytestring.png" height=150px>

\begin{code}
{-@ data ByteString = PS {
      bPtr :: ForeignPtr Word8
    , bOff :: {v:Nat| v        <= fplen bPtr}
    , bLen :: {v:Nat| v + bOff <= fplen bPtr}
    }                                       @-}
\end{code}

Refined Type
------------

<img src="../img/bytestring.png" height=150px>

<br>

**A Useful Abbreviation**

\begin{spec}
type ByteStringN N = {v:ByteString| bLen v = N}
\end{spec}


<div class="hidden">
\begin{code}
{-@ type ByteStringN N = {v:ByteString | bLen v = N} @-}
\end{code}
</div>



Legal Bytestrings
-----------------


<br>

\begin{code}
{-@ good1 :: IO (ByteStringN 5) @-}
good1 = do fp <- malloc 5
           return (PS fp 0 5)

{-@ good2 :: IO (ByteStringN 3) @-}
good2 = do fp <- malloc 5
           return (PS fp 2 3)
\end{code}

<br>

<div class="fragment">
**Note:** *length* of `good2` is `3` which is *less than* allocated size `5`
</div>

Illegal Bytestrings
-----------------

<br>

\begin{code}
bad1 = do fp <- malloc 3
          return (PS fp 0 10)

bad2 = do fp <- malloc 3
          return (PS fp 2 2)
\end{code}

<br>

<div class="fragment">
Claimed length *exceeds* allocation ... **rejected** at compile time
</div>

API: `create`
-------------

<div class="hidden">
\begin{code}
create :: Int -> (Ptr Word8 -> IO ()) -> ByteString
\end{code}
</div>

*Allocate* and *fill* a `ByteString`

<br>

<div class="fragment">
**Specification**
\begin{code}
{-@ create :: n:Nat -> (PtrN Word8 n -> IO ())
           -> ByteStringN n                @-}
\end{code}
</div>


<div class="fragment">
**Implementation**

\begin{code}
create n fill = unsafePerformIO $ do
  fp  <- malloc n
  withForeignPtr fp fill
  return (PS fp 0 n)
\end{code}
</div>

<!-- CUT
<div class="fragment">
Yikes, there is an error! How to fix?
</div>
-->

API: `pack`
------------

**Specification**

\begin{code}
{-@ pack :: s:String -> ByteStringN (len s) @-}
\end{code}

<br>

<div class="fragment">

**Implementation**

\begin{code}
pack str      = create n $ \p -> go p xs
  where
  n           = length str
  xs          = map c2w str
  go p (x:xs) = poke p x >> go (plusPtr p 1) xs
  go _ []     = return  ()
\end{code}

</div>



API: `unsafeTake`
-----------------

Extract *prefix* string of size `n`

<br>

<div class="fragment">
**Specification**

\begin{code}
{-@ unsafeTake :: n:Nat
               -> b:{ByteString | n <= bLen b}
               -> ByteStringN n            @-}
\end{code}
</div>


<br>

<div class="fragment">
**Implementation**

\begin{code}
unsafeTake n (PS x s l) = PS x s n
\end{code}
</div>

API: `unpack`
-------------

**Specification**

\begin{spec}
unpack
 :: b:ByteString -> StringN (bLen b)
\end{spec}

<br>

<div class="fragment">
**Implementation**

\begin{spec}
unpack b = you . get . the . idea -- see source
\end{spec}
</div>

<div class="hidden">
\begin{code}
{-@ qualif Unpack(v:a, acc:b, n:int) : len v = 1 + n + len acc @-}

{-@ unpack :: b:ByteString -> StringN (bLen b) @-}
unpack :: ByteString -> String
unpack (PS _  _ 0)  = []
unpack (PS ps s l)  = unsafePerformIO $ withForeignPtr ps $ \p ->
   go (p `plusPtr` s) (l - 1)  []
  where
   go p 0 acc = peek p >>= \e -> return (w2c e : acc)
   go p n acc = peek (p `plusPtr` n) >>=   \e -> go p (n-1) (w2c e : acc)
\end{code}

</div>

 {#heartbleedredux}
==================


3. Application API
-------------------


<br>

Strategy: Specify and Verify Types for

<br>

1. Low-level `Pointer` API
2. Lib-level `ByteString` API
3. **User-level `Application` API**

<br>

Errors at *each* level are prevented by types at *lower* levels

3. Application API
==================

Revisit "HeartBleed"
--------------------

Lets revisit our potentially "bleeding" `chop`

<br>

<div class="hidden">
\begin{code}
{-@ type StringN N = {v:String | len v = N} @-}
\end{code}
</div>
<div class="fragment">

\begin{code}
{-@ chop :: s:String
         -> n:{Nat | n <= len s}
         -> StringN n
  @-}
chop s n =  s'
  where
    b    = pack s          -- down to low-level
    b'   = unsafeTake n b  -- grab n chars
    s'   = unpack b'       -- up to high-level
\end{code}

<!-- BEGIN CUT
<br>

Yikes! How shall we fix it?

     END CUT -->
</div>

<!-- BEGIN CUT

A Well Typed `chop`
-------------------

\begin{spec}
{-@ chop :: s:String
         -> n:{Nat | n <= len s}
         -> {v:String | len v = n} @-}
chop s n = s'
  where
    b    = pack s          -- down to low-level
    b'   = unsafeTake n b  -- grab n chars
    s'   = unpack b'       -- up to high-level
\end{spec}

END CUT -->

"HeartBleed" no more
--------------------

<br>

\begin{code}
demo     = [ex6, ex30]
  where
    ex   = ['N','o','r','m','a','n']
    ex6  = chop ex 6  -- ok
    ex30 = chop ex 30  -- out of bounds
\end{code}

<br>

"Bleeding" `chop ex 30` *rejected* by compiler

Recap: Types vs Overflows
-------------------------

<br>

**Strategy: Specify and Verify Types for**

<br>

1. Low-level `Pointer` API
2. Lib-level `ByteString` API
3. User-level `Application` API

<br>

**Errors at *each* level are prevented by types at *lower* levels**













<div class="hidden">
Bonus Material
==============

Nested ByteStrings
------------------

For a more in depth example, let's take a look at `group`,
which transforms strings like

   `"foobaaar"`

into *lists* of strings like

   `["f","oo", "b", "aaa", "r"]`.

The specification is that `group` should produce a list of `ByteStrings`

1. that are all *non-empty* (safety)
2. the sum of whose lengths is equal to the length of the input string (precision)

We use the type alias

\begin{code}
{-@ type ByteStringNE = {v:ByteString | bLen v > 0} @-}
\end{code}

to specify (safety) and introduce a new measure

\begin{code}
{-@ measure bLens  :: [ByteString] -> Int
    bLens ([])   = 0
    bLens (x:xs) = (bLen x + bLens xs)
  @-}
\end{code}

to specify (precision). The full type-specification looks like this:

\begin{code}
{-@ group :: b:ByteString -> {v: [ByteStringNE] | bLens v = bLen b} @-}
group xs
    | null xs   = []
    | otherwise = let y = unsafeHead xs
                      (ys, zs) = spanByte (unsafeHead xs) (unsafeTail xs)
                  in (y `cons` ys) : group zs
\end{code}

As you can probably tell, `spanByte` appears to be doing a lot of the work here,
so let's take a closer look at it to see why the post-condition holds.

\begin{code}
spanByte :: Word8 -> ByteString -> (ByteString, ByteString)
spanByte c ps@(PS x s l) = unsafePerformIO $ withForeignPtr x $ \p ->
    go (p `plusPtr` s) 0
  where
    go p i | i >= l    = return (ps, empty)
           | otherwise = do c' <- peekByteOff p i
                            if c /= c'
                                then return (unsafeTake i ps, unsafeDrop i ps)
                                else go p (i+1)
\end{code}

LiquidHaskell infers that `0 <= i <= l` and therefore that all of the memory
accesses are safe. Furthermore, due to the precise specifications given to
`unsafeTake` and `unsafeDrop`, it is able to prove that `spanByte` has the type

\begin{code}
{-@ spanByte :: Word8 -> b:ByteString -> (ByteStringPair b) @-}
\end{code}

where `ByteStringPair b` describes a pair of `ByteString`s whose
lengths sum to the length of `b`.

\begin{code}
{-@ type ByteStringPair B = (ByteString, ByteString)<{\x1 x2 ->
       bLen x1 + bLen x2 = bLen B}> @-}
\end{code}








\begin{code}
-----------------------------------------------------------------------
-- Helper Code
-----------------------------------------------------------------------

{-@ unsafeCreate :: l:Nat -> ((PtrN Word8 l) -> IO ()) -> (ByteStringN l) @-}
unsafeCreate n f = create n f -- unsafePerformIO $ create n f

{-@ invariant {v:ByteString   | bLen  v >= 0} @-}
{-@ invariant {v:[ByteString] | bLens v >= 0} @-}

{-@ qualif PLLen(v:a, p:b) : (len v) <= (plen p) @-}
{-@ qualif ForeignPtrN(v:ForeignPtr a, n:int): fplen v = n @-}
{-@ qualif FPLenPLen(v:Ptr a, fp:ForeignPtr a): fplen fp = plen v @-}
{-@ qualif PtrLen(v:Ptr a, xs:List b): plen v = len xs @-}
{-@ qualif PlenEq(v: Ptr a, x: int): x <= (plen v) @-}

{-@ unsafeHead :: {v:ByteString | (bLen v) > 0} -> Word8 @-}

unsafeHead :: ByteString -> Word8
unsafeHead (PS x s l) = liquidAssert (l > 0) $
  unsafePerformIO  $  withForeignPtr x $ \p -> peekByteOff p s

{-@ unsafeTail :: b:{v:ByteString | (bLen v) > 0}
               -> {v:ByteString | (bLen v) = (bLen b) - 1} @-}
unsafeTail :: ByteString -> ByteString
unsafeTail (PS ps s l) = liquidAssert (l > 0) $ PS ps (s+1) (l-1)

{-@ null :: b:ByteString -> {v:Bool | ((Prop v) <=> ((bLen b) = 0))} @-}
null :: ByteString -> Bool
null (PS _ _ l) = liquidAssert (l >= 0) $ l <= 0

{-@ unsafeDrop :: n:Nat
               -> b:{v: ByteString | n <= (bLen v)}
               -> {v:ByteString | (bLen v) = (bLen b) - n} @-}
unsafeDrop  :: Int -> ByteString -> ByteString
unsafeDrop n (PS x s l) = liquidAssert (0 <= n && n <= l) $ PS x (s+n) (l-n)

{-@ cons :: Word8 -> b:ByteString -> {v:ByteString | (bLen v) = 1 + (bLen b)} @-}
cons :: Word8 -> ByteString -> ByteString
cons c (PS x s l) = unsafeCreate (l+1) $ \p -> withForeignPtr x $ \f -> do
        poke p c
        memcpy (p `plusPtr` 1) (f `plusPtr` s) (fromIntegral l)

{-@ empty :: {v:ByteString | (bLen v) = 0} @-}
empty :: ByteString
empty = PS nullForeignPtr 0 0

{-@ assume mallocForeignPtrBytes :: n:Nat -> IO (ForeignPtrN a n) @-}
{-@ type ForeignPtrN a N = {v:ForeignPtr a | fplen v = N} @-}
{-@ malloc :: n:Nat -> IO (ForeignPtrN a n) @-}
malloc = mallocForeignPtrBytes

{-@ assume
    c_memcpy :: dst:(PtrV Word8)
             -> src:(PtrV Word8)
             -> size: {v:CSize | (v <= (plen src) && v <= (plen dst))}
             -> IO (Ptr Word8)
  @-}
foreign import ccall unsafe "string.h memcpy" c_memcpy
    :: Ptr Word8 -> Ptr Word8 -> CSize -> IO (Ptr Word8)

{-@ memcpy :: dst:(PtrV Word8)
           -> src:(PtrV Word8)
           -> size: {v:CSize | (v <= (plen src) && v <= (plen dst))}
           -> IO ()
  @-}
memcpy :: Ptr Word8 -> Ptr Word8 -> CSize -> IO ()
memcpy p q s = c_memcpy p q s >> return ()

{-@ assume nullForeignPtr :: {v: ForeignPtr Word8 | (fplen v) = 0} @-}
nullForeignPtr :: ForeignPtr Word8
nullForeignPtr = unsafePerformIO $ newForeignPtr_ nullPtr
{-# NOINLINE nullForeignPtr #-}
\end{code}

</div>