Information Technology Reference
In-Depth Information
UnTSubject
:
P
Subject
TSubject
:
P
Subject
Subject
=
UnTSubject
∪
TSubject
UnTSubject
∩
TSubject
=
∅
When a subject want to access a object, it must firstly get the access right
from the decision subsystem of the policy. If granted, the subject, object and
access type triple will add to current access set of system:
AddNewAccessTriple
∆State
R
?:
Req
1
b
=
b
∪{
new
:
AccessTriple
|
new.S
=
R
?
.S
∧
new.O
=
R
?
.O
∧
new.x
=
R
?
.x
}
f
=
f
H
=
H
According to our policy, the subject can get the read access right to the
object if and only if the subject's security level vmax dominates the object's
security level.
ReadPass
State
R
?:
Req
1
R
?
.ra
=
get
R
?
.x
=
r
R
?
.S ∈
dom
f
R
?
.O
dom
f
(
fR
?
.S
)
.vmax dominate
(
fR
?
.O
)
.vmax
∈
As mentioned before, whenever a subject in system wants to access an object,
it must first request the access right from decision subsystem. After validated
the request, the decision subsystem will add the subject, object and access type
access-triple into current access set, otherwise, the State keeps invariant.
Rule GetRead
=(
ReadPass
∧
AddNewAccessTriple
∧
Pass
)
∨
(
ReadDeny
∧
Invariant
∧
Deny
)
∨
(
¬
(
ReadPass
∨
ReadDeny
)
∧
Invariant
∧
Unknown
)
In above definition, ReadDeny has the same structure as ReadPass while
ReadDeny represents the condition that the get read request should be rejected.
Invariant is a schema which indicating that the system state is kept unchanged.
Pass, Deny, Unknown are simply schemas represent answer to the get read request.
There are many other rules in our formal specification. Because the limitation
of space, we only list another rule ChangeObjectRange here. Under following
condition, a subject's request of change a object's security level can be granted:
