{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleContexts #-}

-- | Provide security for computations involving side-effects. 
module SecLib.SecIO where

import SecLib.Lattice
import SecLib.Sec 


import Data.IORef
import Network.Socket

-- Monad

{-| This type represents secure side-effect computations. 
    These computations perform side-effects at security level, at least, @s@ and return
    a value of type @a@ with confidentiality level, at least, @s@.
-}
newtype SecIO s a = MkSecIO (IO (Sec s a))

instance Functor (SecIO s) where
  h `fmap` (MkSecIO io) = MkSecIO ( do sec <- io
                                       return (h `fmap` sec) )


instance Monad (SecIO s) where
  return x =
    MkSecIO (return (return x))
  
  MkSecIO m >>= k =
    MkSecIO (do sa <- m
                let MkSecIO m' = k (reveal sa)
                m')

-- SecIO functions

-- | Lift a pure confidential value into a secure side-effect computation. 
value :: Sec s a -> SecIO s a
value sa = MkSecIO (return sa)


-- | Execute secure computations.
run :: SecIO s a -> IO (Sec s a)
run (MkSecIO m) = m

-- | Safely downgrade the security level indicating the side-effects performed by the computation. 
plug :: Less sl sh => SecIO sh a -> SecIO sl (Sec sh a)
plug secio_sh@(MkSecIO m) = less sl sh `seq` secio_sl
                            where 
                                 (secio_sl) = MkSecIO (do sha <- m
                                                          return (sec sha))
                                 sl = unSecIOType secio_sl
                                 sh = unSecIOType secio_sh

-- | Internal function, not exported. For type-checking purposes.
unSecIOType :: SecIO s a -> s   
unSecIOType _ = undefined

-- | Break the abstraction provided by 'SecIO'. It is used only in trustworthy code!
revealIO :: SecIO s a -> IO (Sec s a)
revealIO (MkSecIO io) = io


{-| 
    Represent secure locations.
    This data type is internally used to easily introduce new side-effects into this module.
    Type @t@ is the raw type needed to perform side-effects. For instance, 
    @t@ is 'FilePath' for files and @'IORef' a@ for references. Type @s@ is the confidentiality level of the 
    location. Type @a@ is the type of values written and read form @t@. 
-}
data Loc t s a b = MkLoc t


{-| Introduce the underlining operations for reading and writing values of type @a@ provided 
    the type @t@.
-}
class UnsecureRW t a b | t -> a b where
   unsec_write :: t -> a -> IO b 
   unsec_read  :: t -> IO a       

{-| Introduce safe read and write operations for locations of type @'Loc' t s a@.
    This class acts as a wrapper for the type class @'UnsecureRW'@.
-}
class UnsecureRW t a b => SecureRW t s a b where
   {-| It provides a secure read operation when reading values might be visible 
       for the attacker (from inside of the program). 
       For example, reading from a channel in a network communication changes the 
       buffer pointer for that channel, which can be exploited to leak information. 
   -}
   effectful_read  :: Loc t s a b -> SecIO s a
   {-| It provides a secure read operation when reading values is not observable by the attacker. 
       For example, reading from references does not produce any observable effect.
   -}
   effectless_read :: Loc t s a b -> SecIO s' (Sec s a)
   -- | It provides a secure write operation.
   effectful_write :: Loc t s a b -> a -> SecIO s b



instance UnsecureRW t a b => SecureRW t s a b where
    effectless_read (MkLoc loc)   = MkSecIO ( (sec.sec) `fmap` unsec_read loc)
    effectful_read  (MkLoc loc)   = MkSecIO (sec `fmap` (unsec_read loc))
    effectful_write (MkLoc loc) a = MkSecIO (sec `fmap` (unsec_write loc a))



-- | Locations that represent files   
type File s = Loc FilePath s String ()

instance UnsecureRW FilePath String () where
   unsec_read file      = readFile file
   unsec_write file str = writeFile file str


-- | Secure read operation for files.
readFileSecIO  :: File s -> SecIO s' (Sec s String)
readFileSecIO  = effectless_read

-- | Secure write operation for files. 
writeFileSecIO :: File s -> String -> SecIO s ()
writeFileSecIO = effectful_write
 
-- Creation of files: we do not allow that!

-- | Locations that represent references. 
type Ref s a = Loc (IORef a) s a ()

instance UnsecureRW (IORef a) a () where
   unsec_read  ref    = readIORef ref
   unsec_write ref a  = writeIORef ref a

{-| Creation of files is only allowed by trustworhty code. 
Observe that by creating a file, the 
confidentiality level of its content is being established.
Therefore, the attacker can create a public file using the name 
of a secret file and just read it! |-} 
mkFile :: FilePath -> File s 
mkFile f =  MkLoc f


-- | Secure read operation for references.
readRefSecIO  :: Ref s a -> SecIO s' (Sec s a)
readRefSecIO  = effectless_read 

-- | Secure write operation for references.
writeRefSecIO :: Ref s a -> a -> SecIO s ()
writeRefSecIO = effectful_write


{-| Secure creation of a reference. We assume that the attacker 
    has no manner to observe the side-effect of creating a reference from inside of the program, 
    for example, by inspecting the amount of free memory. At the moment, there are no such functions inside of 
    the monad 'SecIO'. Nevertheless, if there is a consideration of include, for instance, a function that returns 
    the amount of free memory in the program, then the function type of 'newIORefSecIO' needs 
    to be changed. 
-}
newIORefSecIO :: s -> a -> SecIO s' (Ref s a) 
newIORefSecIO _ a = MkSecIO ( (sec.MkLoc) `fmap` newIORef a )


{-|  Location that represents the screen-keyword. Here, we can choose between 
     a) The attacker is on the screen-keyword, which implies that when taking input 
     from the screen has an effect -- the attacker can see when the input is required. 
     Therefore, we need to implement taking input from the keyword using 'effectful_read'.
     b) The attacker is not on the screen-keyword. In this case, we implement 
     reading using 'effectless_read'. We choose option a) as a model.
