The state of the system

Require Export ListFunctions.


Implicit Arguments On.


When appropriate, each formal term is preceded by its interpretation or designation.

Proofs are ommited, they can be found here.




Definition of security class, and its standard partial order.

  • SECLEV: security levels
  • CATEGORY: categories, departments or need-to-know

Definition SECLEV := nat.
Parameter CATEGORY: Set.

  • SecClass: security class or access class

Record SecClass : Set := sclass
   {level : SECLEV;
    categs: (set CATEGORY)}.

  • Equality of security classes

Definition eq_sc [a,b:SecClass] : Prop :=
   (level a)=(level b)
   /\(categs a)=(categs b).

  • Standard partial order over security classes


Definition le_sc [a,b:SecClass] : Prop :=
   (le (level a) (level b))
   /\(Included (categs a) (categs b)).



Hints Unfold eq_sc le_sc.


Security Policy Subjects

This are global parameters introducing some of the basic sets of the model:

  • SUBJECT: all the subjects of the system
  • GRPNAME: all the group names of the system
  • root: UNIX superuser
  • secofr: security officer, in charge of MAC attributes


Parameter SUBJECT, GRPNAME: Set.
Parameter root, secofr: SUBJECT.


  • These axioms are needed by functions of ListSet; they are for equality decidability


Axiom SUBeq_dec : (x,y:SUBJECT){x=y}+{~x=y}.
Axiom GRPeq_dec : (x,y:GRPNAME){x=y}+{~x=y}.

Hints Resolve SUBeq_dec GRPeq_dec.


The Filesystem
  • OBJNAME: all the possible absolute path names for files and directories
  • BYTE: elements that can be stored in a file

Parameters OBJNAME, BYTE:Set.


These axioms are needed by functions of ListSet

Axiom OBJNAMEeq_dec : (x,y:OBJNAME){x=y}+{~x=y}.
Axiom BYTEeq_dec : (x,y:BYTE){x=y}+{~x=y}.

Hints Resolve OBJNAMEeq_dec BYTEeq_dec.


  • OBJTYPE: used to distinguish between files and directories

Inductive OBJTYPE: Set :=
 |File: OBJTYPE
 |Directory: OBJTYPE.

Lemma OBJTYPEeq_dec: (x,y:OBJTYPE){x=y}+{~x=y}.
Intros.
Elim x; Elim y.
Left; Auto.

Right; Intro; Discriminate H.

Right; Intro; Discriminate H.

Left; Auto.

Qed.

Hints Resolve OBJTYPEeq_dec.


  • FILECONT: all the possible contents of files

Definition FILECONT := (list BYTE).



Lemma FILECONTeq_dec: (x,y:FILECONT){x=y}+{~x=y}.
Unfold FILECONT; Intros; Apply Listeq_dec.
Auto.

Qed.



Hints Resolve FILECONTeq_dec.


  • DIRCONT: all the possible contents of directories

Definition DIRCONT := (list OBJNAME).

Lemma DIRCONTeq_dec: (x,y:DIRCONT){x=y}+{~x=y}.
Unfold DIRCONT; Intros; Apply Listeq_dec.
Auto.

Qed.



Hints Resolve DIRCONTeq_dec.

  • OBJECT: the objects managed by the system are just pairs of a name and a type

Definition OBJECT := OBJNAME*OBJTYPE.



Lemma OBJeq_dec: (x,y:OBJECT){x=y}+{~x=y}.
Unfold OBJECT.
Intros.
Apply Prodeq_dec; Auto.
Qed.


  • MyDir(o): parent directory of object o

Parameter MyDir: OBJNAME -> OBJECT.

Definition ObjName [o:OBJECT] : OBJNAME := (Fst o).

Definition ObjType [o:OBJECT] : OBJTYPE := (Snd o).



Security Policy Objects
  • (allowedTo a b):
    • if a pattern-matches (PM) true, then read access is allowed; otherwise it isn'
    • if b PM true, then write access is allowed; otherwise it isn't


Record RIGHTS : Set := allowedTo
   {read_right : bool;
    write_right: bool}.

  • (rwx o g a):
    • if o PM (allowedTo x y) then the owner has or has't read and/or write access;
    • if g PM (allowedTo x y) then group g has or has't read and/or write access;
    • if a PM (allowedTo x y) then all the system subjects has or has't read and/or write access


Record PERMS : Set := rwx
   {ownerp: RIGHTS;
    groupp: RIGHTS;
    otherp: RIGHTS}.

  • For a designation of acldata, see below

Record AccessCtrlListData : Set := acldata
   {owner: SUBJECT;
    group: GRPNAME;
    UsersReaders: (set SUBJECT);
    GroupReaders: (set GRPNAME);
    UsersWriters: (set SUBJECT);
    GroupWriters: (set GRPNAME);
    UsersOwners : (set SUBJECT);
    GroupOwners : (set GRPNAME)}.


  • For a designation of mkRW, see below.

Record ReadersWriters : Set := mkRW
   {ActReaders: (set SUBJECT);
    ActWriters: (set SUBJECT)}.

Axiom RWeq_dec : (x1,x2:ReadersWriters) {x1=x2}+{~x1=x2}.



Secure FileSystem

