A bit about what I do

Research (UPB/ACS)

• Improving the security of software systems

• In general, system software

• In particular, operating systems

A bit about what I do

Development (VirtualMetrix)

• VMXL4, a "provably secure" microkernel/hypervisor

• Virtualization for mobile phones

A bit about what I do

Teaching assistant (UPB/ACS) for the following courses:

• Programming Paradigms

• Operating System Security

• Advanced Operating Systems

Some related work

seL4 microkernel

• Developed by UNSW/NICTA/General Dynamics

• Formally verified protection model and implementation

• Prototype written in Haskell

• Recently GPLed: https://github.com/seL4/seL4

Designing software using Haskell

Haskell is:

Algebraic data types

Every Haskell type is

• Either a primitive type

• Or a sum of types

• Or a product of types

Example 1: primitive types

3 :: Int
120894192912541294198294982 :: Integer
3.14 :: Float
'a' :: Char
"The cake is a lie" :: String
True :: Bool

• :: is similar to set membership ( ∈ )
• Intuition: types are (a generalization of) sets

Example 2: sum types

• Problem: encode an enumeration of fruits
• Suppose we wish to have exactly four types of fruit
  • Apples
  • Pears
  • Oranges
  • Tomatoes

Example 2 in C

typedef enum {
    Apples = 1,
    Pears = 2,
    Oranges = 3,
    Tomatoes = 4
} fruit_e;

Now we can say:

fruit_e fr = Tomatoes;

Example 2 in C

typedef enum {
    Apples = 1,
    Pears = 2,
    Oranges = 3,
    Tomatoes = 4
} fruit_e;

But we can also say:

fruit_e fr = 5;

Example 2 in Haskell

data Fruit =
    Apples
  | Pears
  | Oranges
  | Tomatoes

• Fruit is the type's name
• | is the sum type-level operator
• Apples, Pears, Oranges, Tomatoes are possible values
  • More generally, constructors

Example 2 in Haskell

data Fruit =
    Apples
  | Pears
  | Oranges
  | Tomatoes

> :t Apples
Apples :: Fruit
> 5 :: Fruit

<interactive>
  No instance for (Num Fruit) ..

Example 2 in Haskell

data Fruit =
    Apples
  | Pears
  | Oranges
  | Tomatoes

• Note: we select one of the values in Fruit
• | is in general similar to unions
• Intuition: | is the logical equivalent of or

Example 3: product types

• Problem: encode "a bucket of fruit"
• A bucket of fruit consists of:
  • A type of fruit
  • The quantity of fruit in the bucket

Example 3

Possible approach: use built-in pairs

> :t (,)
(,) :: a -> b -> (a, b)
> (,) Pears 2 :: (Fruit, Int)
(Pears,2)
> (Pears, 2) -- sugar
(Pears,2)

• (,) defines pairs of values
• Note: small letters denote type variables
  • Parametric polymorphism

Example 3

data Bucket = MkBucket Fruit Int

• Bucket is the type's name
• MkBucket is the constructor

> :t MkBucket
MkBucket :: Fruit -> Int -> Bucket

Example 3

• It may be useful to generalize
• In this case, Fruit is too particular

data Bucket a = MkBucket a Int

Example 3

• We can implicitly define field selectors
• ... by using record notation

data Bucket a = MkBucket
  { bucketObject  :: a
  , bucketQty     :: Int
  }

> let myBucket = MkBucket Apples 10
> bucketQty myBucket
10

Example 3

• We can implicitly define field selectors
• ... by using record notation

data Bucket a = MkBucket
  { bucketObject  :: a
  , bucketQty     :: Int
  }

• Type fields are similar to structs
• Intuition: tuples are the logical equivalent of and

Example 4: MultiBuckets

• What if we want to hold more than one type of fruit in a bucket?

> MkBucket (Pears, Apples) 50

• ... but we can't distinguish between types of fruits

Example 4

type MultiBucket a = [Bucket a]

• type is similar to C's typedef
  • Type synonyms
• Note: synonyms are not subjected to type checking
  • E.g. MultiBucket a and [Bucket a] are the same type

Example 4

type MultiBucket a = [Bucket a]

Extracting all the Apples from a MultiBucket

> let mb = [MkBucket Apples 20,
  MkBucket Pears 30]
> head $
  filter (\ b -> bucketObject b == Apples ) mb
MkBucket {bucketObject = Apples, bucketQty = 20}

Example 4

type MultiBucket a = [Bucket a]

What if there are no apples in the MultiBucket?

> let mb = [MkBucket Pears 30]
> head $
  filter (\ b -> bucketObject b == Apples ) mb
*** Exception: Prelude.head: empty list

Example 5: representing failure

data Maybe a = Nothing | Just a

• Nothing is similar to void
• Just is a 1-tuple that wraps values
• Intuition: return Nothing on failure

Example 5

getBucket :: Fruit -> MultiBucket Fruit
                   -> Maybe (Bucket Fruit)
getBucket obj mb = case filter isEqual mb of
  []      -> Nothing
  (x : _) -> Just x
  where isEqual x = bucketObject x == obj

• Note: case performs pattern matching on values
• Note: [] is the empty list; x : list is a non-empty list

Example 5

> let mb = [MkBucket Pears 30]
> getBucket Apples mb
Nothing
> getBucket Pears mb
Just (MkBucket
  {bucketObject = Pears, bucketQty = 30})

