Safety
CS5204 Review of April 15, 1997
presented April 17, 1997 by Craig H. Ganoe
Definitions
- safety:
-
An initial state/configuration is safe for a given right if there does not
exist a reachable state within which a command leaks that right.
- leaks:
-
A command leaks a given right if its execution can cause the right to be
propagated to a subject not previously possessing that right.
- primitive operation:
-
the atomic actions of the protection model
- commands:
-
useful, commonly used collections of primitive operations
- mono-operational:
-
all commands are primitive operations
Decidability of Safety
-
decidable for a mono-operational system
-
not decidable for an arbitrary configuration of an arbitrary protection system
-
may be decidable for specific protection systems
Take-Grant Model
- Taking a right:
-
Here, X has take right over Y and takes the right to read Z from Y.
- Granting a right:
-
Here, X has grant right over Y and grants the right to read Z to Y.
Safety is decidable for this model.
Bell-LaPadula Model
- subject:
-
has a clearance level (i)
- objects:
-
have a classification level (1 - n)
Subject has:
-
read access only to objects of classification levels 1 to i - 1
-
read/write access to objects of classification level i
-
write access only to objects off classification levels i + 1 to n
Protects from:
-
reading objects above a subject's current clearance level.
-
writing objects to a level below the current clearance level.
Lattice Model
Definitions
Lattice model consists of:
-
subjects, objects, and security classes (SC)
Notation: object x belongs to the security class x
Flow policy modeled by a partially ordered set (SC, ->) where:
-
SC is the set of security classes
-
-> specifies permissible information flow between classes and is a
reflexive, antisymmetric, transitive relation over SC
-
information is allowed to flow from object x to object y iff
x -> y
Flow policy is a lattice if the least upper bound and greatest lower bound
operators exist for SC.
Example Lattice
The least upper bound for (010) and (100) is (110).
The greatest lower bound for (010) and (100) is (000).
Certification of Information Flow
For: b := f(a1,...,an)
-
verify that: a1 + ... + an -> b
For: if e then S1 else S2
-
verify that: e -> S1 x S2
-
where:
S1 = x { b | b is a target of an assignment in S1}
S2 = x { b | b is a target of an assignment in S2}
Other Topics
Covert Channels
get data from observations of system resources
Question to ponder
How do authentication, authorization and safety in general work in a distributed environment?
Up next
Cryptography
- Case Study - The Kerberos System