The security library interface for trustworthy modules.
It is the same interface as the one for untrustworthy code (module Untrustworthy) with the addition of
revealIO to respectively break the abstraction of the security monads
as well as the declassification
- data Sec s a
- up :: Less s s' => Sec s a -> Sec s' a
- public :: Attacker s => Sec s a -> a
- data SecIO s a
- value :: Sec s a -> SecIO s a
- plug :: Less sl sh => SecIO sh a -> SecIO sl (Sec sh a)
- run :: SecIO s a -> IO (Sec s a)
- type File s = Loc FilePath s String ()
- mkFile :: FilePath -> File s
- readFileSecIO :: File s -> SecIO s' (Sec s String)
- writeFileSecIO :: File s -> String -> SecIO s ()
- type Ref s a = Loc (IORef a) s a ()
- readRefSecIO :: Ref s a -> SecIO s' (Sec s a)
- writeRefSecIO :: Ref s a -> a -> SecIO s ()
- newIORefSecIO :: s -> a -> SecIO s' (Ref s a)
- type Screen s = Attacker s => Loc () s String ()
- mkScreen :: () -> Screen s
- getLineSecIO :: Attacker s => Screen s -> SecIO s String
- putStrSecIO :: Attacker s => Screen s -> String -> SecIO s ()
- putStrLnSecIO :: Attacker s => Screen s -> String -> SecIO s ()
- s_read :: Less s' s => File s' -> SecIO s String
- s_write :: Less s s' => File s' -> String -> SecIO s (Sec s' ())
- type SecSocket s = Loc (Socket, Int) s String Int
- data SecSockAddr s
- inet_addrSecIO :: String -> SecIO s HostAddress
- portInet :: PortNumber -> SecSockAddr s -> SecSockAddr s
- socketSecIO :: Family -> SocketType -> ProtocolNumber -> SecIO s' (SecSocket s)
- bindSocketSecIO :: SecSocket s -> SecSockAddr s -> SecIO s ()
- sIsBoundSecIO :: SecSocket s -> SecIO s' (Sec s Bool)
- acceptSecIO :: SecSocket s -> SecIO s (SecSocket s, SecSockAddr s)
- recvSecIO :: SecSocket s -> Int -> SecIO s String
- sendSecIO :: SecSocket s -> String -> SecIO s Int
- connectSecIO :: SecSocket s -> SecSockAddr s -> SecIO s ()
- sIsConnectedSecIO :: SecSocket s -> SecIO s' (Sec s Bool)
- type Open s = SecIO s ()
- type Close s = SecIO s ()
- data Authority s
- certify :: sh -> Authority sh -> SecIO s a -> SecIO s a
- reveal :: Sec s a -> a
- revealIO :: SecIO s a -> IO (Sec s a)
- data Loc t s a b = MkLoc t
- class Less s s' where
- class Attacker s where
- hatch :: Less sl sh => (a -> b) -> Sec sh a -> SecIO s (Sec sl b)
- ntimes :: Int -> (Sec sh a -> SecIO s (Sec sl b)) -> IO (Sec sh a -> SecIO s (Sec sl b))
- flock :: (Sec sh a -> SecIO s (Sec sl b)) -> IO (Sec sh a -> SecIO s (Sec sl b), Open s, Close s)
- dlm :: (Sec sh a -> SecIO s (Sec sl b)) -> IO (Sec sh a -> SecIO s (Sec sl b), Authority sh)
This type represents pure values of type
a at confidentiality level
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,
Lift a pure confidential value into a secure side-effect computation.
Safely downgrade the security level indicating the side-effects performed by the computation.
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! |
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
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
to be changed.
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
b) The attacker is not on the screen-keyword. In this case, we implement
effectless_read. We choose option a) as a model.
It sets the security level of the standard input/output (usually the keyboard/screen). To be used only by trustworthy code. |
It is a derived operation for reading from files (legacy code).
It is a derived operation for writing into files (legacy code).
Locations that represent network communications via sockets.
Assing a port to the
AF_INET sockets. Port numbers are public.
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
Return if a socket is bound to some address.
Connects to a socket. It is a wrapper for
Determines a given socket is connected. It is a wrapper for
Certify that a piece of code have certain authority.
Break the abstraction provide by
Sec. It is used only in trustworthy code.
Break the abstraction provided by
SecIO. It is used only in trustworthy code!
Represent secure locations.
This data type is internally used to easily introduce new side-effects into this module.
t is the raw type needed to perform side-effects. For instance,
FilePath for files and
for references. Type
s is the confidentiality level of the
a is the type of values written and read form
This method determines that information at security level
s can flow to security level
Limit the number of times that an escape hatch can be applied by a single run of the program.
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.
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