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
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.
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.
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.