Information Technology Reference
In-Depth Information
1. if the requesting subject is a trusted subject, or
2. the subject's security level dominate the object's security level and the goal
security level's vmax equals amin (can not make the object a trusted subject)
and the new security level should not violate the
-property of current access
set and the new security level should keep the hierarchy rule that every
object's security level should dominate its directory parent's security level.
∗
ChangePass
State
R
?:
Req
3
R
?
.ra
=
change
R
?
.S
∈
dom
f
R
?
.O
∈
dom
f
R
?
.O /
Subject
(
R
?
.range
)
.vmax
=(
R
?
.range
)
.amin
R
?
.S ∈ UnTSubject ⇒
(
R
?
.range
)
.vmax dominate
(
fR
?
.O
)
.vmax
∀ Triple
:
AccessTriple | Triple
∈
∈ b ∧ Triple .O
=
R
?
.O •
(
Triple .x
=
r
⇒
(
fTriple.S
)
.vmax dominate
(
R
?
.range
)
.vmax
)
∧
(
Triple .x
=
a
⇒
(
R
?
.range
)
.amin dominate
(
fTriple.S
)
.amin
)
∧
(
Triple .x
=
w
⇒
((
fTriple.S
)
.vmax dominate
(
R
?
.range
)
.vmax
∧
(
R
?
.range
)
.amin dominate
(
fTriple.S
)
.amin
))
∀
Opar
:
Object
\
Subject
|
Opar
∈
dom
f
•
R
?
.O
∈
H
(
Opar
)
⇒
(
R
?
.range
)
.vmax dominate
(
fOpar
)
.vmax
∀
Ochd
:
Object
\
Subject
|
Ochd
∈
dom
f
•
Ochd
∈
H
(
R
?
.O
)
⇒
(
fOchd
)
.vmax dominate
(
R
?
.range
)
.vmax
According to this rules, we can write security invariant and security theorems:
A system's state is a secure state if and only if every access-triple in state's access
set satisfy
∗
-property:
SecureState
State
∀
•
(
f
(
p.S
))
.vmax dominate
(
f
(
p.O
))
.vmax
p
:
AccessTriple
|
p
∈
b
∧
p.x
=
r
∀ p
:
AccessTriple | p ∈ b ∧ p.x
=
a •
(
f
(
p.O
))
.amin dominate
(
f
(
p.S
))
.amin
∀ p
:
AccessTriple | p ∈ b ∧ p.x
=
w •
(
f
(
p.S
))
.vmax dominate
(
f
(
p.O
))
.vmax
∧
(
f
(
p.O
))
.amin dominate
(
f
(
p.S
))
.amin
