Operation: stat

  • This operation outputs the UNIX security information stored in the ACL of a given object.
  • Note that in our model the only precondition for this operation is that the user has DAC read access to the object and not, as in the standard UNIX, execute access.

Require Export DACandMAC.

Implicit Arguments On.



Section Stat.



Variable s: SFSstate.

  • This function computes the object's mode from the object's ACL by searching owner, group and AllGrp in UsersReaders, UsersWriters, GroupReaders and GroupWriters. It's under-specified.


Parameter comp_mode: AccessCtrlListData -> PERMS.

  • This record stores the security attributes present in a conventinoal i-node.


Record stat_struct : Set := stat_fields
   {st_mode: PERMS;
    st_uid : SUBJECT;
    st_gid : GRPNAME}.

Operation definition



Inductive stat
  [u:SUBJECT; o:OBJECT] : SFSstate -> (Exc stat_struct) -> Prop :=

  |StatOK:
     (PreDACRead s u o)
     ->(stat u o s
             Cases (facl (acl s) o) of
              |None => (None stat_struct)
              |(Some y) =>
                     (Some stat_struct
                            (stat_fields (comp_mode y) (owner y) (group y)))
             end).



End Stat.

Index
This page has been generated by coqdoc