Theory Step

subsection ‹Separation kernel state and atomic step function›

theory Step
  imports Step_policies
begin


subsubsection ‹Interrupt points›

text ‹To model concurrency, each system call is split into several atomic steps,
        while allowing interrupts between the steps. The state of a thread is
        represented by an ``interrupt point" (which corresponds to the value of the program counter
        saved by the system when a thread is interrupted).›

datatype ipc_direction_t = SEND | RECV
datatype ipc_stage_t = PREP | WAIT | BUF page_t

datatype ev_consume_t = EV_CONSUME_ALL | EV_CONSUME_ONE
datatype ev_wait_stage_t = EV_PREP | EV_WAIT | EV_FINISH
datatype ev_signal_stage_t = EV_SIGNAL_PREP | EV_SIGNAL_FINISH

datatype int_point_t =
   SK_IPC ipc_direction_t ipc_stage_t thread_id_t page_t ― ‹The thread is executing a sending / receiving IPC.›
 | SK_EV_WAIT ev_wait_stage_t ev_consume_t ― ‹The thread is waiting for an event.›
 | SK_EV_SIGNAL ev_signal_stage_t thread_id_t ― ‹The thread is sending an event.›
 | NONE ― ‹The thread is not executing any system call.›

subsubsection ‹System state›

typedecl obj_t ― ‹value of an object›

text ‹Each thread belongs to a partition. The relation is fixed (in this instantiation of a separation kernel).›

consts
  partition :: "thread_id_t ⇒ partition_id_t"

text ‹The state contains the dynamic policy (the communication rights in the current state
  of the system, for example).›

record thread_t =
  (* 
  id :: thread_id_t           -- {* thread identifier *}
  int_point :: int_point_t    -- {* interrupt point *}*)
  ev_counter :: nat           ― ‹event counter›
  
record state_t =  
  sp_impl_subj_subj :: sp_subj_subj_t    ― ‹current subject-subject policy›
  sp_impl_subj_obj :: sp_subj_obj_t      ― ‹current subject-object policy›
  current :: "thread_id_t"               ― ‹current thread›
  obj :: "obj_id_t ⇒ obj_t"             ― ‹values of all objects›
  thread :: "thread_id_t ⇒ thread_t"    ― ‹internal state of threads›

text ‹Later (Section~\ref{sect:step_invariants}), the system invariant @{term sp_subset} will be used to ensure that the dynamic policies (sp\_impl\_...)
are a subset of the corresponding static policies (sp\_spec\_...).›

subsubsection ‹Atomic step›

text_raw ‹\paragraph{Helper functions}›

text ‹Set new value for an object.›

definition set_object_value :: "obj_id_t ⇒ obj_t ⇒ state_t ⇒ state_t" where
  "set_object_value obj_id val s =
    s ⦇ obj := fun_upd (obj s) obj_id val ⦈"

text ‹Return a representation of the opposite direction of IPC communication.›

definition opposite_ipc_direction :: "ipc_direction_t ⇒ ipc_direction_t" where
  "opposite_ipc_direction dir ≡ case dir of SEND ⇒ RECV | RECV ⇒ SEND"

text ‹Add an access right from one partition to an object. In this model, not 
available from the API, but shows how dynamic changes of access rights could be implemented.›

definition add_access_right :: "partition_id_t => obj_id_t => mode_t => state_t => state_t" where
  "add_access_right part_id obj_id m s = 
    s ⦇ sp_impl_subj_obj := λ q q' q''. (part_id = q ∧ obj_id = q' ∧ m = q'') 
     ∨ sp_impl_subj_obj s q q' q''⦈"

text ‹Add a communication right from one partition to another. In this model, not
available from the API.›

definition add_comm_right :: "partition_id_t ⇒ partition_id_t ⇒ state_t ⇒ state_t" where
  "add_comm_right p p' s ≡
    s ⦇ sp_impl_subj_subj := λ q q' . (p = q ∧ p' = q') ∨ sp_impl_subj_subj s q q' ⦈"

text_raw ‹\paragraph{Model of IPC system call}›

text ‹We model IPC with the following simplifications:

\begin{enumerate}
\item The model contains the system calls for sending 
      an IPC (SEND) and receiving an IPC (RECV), often implementations
      have a richer API (e.g. combining SEND and RECV in one invocation). 
