**Research** (UPB/ACS)

Improving the security of software systems

In general, system software

In particular, operating systems

**Development** (VirtualMetrix)

VMXL4, a "provably secure" microkernel/hypervisor

Virtualization for mobile phones

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

Programming Paradigms

Operating System Security

Advanced Operating Systems

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

Is it deployed in the real world?

Haskell is:

- Pure, lazy
- Strongly typed, statically-typed

Haskell's type system has the following particularities:

- Algebraic data types
- Parametric polymorphism
- Ad-hoc polymorphism

Every Haskell type is

Either a primitive type

Or a sum of types

Or a product of 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

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

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

Now we can say:

`fruit_e fr = Tomatoes;`

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

But we can also say:

`fruit_e fr = 5;`

```
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**

- More generally,

```
data Fruit =
Apples
| Pears
| Oranges
| Tomatoes
```

```
> :t Apples
Apples :: Fruit
> 5 :: Fruit
<interactive>
No instance for (Num Fruit) ..
```

```
data Fruit =
Apples
| Pears
| Oranges
| Tomatoes
```

**Note**: we select**one of**the values in`Fruit`

`|`

is in general similar to`union`

s**Intuition**:`|`

is the logical equivalent of**or**

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

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**

`data Bucket = MkBucket Fruit Int`

`Bucket`

is the type's name`MkBucket`

is the**constructor**

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

- It may be useful to generalize
- In this case,
`Fruit`

is too particular

`data Bucket a = MkBucket a Int`

- 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
```

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

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

- Type fields are similar to
`struct`

s **Intuition**: tuples are the logical equivalent of**and**

- 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

**Idea**:`MultiBucket`

s as lists of`Bucket`

s

`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

- E.g.

`type MultiBucket a = [Bucket a]`

Extracting all the `Apple`

s from a MultiBucket

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

`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
```

`data Maybe a = Nothing | Just a`

`Nothing`

is similar to`void`

`Just`

is a 1-tuple that wraps values**Intuition**: return`Nothing`

on failure

```
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

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

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

```
> :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`(==)`

"

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

```
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
```

`Bucket`

s can have non-sensical values:

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

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

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`

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
```

Possible approach: Peano naturals

`data Nat2 = Z | S Nat2`

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

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

- 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
`*`

```
class MyClass a where
myMethod :: a -> Int
instance MyClass Int where
myMethod = (+ 1) . fromIntegral
```

```
> myMethod (42 :: Int)
42
```

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

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
```

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`

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
```

Testing

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

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

`head`

and `tail`

are unsafe

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

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!

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
```

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) ..
```