kuifje (empty) → 0.1.0.0

raw patch · 9 files changed

+399/−0 lines, 9 filesdep +basedep +boxesdep +containerssetup-changed

Dependencies added: base, boxes, containers, lens, unordered-containers

Files

ChangeLog.md +5/−0
LICENSE +30/−0
README.md +83/−0
Setup.hs +2/−0
kuifje.cabal +32/−0
src/Language/Kuifje/Distribution.hs +63/−0
src/Language/Kuifje/PrettyPrint.hs +52/−0
src/Language/Kuifje/Semantics.hs +80/−0
src/Language/Kuifje/Syntax.hs +52/−0

+ ChangeLog.md view

@@ -0,0 +1,5 @@+# Revision history for kuifje++## 0.1.0.0  -- YYYY-mm-dd++* First version. Released on an unsuspecting world.

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2019, Marton Bognar++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Marton Bognar nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,83 @@+# 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`

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ kuifje.cabal view

@@ -0,0 +1,32 @@+-- Initial kuifje.cabal generated by cabal init.  For further+-- documentation, see http://haskell.org/cabal/users-guide/++name:                kuifje+version:             0.1.0.0+synopsis:            A Quantitative Information Flow aware programming language.+description:         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.+-- description:+license:             BSD3+license-file:        LICENSE+author:              Marton Bognar+maintainer:          marton.bognar@student.kuleuven.be+homepage:            https://github.com/martonbognar/kuifje+-- copyright:+category:            Language+build-type:          Simple+extra-source-files:  ChangeLog.md, README.md+cabal-version:       >=1.10+-- repository:+source-repository head+  type:     git+  location: git://github.com/martonbognar/kuifje.git++library+  exposed-modules:     Language.Kuifje.Distribution, Language.Kuifje.PrettyPrint, Language.Kuifje.Semantics, Language.Kuifje.Syntax+  --other-modules:+  other-extensions:    TemplateHaskell, ExistentialQuantification, TypeOperators, TypeSynonymInstances, FlexibleInstances+  build-depends:       base >=4.9 && <4.10, lens >=4.17 && <4.18, boxes >=0.1 && <0.2, containers >=0.5 && <0.6, unordered-containers >= 0.2.10 && < 0.3+  hs-source-dirs:      src+  default-language:    Haskell2010

+ src/Language/Kuifje/Distribution.hs view

