Context Relabeling Authorization

[Matt Benke <mbenke@xxxxxxxxxxxxxxxx>]

All,

I'm struggling to develop a subject-to-subject information flow model based on "Verifying Information Flow Goals in Security-Enhanced Linux" but with MLS/MCS and context relabeling.  The scrawl below depicts a potential information flow from a source subject with context x_a that invokes class c_a operation p_a on object x_o to a target subject with context x_b that invokes class c_b operation p_b on the relabeled object now with context x_o' (provided that modifications resulting from c_a.p_a are observable via c_b.p_b):


x_a -- c_a.p_a -> x_o
                   .
                   .
               (relabel)
                   .
                   v
                  x_o' <- c_b.p_b -- x_b


To account for context relabeling requires knowing which SELinux policy components enforce whether a subject with context x_s = (u_s:r_s:t_s:m_s) is allowed to relabel an object (perhaps a subject, perhaps a child process, perhaps itself) instance of class k from context x_c = (u_c:r_c:t_c:m_c) to context x_c' = (u_c':r_c':t_c':m_c').  I remain ignorant, but my reading so far suggests that the decision depends upon:

• whether the new context is valid
  (user, role, and type declaration and association statements),
  
  
• whether a role transition is allowed
  (role-allow authorization statements),
  
  
• whether the object is a subject
  (a process instance, and thus whether a domain transition or object transition is requested),
  
  
• what corresponding relabeling operations are authorized
  (type-allow authorization statements), and
  
  
• what additional constraints are in place
  ((mls)constrain and (mls)validatetrans statements)
  

But what source statements constrain relabeling of user and MLS/MCS context components, and what related basics continue to defy my limited comprehension, as bizarrely expressed below?

can_relabel(x_s, x_c, x_c') :
  valid(x_c') AND
  role_transition_allowed(r_c, r_c') AND
  satisfies_transition_constraints(k, x_s, x_c, x_c') AND
  (
    (
      k == 'process' AND
      x_s == x_c AND
      process_transition_allowed(x_c, x_c')
    ) OR
    (
      k =/= 'process' AND
      object_transition_allowed(k, x_s, x_c, x_c')
    )
  ) WHERE
  (
    valid(x_c') :
      (
        user_role_associated(u_c', r_c') AND
        role_type_associated(r_c', t_c') AND
        user_range_bounded(u_c', m_c')
      ) WHERE
      (
        user_role_associated(u, r) :
          ["user u roles r ..." is in the policy]
        ,
        role_type_associated(r, t) :
          ["role r types t" is in the policy]
        ,
        user_range_bounded(u, m) :
          ["user u ... range m'" is in the policy] AND
          [m is bounded by m']
      ) ,
    role_transition_allowed(r, r') :
      ["allow r r'" is in the policy]
    ,
    satisfies_transition_constraints(k, x_s, x_c, x_c') :
      [x_s, x_c, x_c' satisfy e for all "(mls)validatetrans k e" in the policy]
    ,
    (
      process_transition_allowed(x, x') :
        (
          operation_allowed(process.transition, x, x') AND
          EXISTS e
          (
            operation_allowed(file.execute, x, e) AND
            operation_allowed(file.entrypoint, x', e)
          )
        ) ,
      object_transition_allowed(k, s, c, c') :
        (
          operation_allowed(k.relabelfrom, s, c) AND
          operation_allowed(k'.relabelto, s, c')
        )
    ) WHERE
    (
      operation_allowed(k.p, x, x') :
      (
        ["allow t t' : k p" is in the policy] AND
        [x, x' satisfy e for all "(mls)constrain k p e" in the policy]
      )
    )
  )