###### tags: `chalmers`
# Security

We divided the code for our secure interpreter in two module files plus a testing one:

- `Security.hs` which turned out to be so short it's easier to just copy-paste it, rather than trying to explain what it does:

module Security where

-- * Task 1

data Sensitivity = Secret | Public
 deriving (Show, Eq, Ord)

instance Semigroup Sensitivity where
   Public <> Public = Public
   _ <> _ = Secret

instance Monoid Sensitivity where 
   mempty = Public

-- * Task 2

data Labeled a = LV Sensitivity a
 deriving (Show, Eq)

instance (Ord a) => Ord (Labeled a) where
   (LV _ a) <= (LV _ b) = a <= b 

> NOTE: even if we were asked to instantiate `Monoid Semigroup` by defining `mappend` we decided to use the `<>` operator of the `Semigroup` class, instead. If we are not mistaken, this has been the best practice since `mappend` has become obsolete in the versions of Haskell following after base-4.11.0.0 [[docs](https://hackage.haskell.org/package/base-4.14.1.0/docs/Prelude.html#v:mappend)].

- `Basic.hs` which imports `Security` and in which the actual interpreter is defined

and

- `Test.hs` for automatic testing.

In `Basic.hs` we define the types `Expr`, `Name`, `Value`, `Env`, `Ptr` and `Store` accordingly:

data Expr = Lit Integer
          | Expr :+: Expr
          | Var Name
          | Let Name Expr Expr
          | NewRef Expr
          | Deref Expr
          | Expr := Expr
          | Secr Expr
  deriving (Show)

-- | Preliminaries for (immutable) local bindings
type Name  = String
type Value = Integer

-- | An environment maps variables to values.
type Env = Map Name (Labeled Value)

-- | Preliminaries for mutuable references
type Ptr    = Value
  -- ^ dangerous language: any 'Value' can be used as a 'Ptr'

-- | We need to keep track of the store containing the values of
-- our references. We also remember the next unused pointer.
data Store = Store { nextPtr :: Ptr
                   , heap    :: Map Ptr (Labeled Value)
                   }

The only changes from the code skeleton is that the environment `Env` as well as `heap` in `Store` now maps to `Labeled Value` to allow for security. We also added the `Secr` constructor for `Expr` which is used to create secret values.

The rest of the code was modified to work with `Labeled Value` instead of `Value`, which did not make it all that different. One interesting thing to point out however is how we handled the security level of references. Our heap is a map from `Ptr` to `Labeled Value`. The security level of the value cannot be changed after the reference has been created. If one tries to write a public value to a secret reference, the value in the reference becomes secret. If one tries to write a secret value to a public reference, the interpreter throws an error. Below is the code for the assignment operator of our language:

(=:) :: MonadState Store m => Ptr -> Labeled Value 
         -> m (Labeled Value)
(=:) ptr (LV p v) = do 
   store <- get
   let h = heap store
   case Map.lookup ptr h of
      Nothing -> fail $
         "Segmentation fault: "++show ptr++" is not bound"
      Just (LV p' v') -> if p < p' 
      then fail $
         "Security fault: " ++
         "Cannot write a secret value to a public location"
      else do 
         let heap' = Map.adjust (const (LV p' v)) ptr (heap store)
         put (store {heap = heap'})
         return (LV p' v)