dclabel-0.0.4: tests/Tests.hs
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Main (main) where
import Test.Framework (Test, defaultMain)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.QuickCheck
import Control.Monad (liftM)
import DCLabel.TCB
import DCLabel.Secrecy
import DCLabel.Integrity
import Data.List (tails)
import Data.Serialize
instance Arbitrary Principal where
arbitrary = do p <- oneof $ map return ["A", "B", "C"]
return $ principal p
instance Arbitrary Disj where
arbitrary = sized disjunction
where disjunction 0 = return $ MkDisj { disj = [] }
disjunction n = do a <- arbitrary
m <- choose (0, n-1)
djs <- disjunction m
return $ MkDisj $ a:(disj djs)
instance Arbitrary Conj where
arbitrary = sized conjunction
where conjunction 0 = oneof [return $ MkConj { conj = [] } ,
return $ MkConj { conj = [MkDisj []] },
return $ MkConj { conj = [MkDisj [], MkDisj []] } ]
conjunction n = do a <- arbitrary
m <- choose (0, n-1)
cjs <- conjunction m
return $ MkConj $ a:(conj cjs)
shrink (MkConj ls) = [MkConj ll | l <- tails ls, ll <- shrink l]
instance Arbitrary Component where
arbitrary = do m <- choose (0, 1) :: Gen Int
if m==0 then mkArbLbl arbitrary
else return MkComponentAll
where mkArbLbl :: Gen Conj -> Gen Component
mkArbLbl = liftM MkComponent
instance Arbitrary (SLabel) where
arbitrary = do s <- arbitrary
return $ MkSLabel s
instance Arbitrary (ILabel) where
arbitrary = do s <- arbitrary
return $ MkILabel s
instance Arbitrary DCLabel where
arbitrary = do s <- arbitrary
i <- arbitrary
return $ MkDCLabel { secrecy = s, integrity = i }
instance Arbitrary TCBPriv where
arbitrary = do p <- arbitrary
return $ MkTCBPriv p
-- cleanComponent does not modify the semantics of the label
prop_cleanComponent :: Component -> Bool
prop_cleanComponent l = let l' = cleanComponent l
in l `implies` l' && l' `implies` l
-- Reduction function toLNF does not modify the semantics of the label
prop_toLNF :: Component -> Bool
prop_toLNF l = let l' = toLNF l
in l `implies` l' && l' `implies` l
-- Idempotenncy of toLNF
prop_toLNF_idem :: Property
prop_toLNF_idem = forAll (arbitrary :: Gen Component) $ \l->
let l' = toLNF l
l'' = toLNF l'
in l' == l''
-- Partial order for DCLabels
prop_dc_porder :: (DCLabel, DCLabel) -> Bool
prop_dc_porder (l1,l2) = let l1' = toLNF l1
l2' = toLNF l2
ge = l1' `canflowto` l2'
le = l2' `canflowto` l1'
eq = l2' == l1'
in (eq && ge && le) || -- ==
((not eq) && (ge || le) && (ge /= le)) || -- < or >
(not (eq || ge || le)) -- incomparable
-- Check that labels flow to their join for DCLabels
prop_DC_join :: (DCLabel, DCLabel) -> Bool
prop_DC_join (l1,l2) = let l3 = l1 `join` l2
t1 = l1 `canflowto` l3
t2 = l2 `canflowto` l3
in t1 && t2
-- Check that join is the least upper bound for DCLabels
-- TODO: we need to fix this since it is difficult to satisfy the
-- hypothesis.
prop_dc_join_lub :: (DCLabel, DCLabel) -> Property
prop_dc_join_lub (l1,l2) = forAll (arbitrary :: Gen DCLabel) $ \l3' ->
(l1 `canflowto` l3') && (l2 `canflowto` l3') ==> (l1 `join` l2) `canflowto` l3'
-- Check that meet flows to the labels making it, for DCLabels
prop_dc_meet :: (DCLabel, DCLabel) -> Bool
prop_dc_meet (l1,l2) = let l3 = l1 `meet` l2
t1 = l3 `canflowto` l1
t2 = l3 `canflowto` l2
in t1 && t2
-- Check that meet the greatest lower bound for DCLabels
prop_dc_meet_glb :: (DCLabel, DCLabel) -> Property
prop_dc_meet_glb (l1,l2) = forAll (arbitrary :: Gen DCLabel) $ \l3' ->
(l3' `canflowto` l1) && (l3' `canflowto` l2) ==> l3' `canflowto` (l1 `meet` l2)
-- Check that the top is indeed indeed the highest element in the lattice
prop_dc_top :: DCLabel -> Property
prop_dc_top l1 = forAll (gen l1) $ \l -> l `canflowto` top
where gen :: DCLabel -> Gen DCLabel
gen _ = arbitrary
-- Check that the bottom is indeed indeed the lowest element in the lattice
prop_dc_bottom :: DCLabel -> Property
prop_dc_bottom _ = forAll (arbitrary :: Gen DCLabel) $ \l -> bottom `canflowto` l
-- LIO's lostar
lostar :: TCBPriv -> DCLabel -> DCLabel -> DCLabel
lostar p l g =
let (ls, li) = (toLNF . secrecy $ l, toLNF . integrity $ l)
(gs, gi) = (toLNF . secrecy $ g, toLNF . integrity $ g)
lp = toLNF $ priv p
rs' = c2l [c | c <- getCats ls
, not (lp `implies` (c2l [c]))]
rs'' = c2l [c | c <- getCats gs
, not (rs' `implies` (c2l [c]))]
rs = if ls == allComponent || gs == allComponent
then allComponent
else rs' `and_component` rs''
ri = (li `and_component` lp) `or_component` gi
in toLNF $ simpleNewComponent p (newDC rs ri)
where getCats = conj . component
c2l = MkComponent . MkConj
simpleNewComponent pr lr | pr == rootPrivTCB = g
| pr == noPriv = l `join` g
| otherwise = lr
{-
lr = lostar p li lg satisfies:
- canflowto lg lr
- canflowto_p p li lr
- lr is the greatest lower bound
-}
prop_lostar :: TCBPriv -> DCLabel -> DCLabel -> Property
prop_lostar p li lg =
let lr = lostar p li lg
in forAll (arbitrary :: Gen DCLabel) $ \lr' ->
canflowto lg lr &&
canflowto_p p li lr &&
not ( canflowto lg lr' &&
canflowto_p p li lr' &&
lr' /= lr &&
canflowto lr' lr)
-- | Test serialization.
prop_DC_serialize :: DCLabel -> Bool
prop_DC_serialize l = case decode (encode l) of
Left _ -> False
Right l' -> l == l'
main :: IO ()
main = defaultMain tests
tests :: [Test]
tests = [
testProperty "cleanComponent" (prop_cleanComponent :: Component -> Bool)
, testProperty "toLNF" (prop_toLNF :: Component -> Bool)
, testProperty "Idempotence of function toLNF" (prop_toLNF_idem :: Property)
, testProperty "Property of top" (prop_dc_top :: DCLabel -> Property)
, testProperty "Property of bottom" (prop_dc_bottom :: DCLabel -> Property)
, testProperty "Join operation" (prop_DC_join :: (DCLabel, DCLabel) -> Bool)
, testProperty "Join operation is the least upper bound"
(prop_dc_join_lub :: (DCLabel, DCLabel) -> Property)
, testProperty "Meet operation" (prop_dc_meet :: (DCLabel, DCLabel) -> Bool)
, testProperty "Meet operation is the greatest lower bound"
(prop_dc_meet_glb :: (DCLabel, DCLabel) -> Property)
, testProperty "DC labels form a partial order"
(prop_dc_porder :: (DCLabel, DCLabel) -> Bool)
, testProperty "lostar implementation"
(prop_lostar :: TCBPriv -> DCLabel -> DCLabel -> Property)
, testProperty "Serialization of DC labels"
(prop_DC_serialize :: DCLabel -> Bool)
]