{-# OPTIONS_GHC -Wall -Werror #-}

{-# LANGUAGE NoGeneralizedNewtypeDeriving #-}
{-# LANGUAGE Safe                         #-}

--------------------------------------------------------------------------------

-- |
-- Copyright  : (c) 2026 SPISE MISU ApS
-- License    : SSPL-1.0 OR AGPL-3.0-only
-- Maintainer : SPISE MISU <mail+hackage@spisemisu.com>
-- Stability  : experimental
--
-- Mandatory Access Control (MAC)
--
-- https://en.wikipedia.org/wiki/Mandatory_access_control
--
-- In computer security, mandatory access control (MAC) refers to a type of
-- access control by which the operating system or database constrains the
-- ability of a subject or initiator to access or generally perform some sort of
-- operation on an object or target.[1] In the case of operating systems, a
-- subject is usually a process or thread; objects are constructs such as files,
-- directories, TCP/UDP ports, shared memory segments, IO devices, etc. Subjects
-- and objects each have a set of security attributes. Whenever a subject
-- attempts to access an object, an authorization rule enforced by the operating
-- system kernel examines these security attributes and decides whether the
-- access can take place. Any operation by any subject on any object is tested
-- against the set of authorization rules (aka policy) to determine if the
-- operation is allowed. A database management system, in its access control
-- mechanism, can also apply mandatory access control; in this case, the objects
-- are tables, views, procedures, etc.
--
-- With mandatory access control, this security policy is centrally controlled
-- by a security policy administrator; users do not have the ability to override
-- the policy and, for example, grant access to files that would otherwise be
-- restricted. By contrast, discretionary access control (DAC), which also
-- governs the ability of subjects to access objects, allows users the ability
-- to make policy decisions and/or assign security attributes. (The traditional
-- Unix system of users, groups, and read-write-execute permissions is an
-- example of DAC.) MAC-enabled systems allow policy administrators to implement
-- organization-wide security policies. Under MAC (and unlike DAC), users cannot
-- override or modify this policy, either accidentally or intentionally. This
-- allows security administrators to define a central policy that is guaranteed
-- (in principle) to be enforced for all users.
--
-- [1] Belim, S. V.; Belim, S. Yu. (December 2018). "Implementation of Mandatory
-- Access Control in Distributed Systems". Automatic Control and Computer
-- Sciences. 52 (8): 1124–1126. doi:10.3103/S0146411618080357. ISSN 0146-4116.

--------------------------------------------------------------------------------

module Agent.Control.MAC
  ( MAC (MAC, run)
  , UID (UID, uid)
  , RES (RES, res)
  , join
  , label
  , unlabel
  , value
  )
where

--------------------------------------------------------------------------------

import           Control.Monad     ( ap, liftM )

import           Control.Exception ( Exception, SomeException )
import qualified Control.Exception as Ex

import           Agent.Control.IFC ( Flow )

--------------------------------------------------------------------------------

newtype MAC p a = MAC { forall p a. MAC p a -> IO a
run :: IO a }

instance Monad (MAC p) where
  >>= :: forall a b. MAC p a -> (a -> MAC p b) -> MAC p b
(>>=) MAC p a
m a -> MAC p b
f = IO b -> MAC p b
forall p a. IO a -> MAC p a
MAC (IO b -> MAC p b) -> IO b -> MAC p b
forall a b. (a -> b) -> a -> b
$ MAC p a -> IO a
forall p a. MAC p a -> IO a
run MAC p a
m IO a -> (a -> IO b) -> IO b
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= MAC p b -> IO b
forall p a. MAC p a -> IO a
run (MAC p b -> IO b) -> (a -> MAC p b) -> a -> IO b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> MAC p b
f

instance Applicative (MAC p) where
  pure :: forall a. a -> MAC p a
pure  = IO a -> MAC p a
forall p a. IO a -> MAC p a
MAC (IO a -> MAC p a) -> (a -> IO a) -> a -> MAC p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IO a
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  <*> :: forall a b. MAC p (a -> b) -> MAC p a -> MAC p b
(<*>) = MAC p (a -> b) -> MAC p a -> MAC p b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Functor (MAC p) where
  fmap :: forall a b. (a -> b) -> MAC p a -> MAC p b
fmap = (a -> b) -> MAC p a -> MAC p b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

--------------------------------------------------------------------------------

-- UID: Unique identifier
-- RES: Resource
-- LAB: Label

newtype UID   a = UID   { forall a. UID a -> a
uid :: a }
newtype RES p a = RES   { forall p a. RES p a -> a
res :: a }
type    LAB p a = RES p ( UID    a )

--------------------------------------------------------------------------------

value
  :: LAB l a
  -> a
value :: forall l a. LAB l a -> a
value =
  UID a -> a
forall a. UID a -> a
uid (UID a -> a) -> (LAB l a -> UID a) -> LAB l a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LAB l a -> UID a
forall p a. RES p a -> a
res

label
  :: Flow l h
  => a
  -> MAC l (LAB h a)
label :: forall l h a. Flow l h => a -> MAC l (LAB h a)
label =
  IO (UID a) -> MAC l (RES h (UID a))
forall {a} {p} {p}. IO a -> MAC p (RES p a)
aux (IO (UID a) -> MAC l (RES h (UID a)))
-> (a -> IO (UID a)) -> a -> MAC l (RES h (UID a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UID a -> IO (UID a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UID a -> IO (UID a)) -> (a -> UID a) -> a -> IO (UID a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> UID a
forall a. a -> UID a
UID
  where
    aux :: IO a -> MAC p (RES p a)
aux IO a
io = a -> RES p a
forall p a. a -> RES p a
RES (a -> RES p a) -> MAC p a -> MAC p (RES p a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO a -> MAC p a
forall p a. IO a -> MAC p a
MAC IO a
io

unlabel
  :: Flow l h
  => LAB l a
  -> MAC h a
unlabel :: forall l h a. Flow l h => LAB l a -> MAC h a
unlabel =
  (UID a -> IO a) -> RES l (UID a) -> MAC h a
forall {b} {a} {p} {p}. (b -> IO a) -> RES p b -> MAC p a
aux ((UID a -> IO a) -> RES l (UID a) -> MAC h a)
-> (UID a -> IO a) -> RES l (UID a) -> MAC h a
forall a b. (a -> b) -> a -> b
$ a -> IO a
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> IO a) -> (UID a -> a) -> UID a -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UID a -> a
forall a. UID a -> a
uid
  where
    aux :: (b -> IO a) -> RES p b -> MAC p a
aux b -> IO a
io = IO a -> MAC p a
forall p a. IO a -> MAC p a
MAC (IO a -> MAC p a) -> (RES p b -> IO a) -> RES p b -> MAC p a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> IO a
io (b -> IO a) -> (RES p b -> b) -> RES p b -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RES p b -> b
forall p a. RES p a -> a
res

join
  :: Flow l h
  => MAC h        a
  -> MAC l (LAB h a)
join :: forall l h a. Flow l h => MAC h a -> MAC l (LAB h a)
join MAC h a
m =
  (IO a -> MAC l a
forall p a. IO a -> MAC p a
MAC (IO a -> MAC l a) -> (MAC h a -> IO a) -> MAC h a -> MAC l a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MAC h a -> IO a
forall p a. MAC p a -> IO a
run) (MAC h a -> MAC h a
forall {l} {a}. MAC l a -> MAC l a
aux MAC h a
m) MAC l a -> (a -> MAC l (LAB h a)) -> MAC l (LAB h a)
forall a b. MAC l a -> (a -> MAC l b) -> MAC l b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> MAC l (LAB h a)
forall l h a. Flow l h => a -> MAC l (LAB h a)
label
  where
    aux :: MAC l a -> MAC l a
aux MAC l a
x = MAC l a -> (SomeException -> MAC l a) -> MAC l a
forall e l a. Exception e => MAC l a -> (e -> MAC l a) -> MAC l a
catch MAC l a
x SomeException -> MAC l a
forall l a. SomeException -> MAC l a
throw

--------------------------------------------------------------------------------

-- HELPERS

throw
  :: SomeException
  -> MAC l a
throw :: forall l a. SomeException -> MAC l a
throw =
  IO a -> MAC l a
forall p a. IO a -> MAC p a
MAC (IO a -> MAC l a)
-> (SomeException -> IO a) -> SomeException -> MAC l a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeException -> IO a
forall a e. Exception e => e -> a
Ex.throw

catch
  :: Exception e
  =>       MAC l a
  -> (e -> MAC l a)
  ->       MAC l a
catch :: forall e l a. Exception e => MAC l a -> (e -> MAC l a) -> MAC l a
catch (MAC IO a
io) e -> MAC l a
f =
  IO a -> MAC l a
forall p a. IO a -> MAC p a
MAC (IO a -> MAC l a) -> IO a -> MAC l a
forall a b. (a -> b) -> a -> b
$ IO a -> (e -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
Ex.catch IO a
io ((e -> IO a) -> IO a) -> (e -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ MAC l a -> IO a
forall p a. MAC p a -> IO a
run (MAC l a -> IO a) -> (e -> MAC l a) -> e -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> MAC l a
f