Example 5

We can make getBucket polymorphic:

getBucket :: Eq a => a -> MultiBucket a
                       -> Maybe (Bucket a)

• Implementation stays the same
• Eq a: constraint imposed on a due to (==)

Example 5

> :t (==)
(==) :: Eq a => a -> a -> Bool

• deriving tries to automatically implement (==) for ADTs
• Eq a is a type class constraint
• Ad-hoc polymorphism:
  • Eq a  ≡  "all types a that implement (==)"

Example 6: seL4 kernel objects

 data KernelObject 
     = KOEndpoint  Endpoint
     | KOAEndpoint AsyncEndpoint
     | KOKernelData
     | KOUserData
     | KOTCB       TCB
     | KOCTE       CTE
     | KOArch      ArchKernelObject

Example 6

data TCB = Thread {
        tcbCTable :: CTE,
        tcbVTable :: CTE,
        tcbReply :: CTE,
        tcbCaller :: CTE,
        tcbIPCBufferFrame :: CTE,
        tcbDomain :: Domain,
        tcbState :: ThreadState,
        ..
        tcbFaultHandler :: CPtr,
        tcbIPCBuffer :: VPtr,
        tcbContext :: UserContext }
    deriving Show

Example 7: natural numbers

Buckets can have non-sensical values:

> :t MkBucket Apples (-2)
MkBucket Apples (-2) :: Bucket Fruit

Example 7

Possible approach: smart constructors

newtype Nat1 = Nat1 { fromNat1 :: Int }

• newtype is like data, only
  • It has exactly one constructor
  • ... and exactly one field
• Additionally, it's erased at compile-time
  • No run-time overhead

Example 7

Possible approach: smart constructors

mkNat :: Int -> Nat1
mkNat n = if n < 0
  then error "Only positive numbers are permitted"
  else Nat1 n

• mkNat checks for positive numbers at run-time
• It provides some compile-time guarantees
  • All type conversions are explicit
  • Signedness is (a weak) invariant under Nat1

Example 8: more naturals

Possible approach: Peano naturals

data Nat2 = Z | S Nat2

> :t Z -- 0
Z :: Nat2
> :t S $ S $ S Z -- 3
S $ S $ S Z :: Nat2

Example 8

Possible approach: Peano naturals

data Nat2 = Z | S Nat2

• Very clunky and inefficient
• Works well for small enough numbers

Example 9: even more naturals

Possible approach: type-level numbers

data Z
data S n

• Z and S n are types encoding numbers!
• Note: Z and S n lack constructors

Digression: kinds

• Types also have types
• They are called kinds

> :k Z
Z :: *
> :k S
S :: * -> *
> :k (S (S Z))
(S (S Z)) :: *

• Well-formed typed expressions have the kind *

Digression: type classes

class MyClass a where
  myMethod :: a -> Int

instance MyClass Int where
  myMethod = (+ 1) . fromIntegral

> myMethod (42 :: Int)
42

Example 9

First we define cardinalities on type-level naturals

class Card n where

instance Card Z where
instance (Card n) => Card (S n) where

• Note: computations are done purely at type-level
  • type class and instances have no methods

Example 9

Next, we define a class for bound checking

class (Card n) => InBounds n where

instance InBounds (S Z) where
instance InBounds (S (S Z)) where
instance InBounds (S (S (S Z))) where

Example 9

Finally, we define a concrete type and a smart constructor

data MaxThree n = MaxThree
  deriving Show

maxthree :: InBounds n => n -> MaxThree n
maxthree _ = MaxThree

• Note: We restrict smart constructor to InBounds

Example 9

Some useful auxiliary functions

incr :: Card n => n -> S n
incr = undefined

d0 = undefined :: Z
d1 = incr d0
d2 = incr d1
d3 = incr d2
d4 = incr d3

Example 9

Testing

> maxthree d4

<interactive>
  No instance for (InBounds Z) ..
> maxthree d1
MaxThree

Example 9: conclusion

• We can perform compile-time checks on numbers

• However, it's very tedious to do that

• We can use dependently typed languages (e.g. Idris) as an alternative

Haskell extensions for static checking

• Functional dependencies
  http://haskell.org/haskellwiki/Functional_dependencies
• Contract checking
  http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/index.htm
  http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/

Extra example: non-empty lists

head and tail are unsafe

> let xs = []
> head xs
*** Exception: Prelude.head: empty list
> tail xs
*** Exception: Prelude.tail: empty list

Extra example

We can make them safe by encoding non-emptiness in the program logic

data NonEmpty a = a :| [a] -- Data.List.NonEmpty

> let xs = 1 :| [2,3,4]
> -- provably non-empty
> head xs
1

• Note: This can make coding more difficult!

Extra example

Generalization using type-level numbers: mono-traversable

cadr :: MinLen (Succ (Succ nat)) [a] -> a
cadr = ML.head . ML.tailML

> let xs = mlcons 3 $ mlcons 2 $ toMinLenZero []
> cadr xs
2

Extra example

Generalization using type-level numbers: mono-traversable

-- this fails at compile-time!
> let xs = mlcons 2 $ toMinLenZero []
> cadr xs

<interactive>
  Couldn't match type `Zero' with `Succ nat0'
  Expected type: MinLen (Succ (Succ nat0)) .. 
  Actual type: MinLen (Succ Zero) ..