Information Technology Reference
In-Depth Information
={ S Σ , T ,
A system
Σ
, Q } is a finite machine: a state
is reachable in the sys-
tem
Σ
if and only if there is the sequence <( q 0 ,
), ..., ( q n ,
)> such that
=
,
s
=
, and
= T ( q i ,
) if 0< i < n . Note that for any system
is trivially
1
reachable.
A General Security Model. A general security model M is an ensemble of sets,
M ={ S , R , C }, where:
S denotes the set of the security states defined by the security model,
R is the set of the access control rules in the form of logical predicates r ( s , s' ) de-
fined on S × S and checking that the transition from s to s' meets to the security
model,
C is the set of the state security criteria in the form of logical predicates c ( s ) de-
fined on S and checking security of the state s . A state s S is secure if and only if
for every security criterion c from C the predicate c ( s ) is true:
c C : c ( s )=true.
A System Safety Property. A system safety property Λ can be formulized as Λ={ M ,
Σ, D }, where:
M is the access control model, M ={ S , R , C },
• Σ
= { S Σ , T ,
denotes the system,
Σ
, Q },
D is the mapping function, D : S Σ S , which sets the relation between the system
states and the security states.
By the definitions being specified, a system safety statement may be formulated.
A System Safety Statement
The system Σ implementing the model M is safe if and only if:
1. ∀ c C : c ( D (
))= true ,
+
+
+
S Σ :
2. ∀
,
= T ( q ,
) ∃ s i = D (
), s i +1 = D (
) and ∀ r R : r ( s i , s i +1 )= true ,
S Σ :
3. ∀
))= true .
This statement declares an analogous of the General Security Theorem [4, 5], but
in reference to the safety problem in real computer systems.
is reachable from
, ∀ c C : c ( D (
Security Tasks Statement
The introduced theory establishes a basis of the problems which face every participant
of IT-security: the theoreticians, the system developers and the evaluators. According
to the proposed definitions we can state three problems.
Model Proof. For the given model M we have to prove that any reachable state from
S satisfies the security criteria C . In this case we prove that every system realized on
such a mode will be safe in general.
System Design. For the given system Σ, the security criteria C , and the security states
S we have to create the access control rules R so that system Σ with M ={ C , S , R } will
be safe.
Search WWH ::




Custom Search