kuifje: A Quantitative Information Flow aware programming language.

[ bsd3, language, library ] [ Propose Tags ]

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.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.1.0.0, 0.1.1.0, 0.1.2.0
Change log ChangeLog.md
Dependencies base (>=4.9 && <4.13), boxes (>=0.1 && <0.2), containers (>=0.5 && <0.7), lens (>=4.17 && <4.18) [details]
License BSD-3-Clause
Author Marton Bognar
Maintainer marton.bognar@student.kuleuven.be
Category Language
Home page https://github.com/martonbognar/kuifje
Source repo head: git clone git://github.com/martonbognar/kuifje.git
Uploaded by martonbognar at 2019-09-10T10:36:55Z
Distributions
Downloads 1060 total (8 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2019-09-10 [all 1 reports]

Readme for kuifje-0.1.2.0

[back to package description]

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