Operation: chobjsc

• This operation changes the security class of a given object.
• The only users allowed to execute this operations are the Security Administrators (secadm), in other words those belonging to SecAdmGrp group.

Section Chobjsc.



Variable s: SFSstate.



Some preliminary definitions



Definition chobjsc_SC
 [o:OBJECT; sc:SecClass] : (set OBJECT*SecClass) :=

 Cases (fOSC (objectSC s) o) of
  |None => (objectSC s)
  |(Some y) => (set_add OSCeq_dec
                         (o,sc)
                         (set_remove OSCeq_dec (o,y) (objectSC s)))
 end.



Next state definition

Local t [o:OBJECT; sc:SecClass]: SFSstate :=

   (mkSFS (groups s) (primaryGrp s) (subjectSC s) (AllGrp s)
          (RootGrp s) (SecAdmGrp s) (chobjsc_SC o sc) (acl s)
          (secmat s) (files s) (directories s)).




Operation definition

Inductive chobjsc
  [secadm:SUBJECT; o:OBJECT; sc:SecClass] : SFSstate -> Prop :=

  |chsobjscOK:
      (set_In secadm ((groups s) (SecAdmGrp s)))
      ->~(set_In o (domsecmat (secmat s)))
      ->(chobjsc secadm o sc (t o sc)).



End Chobjsc.

Hints Unfold chobjsc_SC.