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:

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

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