kuifje-0.1.0.0: README.md
# Kuifje
A prototype for a Quantitative Information Flow aware programming language.
Based on the paper: "Quantitative Information Flow with Monads in Haskell" by Jeremy Gibbons, Annabelle McIver, Carroll Morgan, and Tom Schrijvers.
## Generating documentation
The important functions in the code are documented using Haddock notation.
To generate the documentation in HTML format, run `cabal haddock`.
## Defining a program
The syntax of the language is defined in the `src/Syntax.hs` file. You can use the predefined constructor functions and the combinator `<>` to define programs. Using the `Control.Lens` library and helper functions for the syntax can simplify the implementation.
A brief example:
```hs
-- | State space for the program.
data SE = SE {
_x :: Integer,
_y :: Integer
} deriving (Eq, Ord)
makeLenses ''SE
-- | Initialize the state by giving a value to x and setting y to 0.
initSE :: Integer -> SE
initSE x = SE { _x = x, _y = 0 }
program :: Kuifje SE
program
= update (\s -> return (s.^y $ 0)) <> -- y := 0
while (\s -> return (s^.x > 0)) ( -- while (x > 0) {
update (\s -> return (s.^y $ (s^.x + s^.y))) <> -- y := x + y
update (\s -> return (s.^x $ (s^.x - 1))) -- x := x - 1
) -- }
```
For more elaborate syntax, see the examples.
## Running the analysis
The function `hysem` from the `Semantics` module can be used to calculate the hyper-distributions based on a program and the input distributions.
The `Semantics` module offers the `bayesVuln` function to calculate the Bayes Vulnerability of distributions, this can be combined with the `condEntropy` function to calculate the average entropy over a hyper-distribution.
Continuing the above example:
```hs
-- | Extract the meaningful variable from the state space.
project :: Dist (Dist SE) -> Dist (Dist Integer)
project = fmap (fmap (\s -> s^.y))
-- | Generate the hyper-distribution for an input of x : [5..8]
-- with uniform distribution.
hyper :: Dist (Dist Integer)
hyper = project $ hysem program (uniform [initSE x | x <- [5..8]])
run :: IO ()
run = do
putStrLn "> hyper"
print hyper
putStrLn "> condEntropy bayesVuln hyper"
print $ condEntropy bayesVuln hyper
-- > hyper
-- 1 % 4 1 % 1 15
-- 1 % 4 1 % 1 21
-- 1 % 4 1 % 1 28
-- 1 % 4 1 % 1 36
-- > condEntropy bayesVuln hyper
-- 1 % 1
```
## Examples
The following examples are implemented in this repository:
- The Monty-Hall problem: `Monty.hs`
- Defence against side-channels: `SideChannel.hs`
- Password checker: `Password.hs`