kuifje
所属分类：论文
开发工具：Haskell
文件大小：0KB
下载次数：0
上传日期：2019-09-10 09:51:21
上 传 者：
sh-1993
说明： 定量信息流感知编程语言的原型，基于论文：“Monad的定量信息流...，
(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.)
文件列表:
ChangeLog.md (278, 2019-09-10)
LICENSE (1524, 2019-09-10)
Setup.hs (46, 2019-09-10)
examples/ (0, 2019-09-10)
examples/Monty.hs (707, 2019-09-10)
examples/Password.hs (8398, 2019-09-10)
examples/SideChannel.hs (2225, 2019-09-10)
kuifje.cabal (1461, 2019-09-10)
src/ (0, 2019-09-10)
src/Language/ (0, 2019-09-10)
src/Language/Kuifje/ (0, 2019-09-10)
src/Language/Kuifje/Distribution.hs (2077, 2019-09-10)
src/Language/Kuifje/PrettyPrint.hs (1471, 2019-09-10)
src/Language/Kuifje/Semantics.hs (2921, 2019-09-10)
src/Language/Kuifje/Syntax.hs (1262, 2019-09-10)
# 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`
近期下载者：
相关文件：
收藏者：