Case Study: Low Level Memory


"HeartBleed" in Haskell


Modern languages are built on top of C


Implementation errors could open up vulnerabilities


"HeartBleed" in Haskell (1/3)


A String Truncation Function


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


"HeartBleed" in Haskell (2/3)

Works if you use the valid prefix size

λ> let ex = "Ranjit Loves Jamon"

λ> heartBleed ex 10
"Ranjit Lov"


"HeartBleed" in Haskell (3/3)

Leaks overflow buffer if invalid prefix size!

λ> let ex = "Ranjit Loves Jamon"

λ> heartBleed ex 30
"Ranjit Loves Jamon\NUL\201\&1j\DC3\SOH\NUL"

Types Against Overflows


Strategy: Specify and Verify Types for


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


Errors at each level are prevented by types at lower levels

1. Low-level Pointer API


Strategy: Specify and Verify Types for


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


Errors at each level are prevented by types at lower levels

API: Types


Low-level Pointers

data Ptr a

Foreign Pointers

data ForeignPtr a

ForeignPtr wraps around Ptr; can be exported to/from C.

API: Operations (1/2)


Read

peek     :: Ptr a -> IO a

Write

poke     :: Ptr a -> a -> IO ()
Arithmetic
plusPtr  :: Ptr a -> Int -> Ptr b

API: Operations (2/2)


Create

malloc  :: Int -> ForeignPtr a


Unwrap and Use

withForeignPtr :: ForeignPtr a     -- pointer
               -> (Ptr a -> IO b)  -- action
               -> IO b             -- result

Example


Allocate a block and write 4 zeros into it


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

Example


How to prevent overflows e.g. writing 5 or 50 zeros into 4-byte block ?


Step 1

Refine pointers with allocated size


Step 2

Track sizes in pointer operations

Refined API: Types


1. Refine pointers with allocated size

measure plen  :: Ptr a -> Int
measure fplen :: ForeignPtr a -> Int


Abbreviations for pointers of size N

type PtrN a N        = {v:_ | plen v  = N}
type ForeignPtrN a N = {v:_ | fplen v = N}

Refined API: Ops (1/3)


Create

malloc  :: n:Nat -> ForeignPtrN a n


Unwrap and Use

withForeignPtr :: fp:ForeignPtr a              -- pointer
               -> (PtrN a (fplen fp) -> IO b)  -- action
               -> IO b                         -- use

Refined API: Ops (2/3)


Arithmetic

Refine type to track remaining buffer size


plusPtr :: p:Ptr a
        -> o:{Nat | o <= plen p}   -- offset in bounds
        -> PtrN b {plen b - o}     -- remainder

Refined API: Ops (3/3)


Read & Write require non-empty remaining buffer


Read

peek :: {v:Ptr a | 0 < plen v} -> IO a

Write

poke :: {v:Ptr a | 0 < plen v} -> a -> IO ()


Example: Overflow Prevented


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

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


2. ByteString API


Strategy: Specify and Verify Types for


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


Errors at each level are prevented by types at lower levels


ByteString Type


data ByteString = PS { bPtr :: ForeignPtr Word8 , bOff :: !Int , bLen :: !Int }


Refined ByteString Type


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


Refined ByteString Type



A Useful Abbreviation

type ByteStringN N = {v:ByteString| bLen v = N}


{-@ 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)


Note: length of good2 is 3 which is less than allocated size 5

Illegal Bytestrings


bad1 = do fp <- malloc 3 return (PS fp 0 10) bad2 = do fp <- malloc 3 return (PS fp 2 2)


Claimed length exceeds allocation ... rejected at compile time

API create : Allocate and Fill a ByteString


Specification

{-@ create :: n:Nat -> (PtrN Word8 n -> IO ()) -> ByteStringN n @-}

Implementation

create n fill = unsafePerformIO $ do fp <- malloc n withForeignPtr fp fill return (PS fp 0 n)

API pack : Convert List of Char into ByteString


Specification

{-@ pack :: s:String -> ByteStringN (len s) @-}

Implementation

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 ()

API unsafeTake : Extract prefix of size n


Specification

{-@ unsafeTake :: n:Nat -> b:{ByteString | n <= bLen b} -> ByteStringN n @-}

Implementation

unsafeTake n (PS x s l) = PS x s n

API unpack : Convert ByteString into List of Char


Specification

unpack :: b:ByteString -> StringN (bLen b)


Implementation

unpack b = you . get . the . idea -- see source

3. Application API


Strategy: Specify and Verify Types for


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


Errors at each level are prevented by types at lower levels

Revisit "HeartBleed"


Lets revisit our potentially "bleeding" chop

{-@ 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

"HeartBleed" no more


demo = [ex6, ex30] where ex = "St. Louis" -- has size 9 ex6 = chop ex 6 -- ok ex30 = chop ex 30 -- out of bounds


"Bleeding" chop ex 30 rejected by compiler

Recap: Types vs Overflows


Strategy: Specify and Verify Types for


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


Errors at each level are prevented by types at lower levels