This record represents the state of the filesystem from the security point of view. Designations for each field:

  • (groups g): all the subjects which belong to group g
  • (primaryGrp s): the (UNIX) primary group of subject s
  • (subjectSC s u): security class of u in state s; its a FPF
  • AllGrp: group containing all the system subjects
  • SecAdmGrp: group of the security administrators in charge of MAC attributes
  • RootGrp: group of all subjects with the same access of subject root
  • (objectSC s o): security class of o in state s; its a FPF
  • (acl s o) = (acldata o g ur gr uw gw uo go): iff (acldata o g ur gr uw gw uo go) is the ACL of o in state s (its a FPF), in that case:
    • o is the UNIX owner of o,
    • g is the UNIX group of o,
    • ur is a set of subjects with read access to o,
    • gr is a set of groups with read access to o,
    • uw is a set of subjects with write access to o,
    • gw is a set of groups with write access to o,
    • uo is a set of subjects which are owners of o,
    • go is a set of groups wich are owners of o.
  • (secmat s o) = (mkRW ar aw): iff (mkRW ar aw) are the subjects accessing object o in state s (its a FPF), in that case:
    • ar: subjects reading from o
    • aw: subjects writing into o
  • (files s o): content of file o in state s; ; its a FPF
  • (directories s o): content of directory o in state s; its a FPF

Require Export FPF.

Record SFSstate : Set := mkSFS
   {groups : GRPNAME->(set SUBJECT);
    primaryGrp : SUBJECT->GRPNAME;
    subjectSC : (set SUBJECT*SecClass);
    AllGrp : GRPNAME;
    RootGrp : GRPNAME;
    SecAdmGrp : GRPNAME;
    objectSC : (set OBJECT*SecClass);
    acl : (set OBJECT*AccessCtrlListData);
    secmat : (set OBJECT*ReadersWriters);
    files : (set OBJECT*FILECONT);
    directories: (set OBJECT*DIRCONT)}.


  • Axioms needed for decidability

Axiom SSCeq_dec: (x1,x2:SUBJECT*SecClass) {x1=x2}+{~x1=x2}.
Axiom OSCeq_dec: (x1,x2:OBJECT*SecClass) {x1=x2}+{~x1=x2}.
Axiom ACLeq_dec: (x1,x2:OBJECT*AccessCtrlListData){x1=x2}+{~x1=x2}.
Axiom SECMATeq_dec: (x1,x2:OBJECT*ReadersWriters){x1=x2}+{~x1=x2}.
Axiom OBJFeq_dec: (x1,x2:OBJECT*FILECONT){x1=x2}+{~x1=x2}.
Axiom OBJDeq_dec: (x1,x2:OBJECT*DIRCONT){x1=x2}+{~x1=x2}.

Hints Resolve SSCeq_dec OSCeq_dec ACLeq_dec SECMATeq_dec RWeq_dec.



Shorthands for domains and partial functions defined for each of the state's components

Definition domf [f:(set OBJECT*FILECONT)] :=
  (DOM OBJeq_dec f).

Definition ffiles [f:(set OBJECT*FILECONT)] :
  OBJECT -> (Exc FILECONT) :=
  (PARTFUNC OBJeq_dec f).

Definition domd [f:(set OBJECT*DIRCONT)] :=
  (DOM OBJeq_dec f).

Definition fdirs [f:(set OBJECT*DIRCONT)] :
  OBJECT -> (Exc DIRCONT) :=
  (PARTFUNC OBJeq_dec f).

Definition domacl [f:(set OBJECT*AccessCtrlListData)] :=
  (DOM OBJeq_dec f).

Definition facl [f:(set OBJECT*AccessCtrlListData)] :
  OBJECT -> (Exc AccessCtrlListData) :=
  (PARTFUNC OBJeq_dec f).

Definition domsecmat [f:(set OBJECT*ReadersWriters)] :=
  (DOM OBJeq_dec f).

Definition ransecmat [f:(set OBJECT*ReadersWriters)] :=
  (RAN RWeq_dec f).

Definition fsecmat [f:(set OBJECT*ReadersWriters)] :
  OBJECT -> (Exc ReadersWriters) :=
  (PARTFUNC OBJeq_dec f).

Definition domOSC [f:(set OBJECT*SecClass)] :=
 (DOM OBJeq_dec f).

Definition fOSC [f:(set OBJECT*SecClass)] : OBJECT -> (Exc SecClass) :=
  (PARTFUNC OBJeq_dec f).

Definition domSSC [f:(set SUBJECT*SecClass)] :=
 (DOM SUBeq_dec f).

Definition fSSC [f:(set SUBJECT*SecClass)]: SUBJECT -> (Exc SecClass):=
  (PARTFUNC SUBeq_dec f).


Filesystem update functions

They are under-specified, i.e. we do not say how the content of a given directory is changed when a new file is created on it.

Parameter create_files: SUBJECT->OBJNAME->(set OBJECT*FILECONT).
Parameter create_directories: SUBJECT->OBJNAME->(set OBJECT*DIRCONT).
Parameter mkdir_directories: SUBJECT->OBJNAME->(set OBJECT*DIRCONT).
Parameter rmdir_directories: OBJECT->(set OBJECT*DIRCONT).
Parameter unlink_files: OBJECT->(set OBJECT*FILECONT).
Parameter unlink_directories: OBJECT->(set OBJECT*DIRCONT).
Parameter write_files: OBJECT->nat->FILECONT->(set OBJECT*FILECONT).

Modes of access and the list of system operations

  • READ: pure read access
  • WRITE: pure write access


Inductive MODE : Set :=
   |READ : MODE
   |WRITE : MODE.


  • The names of the system operations


Inductive Operation : Set :=
   |Aclstat: Operation
   |AddUsrGrpToAcl: Operation
   |Chmod: Operation
   |Chobjsc: Operation
   |Chown: Operation
   |Chsubsc: Operation
   |Close: Operation
   |Create: Operation
   |DelUsrGrpFromAcl: Operation
   |Mkdir: Operation
   |Open: Operation
   |Oscstat: Operation
   |Owner_Close: Operation
   |Read: Operation
   |Readdir: Operation
   |Rmdir: Operation
   |Sscstat: Operation
   |Stat: Operation
   |Unlink: Operation
   |Write: Operation.

Index
This page has been generated by coqdoc