-}
type Screen s = Attacker s => Loc () s String ()

{-| It sets the security level of the standard input/output 
(usually the keyboard/screen).
To be used only by trustworthy code. |-} 
mkScreen :: () -> Screen s  
mkScreen _ =  MkLoc ()
 


instance UnsecureRW () String () where
   unsec_read  _    = getLine 
   unsec_write _ a  = putStr a


-- | Secure input from the keyword.
getLineSecIO  :: Attacker s => Screen s -> SecIO s String
getLineSecIO scr = observe s `seq` m 
                   where m = effectful_read scr 
                         s = unSecIOType m

-- | Secure output to the screen.
putStrSecIO :: Attacker s => Screen s -> String -> SecIO s ()
putStrSecIO scr str = observe s `seq` m
                      where m = effectful_write scr str
                            s = unSecIOType m

-- | Secure output to the screen.
putStrLnSecIO :: Attacker s => Screen s -> String -> SecIO s ()
putStrLnSecIO scr str = putStrSecIO scr (str++"\n")


-- | It is a derived operation for reading from files (legacy code).
s_read :: Less s' s => File s' -> SecIO s String
s_read file =
   do ss <- readFileSecIO file
      value (up ss)

-- | It is a derived operation for writing into files (legacy code).
s_write :: Less s s' => File s' -> String -> SecIO s (Sec s' ())
s_write file s = plug (writeFileSecIO file s)



{------------------------------------
 --- Network operations
-------------------------------------}

-- | Locations that represent network communications via sockets. 
type SecSocket s   = Loc (Socket,Int) s String Int  


-- | It defines a socket address at confidentiality level @s@.
data SecSockAddr s = MkSockAddr SockAddr

-- | Wrapper for 'inet_addr'.
inet_addrSecIO :: String -> SecIO s HostAddress
inet_addrSecIO s = MkSecIO $ (return `fmap` (inet_addr s))


-- | Assing a port to the 'AF_INET' sockets. Port numbers are public. 
portInet :: PortNumber -> SecSockAddr s -> SecSockAddr s 
portInet p (MkSockAddr (SockAddrInet port host)) = (MkSockAddr (SockAddrInet p host)) 


{- | Create a socket at confidentiality level @s@. The creation has no visible side-effects, e.g. 
     sockets cannot be compared. This function is essentially a wrapper for 'socket'.
-} 
socketSecIO :: Family -> SocketType -> ProtocolNumber -> 
               SecIO s' (SecSocket s)
socketSecIO f s p =  MkSecIO ( (sec.(\s -> MkLoc (s,0))) `fmap` socket f s p)


-- Question: it might be that it is possible to return 
-- SecIO s' () if it is the case that sIsBoundSecIO is the 
-- only observer if a socket is bind or not.

{- Bind a socket to a given address. It is considered an observable operation since the attacker 
   can observe if the 
   socket is bound by calling 'sIsBoundSecIO'. 
-}
bindSocketSecIO :: SecSocket s -> SecSockAddr s -> SecIO s ()
bindSocketSecIO (MkLoc (s,_)) (MkSockAddr address) = 
                 MkSecIO (sec `fmap` bindSocket s address) 


-- | Return if a socket is bound to some address.
sIsBoundSecIO :: SecSocket s -> SecIO s' (Sec s Bool)
sIsBoundSecIO (MkLoc (s,_)) = MkSecIO (sec `fmap` (sec `fmap` sIsBound s)) 


-- | Wrapper for 'accept'.  
acceptSecIO :: SecSocket s -> SecIO s (SecSocket s, SecSockAddr s)
acceptSecIO (MkLoc (s,_)) = MkSecIO (sec `fmap` m)
                            where m = do (sock, addr) <- accept s   
                                         return (MkLoc (sock,0), MkSockAddr addr)


instance UnsecureRW (Socket,Int) String Int where
  unsec_read  (sock,n)     = recv sock n  
  unsec_write (sock,_) str = send sock str   


-- | Secure read operation for sockets. 
recvSecIO :: SecSocket s -> Int -> SecIO s String
recvSecIO (MkLoc (s,_)) n   = effectful_read (MkLoc (s,n))

-- | Secure write operation for sockets. 
sendSecIO :: SecSocket s -> String -> SecIO s Int
sendSecIO = effectful_write 

-- | Connects to a socket. It is a wrapper for 'connect'.
connectSecIO :: SecSocket s -> SecSockAddr s -> SecIO s ()
connectSecIO (MkLoc (s,_)) (MkSockAddr sa) = MkSecIO (sec `fmap` connect s sa) 


-- | Determines a given socket is connected. It is a wrapper for 'sIsConnected'.
sIsConnectedSecIO :: SecSocket s -> SecIO s' (Sec s Bool)
sIsConnectedSecIO (MkLoc (s,_)) = MkSecIO (sec `fmap` (sec `fmap` sIsConnected s))