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
.
- 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)
Documentation
This type represents pure values of type a
at confidentiality level s
.
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
.
value :: Sec s a -> SecIO s aSource
Lift a pure confidential value into a secure side-effect computation.
plug :: Less sl sh => SecIO sh a -> SecIO sl (Sec sh a)Source
Safely downgrade the security level indicating the side-effects performed by the computation.
mkFile :: FilePath -> File sSource
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! |
readRefSecIO :: Ref s a -> SecIO s' (Sec s a)Source
Secure read operation for references.
writeRefSecIO :: Ref s a -> a -> SecIO s ()Source
Secure write operation for references.
newIORefSecIO :: s -> a -> SecIO s' (Ref s a)Source
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 ()Source
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 sSource
It sets the security level of the standard input/output (usually the keyboard/screen). To be used only by trustworthy code. |
s_read :: Less s' s => File s' -> SecIO s StringSource
It is a derived operation for reading from files (legacy code).
s_write :: Less s s' => File s' -> String -> SecIO s (Sec s' ())Source
It is a derived operation for writing into files (legacy code).
type SecSocket s = Loc (Socket, Int) s String IntSource
Locations that represent network communications via sockets.
data SecSockAddr s Source
It defines a socket address at confidentiality level s
.
inet_addrSecIO :: String -> SecIO s HostAddressSource
Wrapper for inet_addr
.
portInet :: PortNumber -> SecSockAddr s -> SecSockAddr sSource
Assing a port to the AF_INET
sockets. Port numbers are public.
socketSecIO :: Family -> SocketType -> ProtocolNumber -> SecIO s' (SecSocket s)Source
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 ()Source
sIsBoundSecIO :: SecSocket s -> SecIO s' (Sec s Bool)Source
Return if a socket is bound to some address.
acceptSecIO :: SecSocket s -> SecIO s (SecSocket s, SecSockAddr s)Source
Wrapper for accept
.
connectSecIO :: SecSocket s -> SecSockAddr s -> SecIO s ()Source
Connects to a socket. It is a wrapper for connect
.
sIsConnectedSecIO :: SecSocket s -> SecIO s' (Sec s Bool)Source
Determines a given socket is connected. It is a wrapper for sIsConnected
.
certify :: sh -> Authority sh -> SecIO s a -> SecIO s aSource
Certify that a piece of code have certain authority.
Break the abstraction provide by Sec
. It is used only in trustworthy code.
revealIO :: SecIO s a -> IO (Sec s a)Source
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.
Type t
is the raw type needed to perform side-effects. For instance,
t
is FilePath
for files and
for references. Type IORef
as
is the confidentiality level of the
location. Type a
is the type of values written and read form t
.
MkLoc t |
This method determines that information at security level s
can flow to security level s'
.
ntimes :: Int -> (Sec sh a -> SecIO s (Sec sl b)) -> IO (Sec sh a -> SecIO s (Sec sl b))Source
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)Source
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)Source
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
.