SecLib.Trustworthy

The security library interface for trustworthy modules. It is the same interface as the one for untrustworthy code (module Untrustworthy) with the addition of functions reveal and revealIO to respectively break the abstraction of the security monads Sec and SecIO as well as the declassification combinators hatch, ntimes, flock, and dlm.

Documentation

data Sec s a

This type represents pure values of type a at confidentiality level s.

Instances

Monad (Sec s)

Functor (Sec s)

up :: Less s s' => Sec s a -> Sec s' a

Raise the confidentiality level of values.

public :: Attacker s => Sec s a -> a

Reveal values that the attacker can observe.

data SecIO s a

This type represents secure side-effect computations. These computations perform side-effects at security level, at least, s and return a value of type a with confidentiality level, at least, s.

Instances

Monad (SecIO s)

Functor (SecIO s)

value :: Sec s a -> SecIO s a

Lift a pure confidential value into a secure side-effect computation.

plug :: Less sl sh => SecIO sh a -> SecIO sl (Sec sh a)

Safely downgrade the security level indicating the side-effects performed by the computation.

run :: SecIO s a -> IO (Sec s a)

Execute secure computations.

type File s = Loc FilePath s String ()

Locations that represent files

mkFile :: FilePath -> File s

Creation of files is only allowed by trustworhty code. Observe that by creating a file, the confidentiality level of its content is being established. Therefore, the attacker can create a public file using the name of a secret file and just read it! |

readFileSecIO :: File s -> SecIO s' (Sec s String)

Secure read operation for files.

writeFileSecIO :: File s -> String -> SecIO s ()

Secure write operation for files.

type Ref s a = Loc (IORef a) s a ()

Locations that represent references.

readRefSecIO :: Ref s a -> SecIO s' (Sec s a)

Secure read operation for references.

writeRefSecIO :: Ref s a -> a -> SecIO s ()

Secure write operation for references.

newIORefSecIO :: s -> a -> SecIO s' (Ref s a)

Secure creation of a reference. We assume that the attacker has no manner to observe the side-effect of creating a reference from inside of the program, for example, by inspecting the amount of free memory. At the moment, there are no such functions inside of the monad SecIO. Nevertheless, if there is a consideration of include, for instance, a function that returns the amount of free memory in the program, then the function type of newIORefSecIO needs to be changed.

type Screen s = Attacker s => Loc () s String ()

Location that represents the screen-keyword. Here, we can choose between a) The attacker is on the screen-keyword, which implies that when taking input from the screen has an effect -- the attacker can see when the input is required. Therefore, we need to implement taking input from the keyword using effectful_read. b) The attacker is not on the screen-keyword. In this case, we implement reading using effectless_read. We choose option a) as a model.

mkScreen :: () -> Screen s

It sets the security level of the standard input/output (usually the keyboard/screen). To be used only by trustworthy code. |

getLineSecIO :: Attacker s => Screen s -> SecIO s String

Secure input from the keyword.

putStrSecIO :: Attacker s => Screen s -> String -> SecIO s ()

Secure output to the screen.

putStrLnSecIO :: Attacker s => Screen s -> String -> SecIO s ()

Secure output to the screen.

s_read :: Less s' s => File s' -> SecIO s String

It is a derived operation for reading from files (legacy code).

s_write :: Less s s' => File s' -> String -> SecIO s (Sec s' ())

It is a derived operation for writing into files (legacy code).

type SecSocket s = Loc (Socket, Int) s String Int

Locations that represent network communications via sockets.

data SecSockAddr s

It defines a socket address at confidentiality level s.

inet_addrSecIO :: String -> SecIO s HostAddress

Wrapper for inet_addr.

portInet :: PortNumber -> SecSockAddr s -> SecSockAddr s

Assing a port to the AF_INET sockets. Port numbers are public.

socketSecIO :: Family -> SocketType -> ProtocolNumber -> SecIO s' (SecSocket s)

Create a socket at confidentiality level s. The creation has no visible side-effects, e.g. sockets cannot be compared. This function is essentially a wrapper for socket.

bindSocketSecIO :: SecSocket s -> SecSockAddr s -> SecIO s ()

sIsBoundSecIO :: SecSocket s -> SecIO s' (Sec s Bool)

Return if a socket is bound to some address.

acceptSecIO :: SecSocket s -> SecIO s (SecSocket s, SecSockAddr s)

Wrapper for accept.

recvSecIO :: SecSocket s -> Int -> SecIO s String

Secure read operation for sockets.

sendSecIO :: SecSocket s -> String -> SecIO s Int

Secure write operation for sockets.

connectSecIO :: SecSocket s -> SecSockAddr s -> SecIO s ()

Connects to a socket. It is a wrapper for connect.

sIsConnectedSecIO :: SecSocket s -> SecIO s' (Sec s Bool)

Determines a given socket is connected. It is a wrapper for sIsConnected.

type Open s = SecIO s ()

Used by flock. It represents computations that open flow locks.

type Close s = SecIO s ()

Used by flock. It represents computations that close flow locks.

data Authority s

Used by dlm.

certify :: sh -> Authority sh -> SecIO s a -> SecIO s a

Certify that a piece of code have certain authority.

reveal :: Sec s a -> a

Break the abstraction provide by Sec. It is used only in trustworthy code.

revealIO :: SecIO s a -> IO (Sec s a)

Break the abstraction provided by SecIO. It is used only in trustworthy code!

data Loc t s a b

Represent secure locations. This data type is internally used to easily introduce new side-effects into this module. Type t is the raw type needed to perform side-effects. For instance, t is FilePath for files and IORef a for references. Type s is the confidentiality level of the location. Type a is the type of values written and read form t.

Constructors

MkLoc t

class Less s s' where

Methods

less :: s -> s' -> ()

This method determines that information at security level s can flow to security level s'.

Instances

Less a a

Information can flow among entities of the same level.

Less L H

Public information can become secret.

class Attacker s where

Methods

observe :: s -> ()

This method determines the observational power of the attacker. Attackers are then capable to break the abstraction of the security monads in module Sec and SecIO for security levels below or equal than s.

Instances

Attacker L

The attacker can observe public data.

hatch :: Less sl sh => (a -> b) -> Sec sh a -> SecIO s (Sec sl b)

Create an escape hatch.

ntimes :: Int -> (Sec sh a -> SecIO s (Sec sl b)) -> IO (Sec sh a -> SecIO s (Sec sl b))

Limit the number of times that an escape hatch can be applied by a single run of the program.

flock :: (Sec sh a -> SecIO s (Sec sl b)) -> IO (Sec sh a -> SecIO s (Sec sl b), Open s, Close s)

This function associates a flow lock to an escape hatch. Then, the escape hatch can be successfully applied when the flow lock is open. The escape hatch cannot by applied after closing the flock lock.

dlm :: (Sec sh a -> SecIO s (Sec sl b)) -> IO (Sec sh a -> SecIO s (Sec sl b), Authority sh)

This function allows to an escape hatch to be applied only when the running code can be certified with some authority. The certification process is just to show that the code has access to a constructor of type sh.