| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell98 |
SecLib.Untrustworthy
Description
The security library. This is the only module of the library to be imported by untrustworthy code.
- data Sec s a
- up :: forall a s s'. 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 :: forall sl sh a. 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.
up :: forall a s s'. Less s s' => Sec s a -> Sec s' a Source
Raise the confidentiality level of values.
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 a Source
Lift a pure confidential value into a secure side-effect computation.
plug :: forall sl sh a. 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.
writeFileSecIO :: File s -> String -> SecIO s () Source
Secure write operation for files.
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 String Source
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 Int Source
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 HostAddress Source
Wrapper for inet_addr.
portInet :: PortNumber -> SecSockAddr s -> SecSockAddr s Source
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 a Source
Certify that a piece of code have certain authority.
Minimal complete definition