Cyber8336 - Trusted OS Model Flashcards
What are three desirable properties of a trusted OS model
Generality: Formal verification
Appropriateness: faithful to the conditions of the operating environment
Predictive ability: allow simulation and query
How does the generality of a trusted OS model help.
Helps establish the internal validity of a model or abstract policy specification. Helps to generate automated test cases to verify the code.
Why is predictive ability a desired property of a trusted OS model?
This allows simulation and querying.
Simulation allows us to mathematically reason about counter examples in the system context.
Why is appropriateness a desired property of a mathematical model of a policy Trusted OS’s?
appropriateness is desired so the model maps faithfully to the conditions of the operating environment and models accomadations that were to difficult to be included in the more abstract policy statement
What is the Bell Lapadula model based on.
It is a multilevel security model based on finite state machines.
What is the Basic Security Theorem specified by Bell and Lapadula?
All controls are security preserving if a sequence of actions from a secure state results in a new secure state.
What is the *-property?
A subject S who has Read access to an object O may have write access to an object P, only if P dominates O.
A subject can only write to the level of the Read access or above.
Why don’t we have the *-property in the paper context?
In the paper world we do not have programs performing operations on behalf of the subject.
Does the *-Property prevent covert channels? Why or why not?
The *-property does not prevent covert channels because it is enforced at the reference monitor. The reference monitor is bypassed in the creation of covert channels. Separate analysis is necessary at design time to make sure they don’t cross levels.
What is the Biba model
It is a dual of the Bell Lapadula concerned with integrity, and provides the simple integrity property and the Integrity *-property
