Information Technology Reference
In-Depth Information
GivePerm
∆State
R
?:
Req
2
R
?
.Caller
∈
PrivUser
∪{
Owner
(
R
?
.O
)
}
R
?
.ra
=
give
b
=
b
ACL
=
ACL
⊕{
R
?
.O
→{
R
?
.User
→
(
ACL R
?
.O
)(
R
?
.User
)
∪{
R
?
.ReqPerm
}}}
Owner
=
Owner
RescindPerm
∆State
R
?:
Req
2
R
?
.Caller
∈
PrivUser
∪{
Owner
(
R
?
.O
)
}
R
?
.ra
=
rescind
b
=
b
ACL
=
ACL ⊕{R
?
.O →{R
?
.User →
(
ACL R
?
.O
)(
R
?
.User
)
\{R
?
.ReqPerm}}}
Owner
=
Owner
3.3 Formal Description of CPF Secure Policy Model
As mentioned in section 2, CPF is a state based trusted process control frame-
work. In the /etc/smos/cpf directory of SECIMOS operating system, there ex-
ists a configuration file prog.conf. In the file prog.conf, there will be a Prog-
PrivTableEntry for each privilege state of each trusted program. prog refers to
the disk program like “wuftpd”, pstate is the privilege state and priv info is
various of capabilities and operating parameters a process of program prog have
in privilege state pstate.
ProgPrivTableEntry
prog
:
Prog
pstate
:
PState
priv info
:
P
(
Priv
×
PParam
)
On the other hand, the system state as a whole consists of the ProgPrivTable
made up from ProgPrivTableEntries, b: the current access set and several of
privilege mapping functions. For example, Proc PState maps one of the process
in system to the privilege state that process is current in.
State
ProgPrivTable
:
P
ProgPrivTableEntry
User Priv
:
User
→
P
Priv
Proc PState
:
Proc
→
PState
Proc User
:
Proc
→
User
Proc Prog
:
Proc
→
Prog
Proc Creds
:
Proc
→
P
(
Priv
×
P
PParam
)
b
:
P
AccessTuple