\item We model only a copying (``BUF") mode, not a memory-mapping mode.
\item The model always copies one page per syscall.
\end{enumerate}
›

definition ipc_precondition :: "thread_id_t ⇒ ipc_direction_t ⇒ thread_id_t ⇒ page_t ⇒ state_t ⇒ bool" where
  "ipc_precondition tid dir partner page s ≡
    let sender = (case dir of SEND ⇒ tid | RECV ⇒ partner) in
    let receiver = (case dir of SEND ⇒ partner | RECV ⇒ tid) in
    let local_access_mode = (case dir of SEND ⇒ READ | RECV ⇒ WRITE) in
    (sp_impl_subj_subj s (partition sender) (partition receiver)
      ∧ sp_impl_subj_obj s (partition tid) (PAGE page) local_access_mode)"

definition atomic_step_ipc :: "thread_id_t ⇒ ipc_direction_t ⇒ ipc_stage_t ⇒ thread_id_t ⇒ page_t ⇒ state_t ⇒ state_t" where
  "atomic_step_ipc tid dir stage partner page s ≡
    case stage of
      PREP ⇒
         s
    | WAIT ⇒
         s
    | BUF page' ⇒
       (case dir of
          SEND ⇒
             (set_object_value (PAGE page') (obj s (PAGE page)) s)
        | RECV ⇒ s)"

text_raw ‹\paragraph{Model of event syscalls}›

(*The maximum allowed event counter*)
(* outcommented, as currently not used consts EV_CTR_MAX :: nat *)

(* Needs to be adapted, if wildcards for masks are defined *)
definition ev_signal_precondition :: "thread_id_t ⇒ thread_id_t ⇒ state_t ⇒ bool" where
 "ev_signal_precondition tid partner s ≡
    (sp_impl_subj_subj s (partition tid) (partition partner))"

(* Assumes error checks have been successful:
   tid is in the event mask of the partner and
   communication rights between tid an partner have been granted *)
definition atomic_step_ev_signal :: "thread_id_t ⇒ thread_id_t ⇒ state_t ⇒ state_t" where
 "atomic_step_ev_signal tid partner s =
    s ⦇ thread := fun_upd (thread s) partner (thread s partner ⦇ ev_counter := Suc (ev_counter (thread s partner) ) ⦈ )   ⦈"

definition atomic_step_ev_wait_one :: "thread_id_t ⇒ state_t ⇒ state_t" where
 "atomic_step_ev_wait_one tid s =
    s ⦇ thread := fun_upd (thread s) tid (thread s tid ⦇ ev_counter := (ev_counter (thread s tid) - 1) ⦈ )   ⦈"

definition atomic_step_ev_wait_all :: "thread_id_t ⇒ state_t ⇒ state_t" where
 "atomic_step_ev_wait_all tid  s =
    s ⦇ thread := fun_upd (thread s) tid (thread s tid ⦇ ev_counter := 0 ⦈ )   ⦈"

text_raw ‹\paragraph{Instantiation of CISK aborting and waiting}›

text ‹
  In this instantiation of CISK, the @{term aborting} function is used to indicate security policy enforcement.
  An IPC call aborts in its @{term PREP} stage if the precondition for the calling thread does 
  not hold. An event signal call aborts in its @{term EV_SIGNAL_PREP} stage if the 
  precondition for the calling thread does not hold. 
›
definition aborting :: "state_t ⇒ thread_id_t ⇒ int_point_t ⇒ bool"
where "aborting s tid a ≡ case a of SK_IPC dir PREP partner page ⇒
                            ¬ipc_precondition tid dir partner page s
                           | SK_EV_SIGNAL EV_SIGNAL_PREP partner ⇒
                            ¬ev_signal_precondition tid partner s
                           | _ => False"
text ‹
  The @{term waiting} function is used to indicate synchronization.
  An IPC call waits in its @{term WAIT} stage while the precondition for the partner thread does not hold.
  An EV\_WAIT call waits until the event counter is not zero.
›
definition waiting :: "state_t ⇒ thread_id_t ⇒ int_point_t ⇒ bool"
where "waiting s tid a ≡ 
           case a of SK_IPC dir WAIT partner page ⇒ 
                                   ¬ipc_precondition partner (opposite_ipc_direction dir) tid (SOME page' . True) s
                   | SK_EV_WAIT EV_PREP _ ⇒ False
                   | SK_EV_WAIT EV_WAIT _ ⇒ ev_counter (thread s tid) = 0
                   | SK_EV_WAIT EV_FINISH _ ⇒ False
                   | _ ⇒ False"

text_raw ‹\paragraph{The atomic step function.}›

text ‹In the definition of @{term atomic_step} the arguments to an interrupt point are
 not taken from the thread state -- the argument given to @{term atomic_step} could have an 
 arbitrary value.
 So, seen in isolation, @{term atomic_step} allows more transitions than actually occur in the 
 separation kernel. However, the CISK framework (1) restricts the atomic step function by
 the @{term waiting} and @{term aborting} functions as well (2) the set of realistic traces as
 attack sequences @{term rAS_set} (Section~\ref{sect:separation_kernel_model}). 
 An additional condition is that (3) the dynamic policy used in @{term aborting} 
 is a subset of the static policy. This is ensured by the invariant @{term sp_subset}.
›

definition atomic_step :: "state_t ⇒ int_point_t ⇒ state_t" where
  "atomic_step s ipt ≡
    case ipt of
      SK_IPC dir stage partner page ⇒
        atomic_step_ipc (current s) dir stage partner page s
    |  SK_EV_WAIT EV_PREP consume ⇒ s
    |  SK_EV_WAIT EV_WAIT consume ⇒ s
    |  SK_EV_WAIT EV_FINISH consume ⇒
      case consume of
          EV_CONSUME_ONE ⇒ atomic_step_ev_wait_one (current s) s   
        | EV_CONSUME_ALL ⇒ atomic_step_ev_wait_all (current s) s  
    | SK_EV_SIGNAL EV_SIGNAL_PREP partner ⇒ s
    | SK_EV_SIGNAL EV_SIGNAL_FINISH partner ⇒
      atomic_step_ev_signal (current s) partner s
    | NONE ⇒ s"

end