-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Static Mandatory Access Control in Haskell
--   
@package mac
@version 0.1.0.0


-- | It defines main data structures for security, i.e., monad family
--   <a>MAC</a> and labeled resources <a>Res</a>.
module MAC.Core

-- | Labeling expressions of type <tt>a</tt> with label <tt>l</tt>.
newtype Res l a
MkRes :: a -> Res l a
unRes :: Res l a -> a

-- | Label of resources
labelOf :: Res l a -> l

-- | This monad labels the results of the computation (of type <tt>a</tt>)
--   with label <tt>l</tt>.
newtype MAC l a
MkMAC :: (IO a) -> MAC l a

-- | Execute secure computations.
runMAC :: MAC l a -> IO a

-- | It lifts arbitrary <a>IO</a>-actions.
ioTCB :: IO a -> MAC l a
instance Monad (MAC l)
instance Applicative (MAC l)
instance Functor (MAC l)


-- | Exceptions
module MAC.Exception

-- | Throwing exceptions
throwMAC :: Exception e => e -> MAC l a

-- | Throwing and catching exceptions are done among family members with
--   the same labels
catchMAC :: Exception e => MAC l a -> (e -> MAC l a) -> MAC l a


-- | A safe interface for module <tt>Core.hs</tt>
module MAC.MAC

-- | Labeling expressions of type <tt>a</tt> with label <tt>l</tt>.
data Res l a

-- | Label of resources
labelOf :: Res l a -> l

-- | This monad labels the results of the computation (of type <tt>a</tt>)
--   with label <tt>l</tt>.
data MAC l a

-- | Execute secure computations.
runMAC :: MAC l a -> IO a

-- | To help the type-system
fix :: l -> MAC l ()


-- | Encodes a security lattice.
module MAC.Lattice

-- | Type class encoding security lattices
class CanFlowTo l l' => Less l l'

-- | Label for secrets
data H

-- | Label for public data
data L
instance [safe] Less H H
instance [safe] Less L H
instance [safe] Less L L
instance [safe] CanFlowTo H H
instance [safe] CanFlowTo L H
instance [safe] CanFlowTo L L


-- | It provides functions which map read and write effects into security
--   checks.
module MAC.Effects

-- | It lifts functions which create resources into secure functions which
--   create labeled resources
create :: Less l l' => IO (d a) -> MAC l (Res l' (d a))

-- | It lifts an <a>IO</a>-action which writes into a data type <tt>d
--   a</tt> into a secure function which writes into a labeled resource
writeup :: Less l l' => (d a -> IO ()) -> Res l' (d a) -> MAC l ()

-- | It lifts an <a>IO</a>-action which reads from a data type <tt>d a</tt>
--   into a secure function which reads from a labeled resource
readdown :: Less l' l => (d a -> IO a) -> Res l' (d a) -> MAC l a

-- | Proxy function to set the index of the family member <a>MAC</a>
fix :: l -> MAC l ()

-- | Auxiliary function. A combination of <a>fix</a> and <a>readdown</a>.
read_and_fix :: Less l l => (d a -> IO a) -> Res l (d a) -> MAC l a

-- | Auxiliary function. A combination of <a>fix</a> and <a>readdown</a>.
write_and_fix :: Less l' l' => (d a -> IO ()) -> Res l' (d a) -> MAC l' ()

-- | It lifts an operation which perform a read on data type <tt>d a</tt>,
--   but it also performs a write on it as side-effect
rw_read :: (Less l l', Less l' l) => (d a -> IO a) -> Res l' (d a) -> MAC l a

-- | It lifts an operation which perform a write on data type <tt>d a</tt>,
--   but it also performs a read on it as side-effect
rw_write :: (Less l l', Less l' l) => (d a -> IO ()) -> Res l' (d a) -> MAC l ()


-- | Labeled expressions.
module MAC.Labeled

-- | Labeled expressions
type Labeled l a = Res l (Id a)

-- | Type denoting values of type <tt>a</tt>
data Id a
MkId :: a -> Id a

-- | Creation of labeled expressions
label :: Less l l' => a -> MAC l (Labeled l' a)

-- | Observing labeled expressions
unlabel :: Less l' l => Labeled l' a -> MAC l a


-- | Synchronization primitives
module MAC.MVar

-- | Labeled <tt>MVars</tt>
type MACMVar l a = Res l (MVar a)

-- | Creation of a labeled <tt>MVar</tt>
newMACMVar :: Less l l' => a -> MAC l (MACMVar l' a)

-- | Creation of an empty labeled <tt>MVar</tt>
newMACEmptyMVar :: Less l l' => MAC l (MACMVar l' a)

-- | Securely taking a labeled <tt>MVar</tt>
takeMACMVar :: Less l l => MACMVar l a -> MAC l a

-- | Securely writing into a labeled <tt>MVar</tt>
putMACMVar :: Less l l => MACMVar l a -> a -> MAC l ()


-- | Provide primitives to communicate among family members. It provides an
--   API for sequential <a>joinMAC</a> and concurrent (<a>forkMAC</a>)
--   setting
module MAC.Control

-- | Primitive which allows family members to safely communicate. The
--   function finishes even if an exception is raised---the exception is
--   rethrown when the returned value gets inspected. <b>This function must
--   not be used in a concurrent setting</b>.
joinMAC :: Less l l' => MAC l' a -> MAC l (Labeled l' a)

-- | Safely spawning new threads
forkMAC :: Less l l' => MAC l' () -> MAC l ()

-- | Safely spawning new threads. The function returns a labeled
--   <a>MVar</a> where the outcome of the thread is stored
forkMACMVar :: (Less l' l', Less l l') => MAC l' a -> MAC l (MACMVar l' a)


-- | Mutuable state (references)
module MAC.Ref

-- | Labeled references
type MACRef l a = Res l (IORef a)

-- | Creation of labeled references
newMACRef :: Less l l' => a -> MAC l (MACRef l' a)

-- | Reading labeled references
readMACRef :: Less l' l => MACRef l' a -> MAC l a

-- | Writing labeled references
writeMACRef :: Less l l' => MACRef l' a -> a -> MAC l ()