{-# LANGUAGE Trustworthy #-}

{- | This is the __trusted__ code written by Alice (marked as @Trustworthy@), and uses Bob's untrusted code
     (marked as @Safe@). Alice code forces Bob's code to use the 'Sec' and 'SecIO' monads to guarantee that
     passwords are not leaked.

     Alice's code provides that following functionality:
        * Add a user to the database. For that feature, Bob's code must fullfil the security policy non-interference.
        * Report the average length of passwords in the system. In this case, Bob's code is allowed to reveal the average
          length of passwords.
-}
module Alice where

import SecLib.TCB.Sec
import SecLib.SecIO
import SecLib.TCB.Ref
import SecLib.Reveal

import Data.IORef

import SecLib.LowHigh

import Bob (strength, existsUser, updateDB, avgPass)

{- |
   The user names are considered public, while the password (or hashes) secret.
-}
type DB = [(Sec L String, Sec H String)]

{- |
   Alice asks for a user password and calls Bob's code to check if it is
   a strong password.
-}
password :: IO String
password = do putStr "Please, select your password:"
              pass <- getLine
              -- Protecting the password
              let spass = return pass :: Sec H String
              -- Calling Bob's code
              let eval  = strength spass
              -- Removing the data from the Sec monad (this is trustworthy code)
              if (unsec eval) then return pass
              else do putStrLn "Password not strong enough!"
                      password

{- |
   Alice asks for a user name and calls Bob's code to verify that it is indeed new.
   The function takes a reference for performance issues.
-}
adduser_menu :: IORef DB -> IO ()
adduser_menu db = do putStr "Choose a username:"
                     user <- getLine
                     let secdb   = tcbRef db :: Ref L DB
                     sec_bool <- run $ existsUser secdb user
                     case unsec sec_bool of
                          True  -> putStrLn "User taken!" >> adduser_menu db
                          -- Calling Bob's code to upgrade the database
                          False -> do -- Choose password
                                     pass <- password
                                     -- Username is considered public
                                     let secuser = return user :: Sec L String
                                     let secpass = return pass :: Sec H String
                                     -- Calling bob's side-effectful code
                                     run (updateDB secdb secuser secpass)
                                     return ()

{- |
   It uses reveal to build a secure espace hatch (downgrade operation).
   This function reveals only the average of the passwords.
-}
passAvg :: Sec H [String] -> Sec L Int
passAvg ps = do let p = public $ reveal ps
                return $ (sum (map length p)) `div` (length p)

report_security :: IORef DB -> IO ()
report_security  db = let secdb = tcbRef db :: Ref L DB
                      in do -- Bob's code which will use declassification
                            secb <- run $ avgPass secdb passAvg
                            let b = public secb
                            if b then putStrLn "Passwords are very strong!"
                            else putStrLn $ "Passwords are OK"

main :: IO ()
main = do putStrLn "Welcome to a very simple user administration interface"
          ref <- newIORef []
          loop ref

loop :: IORef DB -> IO ()
loop ref = do putStrLn "Menu:"
              putStrLn "1-Add user to the system"
              putStrLn "2-Report overall security of passwords"
              putStrLn "3-Exit"
              str <- getLine
              let number = read str :: Int
              case number of
                   1 -> adduser_menu ref >> loop ref
                   2 -> report_security ref >> loop ref
                   3 -> putStrLn "Goodbye!" >> return ()
                   _ -> putStrLn "Invalid option!" >> loop ref