{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE MultiParamTypeClasses,
FlexibleInstances #-}
{- |
Privileges are instances of the class called 'Priv'. They represent
the ability to bypass the protection of certain labels. Specifically,
privilege allows you to behave as if @L_1 ``canFlowTo`` L_2@ even when
that is not the case. The process of making data labeled @L_1@ affect
data labeled @L_2@ when @not (L_1 ``canFlowTo`` L_2)@ is called
/downgrading/.
The basic method of the 'Priv' class is 'canFlowToP', which performs a
more permissive can-flow-to check by exercising particular privileges
(in literature this relation is a pre-order, commonly written as
⊑ₚ). Almost all 'LIO' operations have variants ending
@...P@ that take a privilege argument to act in a more permissive way.
All 'Priv' types are 'Monoid's, and so privileges can be combined with
'mappend'. The creation of 'Priv' values is specific to the
particular label type in use; the method used is 'mintTCB', but the
arguments depend on the particular label type.
-}
module LIO.Privs (
-- * Privilege descriptions
PrivDesc(..)
-- * Privileges
, Priv(..)
, NoPrivs(..)
) where
import Data.Monoid
import LIO.Label
import LIO.Privs.TCB
-- | This class defines privileges and the more-permissive relation
-- ('canFlowToP') on labels using privileges. Additionally, it defines
-- 'partDowngradeP' which is used to downgrage a label up to a limit,
-- given a set of privilege.
class (Label l, PrivTCB p, Monoid p) => Priv l p where
-- | The \"can-flow-to given privileges\" pre-order used to compare
-- two labels in the presence of privileges. If @'canFlowToP' p L_1
-- L_2@ holds, then privileges @p@ are sufficient to downgrade data
-- from @L_1@ to @L_2@. Note that @'canFlowTo' L_1 L_2@ implies
-- @'canFlowToP' p L_1 L_2@ for all @p@, but for some labels and
-- privileges, 'canFlowToP' will hold even where 'canFlowTo' does
-- not.
canFlowToP :: p -> l -> l -> Bool
canFlowToP p a b = partDowngradeP p a b `canFlowTo` b
-- | Roughly speaking, @L_r = partDowngradeP p L L_g@ computes how
-- close one can come to downgrading data labeled @L@ to the goal label
-- @L_g@, given privileges @p@. When @p == 'NoPrivs'@, the resulting
-- label @L_r == L ``upperBound`` L_g@. If @p@ contains /all/
-- possible privileges, then @L_r == L_g@.
--
-- More specifically, @L_r@ is the greatest lower bound of the
-- set of all labels @L_l@ satisfying:
--
-- 1. @ L_g ⊑ L_l@, and
--
-- 2. @ L ⊑ₚ L_l@.
--
-- Operationally, @partDowngradeP@ captures the minimum change required
-- to the current label when viewing data labeled @L_l@. A common
-- pattern is to use the result of 'getLabel' as @L_g@ (i.e., the
-- goal is to use privileges @p@ to avoid changing the label at all),
-- and then compute @L_r@ based on the label of data the code is
-- about to observe.
partDowngradeP :: p -- ^ Privileges
-> l -- ^ Label from which data must flow
-> l -- ^ Goal label
-> l -- ^ Result
--
-- No privileges
--
-- | Generic privilege type used to denote the lack of privileges.
data NoPrivs = NoPrivs deriving (Show, Read)
instance PrivTCB NoPrivs
instance PrivDesc NoPrivs NoPrivs where privDesc = id
instance MintTCB NoPrivs NoPrivs where mintTCB = id
instance Monoid NoPrivs where
mempty = NoPrivs
mappend _ _ = NoPrivs
-- | With lack of privileges, 'canFlowToP' is simply 'canFlowTo', and
-- 'partDowngradeP' is the least 'upperBound'.
instance Label l => Priv l NoPrivs where
canFlowToP _ l1 l2 = l1 `canFlowTo` l2
partDowngradeP _ l lg = l `upperBound` lg