The security library. This is the only module of the library to be imported by untrustworthy code.
- 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 ()
- 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 ()
- 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)
- data Authority s
- certify :: sh -> Authority sh -> SecIO s a -> SecIO s a
- class Less s s'
- class Attacker s
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.
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 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.