@@ -0,0 +1,63 @@+{-# OPTIONS_GHC -Wall #-}++{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-}++module Language.Kuifje.Distribution where++import Prelude hiding (filter, foldr, return, (>>=))+import Data.List (genericLength)+import Data.Map.Strict++-- | Type synonym for probabilities.+type Prob = Rational++-- | Distribution data type.+newtype Dist a = D { runD :: Map a Prob }++-- | Top-level fmap function for distributions.+fmap :: (Ord b) => (a -> b) -> Dist a -> Dist b+fmap f dx = dx >>= (return . f)++-- | Top-level return function for distributions. Creates a singleton+-- distribution.+return :: (Ord a) => a -> Dist a+return x = D $ singleton x 1++-- | Top-level bind function for distributions.+(>>=) :: (Ord b) => Dist a -> (a -> Dist b) -> Dist b+d >>= f = D $ fromListWith (+) [(y, p * q) | (x, p) <- toList $ runD d, (y, q) <- toList $ runD (f x)]++-- | Top-level join function for distributions.+join :: (Ord a) => Dist (Dist a) -> Dist a+join x = x >>= id++instance Ord a => Eq (Dist a) where+  d1 == d2  =  unpackD d1 == unpackD d2++instance Ord a => Ord (Dist a) where+  d1 <= d2  =  unpackD d1 <= unpackD d2++-- | Construct a discrete distribution from a nonempty list of elements,+-- assigning the same probability to each element.+uniform :: (Ord a) => [a] -> Dist a+uniform l = D $ fromListWith (+) [(x, 1 / genericLength l) | x <- l]++-- | Construct a distribution in which the first element has probability p+-- and the second 1−p.+choose :: (Ord a) => Prob -> a -> a -> Dist a+choose p x y = D $ fromListWith (+) [(x, p), (y, 1 - p)]++-- | Recover the map representation of a distribution, reduced.+unpackD :: Dist a -> Map a Prob+unpackD = removeZeroes . runD+  where+    removeZeroes = filter (/= 0)++-- | Remove zeroes from a distribution.+reduction :: Dist a -> Dist a+reduction = D . unpackD++-- | Sum the probabilities in the distribution.+weight :: Dist a -> Prob+weight (D l) = foldr (+) 0 l

+ src/Language/Kuifje/PrettyPrint.hs view

@@ -0,0 +1,52 @@+module Language.Kuifje.PrettyPrint where++import Data.List (transpose)+import Text.PrettyPrint.Boxes+import qualified Data.Map.Strict as HM (mapWithKey, elems)++import Language.Kuifje.Distribution++class Boxable a where+  toBox :: a -> Box++instance Boxable Bool where+  toBox b = text (show b)++instance Boxable Integer where+  toBox i = text (show i)++instance Boxable Int where+  toBox i = text (show i)++instance Show a => Boxable [a] where+  toBox = text . show++instance (Show a, Show b) => Boxable (a,b) where+  toBox p  =  text (show p)++instance (Show a, Show b, Show c) => Boxable (a,b,c) where+  toBox p  =  text (show p)++instance (Show a, Show b, Show c, Show d) => Boxable (a,b,c,d) where+  toBox p  =  text (show p)++distToBox :: (Ord a, Boxable a) => Dist a -> Box+distToBox d = tabulate $ HM.elems (HM.mapWithKey lambdaPrint (unpackD d))+                where lambdaPrint e p = [text (show p), toBox e]++instance (Boxable a, Ord a) => Boxable (Dist a) where+  toBox = distToBox++instance (Ord a, Boxable a) => Show (Dist a) where+  show = render . distToBox++tabulate :: [[Box]] -> Box+tabulate rs = table+  where+   heights  = map (maximum . map rows) rs+   rs''     = zipWith (\r h -> map (alignVert top h) r) rs heights+   columns  = transpose rs''+   widths   = map (maximum . map cols) columns+   rs'      = transpose (zipWith (\c w -> map (alignHoriz left w) c) columns widths)+   columns' = map (hsep 3 top) rs'+   table    = vsep 0 left columns'

+ src/Language/Kuifje/Semantics.hs view

@@ -0,0 +1,80 @@+{-# OPTIONS_GHC -Wall #-}++{-# LANGUAGE TypeOperators #-}++module Language.Kuifje.Semantics where++import Prelude hiding (return, fmap, (>>=))+import Data.Map.Strict (fromListWith, toList, elems)++import Language.Kuifje.Distribution+import Language.Kuifje.Syntax++-- | Hyper-distribution type synonym.+type a ~~> b = Dist a -> Dist (Dist b)++-- | Bind with reduction applied to the input distribution.+(=>>) :: (Ord b) => Dist a -> (a -> Dist b) -> Dist b+m =>> f = reduction m >>= f++-- | Kleisli composition.+(==>) :: (Ord c) => (a ~> b) -> (b ~> c) -> (a ~> c)+f ==> g = \x -> f x >>= g++-- | For a given program, returns a function that calculates the+-- hyper-distribution for a given input distribution.+hysem :: (Ord s) => Kuifje s -> (s ~~> s)+hysem Skip          = return+hysem (Update f p)  = huplift f ==> hysem p+hysem (If c p q r)  = conditional c (hysem p) (hysem q) ==> hysem r+hysem (While c p q) = let wh = conditional c (hysem p ==> wh) (hysem q)+                      in wh+hysem (Observe f p) = hobsem f ==> hysem p++-- | Conditional semantics ('If' and 'While').+conditional :: (Ord s) => (s ~> Bool) -> (s ~~> s) -> (s ~~> s) -> (s ~~> s)+conditional c t e d+  = let d' = d =>> \s -> c s =>> \b -> return (b, s)+        w1 = sum [p | ((b, _), p) <- toList $ runD d', b]+        w2 = 1 - w1+        d1 = D $ fromListWith (+) [(s, p / w1) | ((b, s), p) <- toList $ runD d', b]+        d2 = D $ fromListWith (+) [(s, p / w2) | ((b, s), p) <- toList $ runD d', not b]+        h1 = t d1+        h2 = e d2+    in  if       null (runD d2)  then  h1+        else if  null (runD d1)  then  h2+                                 else  join (choose w1 h1 h2)++-- | Lifts a distribution to a hyper-distribution.+huplift :: (Ord s) => (s ~> s) -> (s ~~> s)+huplift f = return . (=>> f)++-- | 'Observe' semantics.+hobsem :: (Ord s, Ord o) => (s ~> o) -> (s ~~> s)+hobsem f = multiply . toPair . (=>> obsem f)+  where++    obsem :: (Ord o, Ord a) => (a ~> o) -> a ~> (o,a)+    obsem f' x = fmap (\w -> (w, x)) (f' x)++    toPair :: (Ord s, Ord o) => Dist (o, s) -> (Dist o, o -> Dist s)+    toPair dp = (d, f')+      where+        d     = fmap fst dp+        f' ws = let dpws = D $ fromListWith (+) [(s, p) | ((ws', s), p) <- toList $ runD dp, ws' == ws]+                in D $ fromListWith (+) [(s, p / weight dpws) | (s, p) <- toList $ runD dpws]++    multiply :: (Ord s) => (Dist o, o -> Dist s) -> Dist (Dist s)+    multiply (d, f') = fmap f' d++-- | Calculate Bayes Vulnerability for a distribution.+bayesVuln :: Ord a => Dist a -> Prob+bayesVuln = maximum . elems . runD . reduction++-- | Based on an entropy function for distributions, calculate the+-- average entropy for a hyper-distribution.+condEntropy :: (Dist a -> Rational) -> Dist (Dist a) -> Rational+condEntropy e m = average (fmap e m) where+  -- | Average a distribution of Rationals.+  average :: Dist Rational -> Rational+  average d = sum [r * p | (r, p) <- toList $ runD d]

+ src/Language/Kuifje/Syntax.hs view

@@ -0,0 +1,52 @@+{-# OPTIONS_GHC -Wall #-}++{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE TypeOperators #-}++module Language.Kuifje.Syntax where++import Data.Semigroup++import Language.Kuifje.Distribution++-- | Kleisli arrow.+type a ~> b = a -> Dist b++-- | Syntax of the Kuifje language.+data Kuifje s+  = Skip+  | Update (s ~> s) (Kuifje s)+  | If (s ~> Bool) (Kuifje s) (Kuifje s) (Kuifje s)+  | While (s ~> Bool) (Kuifje s) (Kuifje s)+  | forall o. (Ord o) => Observe (s ~> o) (Kuifje s)++instance Semigroup (Kuifje s) where+  Skip        <> k = k+  Update f p  <> k = Update f (p <> k)+  While c p q <> k = While c p (q <> k)+  If c p q r  <> k = If c p q (r <> k)+  Observe f p <> k = Observe f (p <> k)++instance Monoid (Kuifje s) where+  mempty = Skip+  mappend = (<>)++-- | Return a 'Skip' instruction.+skip :: Kuifje s+skip = Skip++-- | Return an 'Update' instruction.+update :: (s ~> s) -> Kuifje s+update f = Update f skip++-- | Return a 'While' instruction.+while :: (s ~> Bool) -> Kuifje s -> Kuifje s+while c p = While c p skip++-- | Return an 'If' instruction.+cond :: (s ~> Bool) -> Kuifje s -> Kuifje s -> Kuifje s+cond c p q = If c p q skip++-- | Return an 'Observe' instruction.+observe :: (Ord o) => (s ~> o) -> Kuifje s+observe o = Observe o skip