seclib-0.7: A lightweight library for Information-flow security in Haskell



The security library. This is the only module of the library to be imported by untrustworthy code.



data Sec s a Source

This type represents pure values of type a at confidentiality level s.


Monad (Sec s) 
Functor (Sec s) 

up :: Less s s' => Sec s a -> Sec s' aSource

Raise the confidentiality level of values.

public :: Attacker s => Sec s a -> aSource

Reveal values that the attacker can observe.

data SecIO s a Source

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.

run :: SecIO s a -> IO (Sec s a)Source

Execute secure computations.

type File s = Loc FilePath s String ()Source

Locations that represent files

readFileSecIO :: File s -> SecIO s' (Sec s String)Source

Secure read operation for files.

writeFileSecIO :: File s -> String -> SecIO s ()Source

Secure write operation for files.

type Ref s a = Loc (IORef a) s a ()Source

Locations that represent references.

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.

getLineSecIO :: Attacker s => Screen s -> SecIO s StringSource

Secure input from the keyword.

putStrSecIO :: Attacker s => Screen s -> String -> SecIO s ()Source

Secure output to the screen.

putStrLnSecIO :: Attacker s => Screen s -> String -> SecIO s ()Source

Secure output to the screen.

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.

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.

sIsBoundSecIO :: SecSocket s -> SecIO s' (Sec s Bool)Source

Return if a socket is bound to some address.

recvSecIO :: SecSocket s -> Int -> SecIO s StringSource

Secure read operation for sockets.

sendSecIO :: SecSocket s -> String -> SecIO s IntSource

Secure write operation for sockets.

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.

data Authority s Source

Used by dlm.

certify :: sh -> Authority sh -> SecIO s a -> SecIO s aSource

Certify that a piece of code have certain authority.

class Less s s' Source


Less a a

Information can flow among entities of the same level.

Less L H

Public information can become secret.

class Attacker s Source


Attacker L

The attacker can observe public data.