Information Technology Reference
In-Depth Information
The description of secure state in CPF is lengthy, and we don't discuss it
here. There are also many theorems about secure invariant of CPF secure policy
model which can be proved by Z tools for example Z/EVES [13].
4
Comparison of Formal Methods for Secure Operating
Systems
There are more than two hundred of formal tools existing today. According to
the verification approach taken, they can be divided into two categories: Model
Checking and Theory Proving. Model checking mainly depends on constructing
the finite state model of system and verifying the desired property of the model.
The verification of model checking is automatic and speedy. SPIN [14] and SMV
[15] are the most famous tools of model checking. The above two model checking
tools are used in NASA's space craft projects to check software fault. Model
checking has the unconquerable shortcoming of combinatory exploding, and not
suitable for complicated state transformation systems such as secure operating
systems as a whole (model checking can apply the limited formalization on some
parts of secure operating system). A theorem proving system includes a set of
axioms and a set of induction rules, the verification produce is to prove given
property of system start from system axioms using the induction rules. Theorem
proving is usually human-machine interactive: people should give proof hints to
machine during the proving steps. Theorem proving methods can describe and
verify systems with infinite states. The most influential theorem proving tools
is Gypsy specification language and GVE (Gypsy Verification Environment) [7].
The high security level operating systems ASOS and LOCK all use Gypsy and
GVE as formal methods. The reason to choose Gypsy is that it clearly maps the
specification to implementation. But GVE has shortcomings in secure theorem
proving: GVE is not adaptable, after small change in specification, the proof
procedure as whole needs to be rewrite from beginning, and Gypsy is not suitable
for divide and conquer prove for large problem space. Z specification language
gives a clean and punctual specification to state based systems, the Z/EVES has
many nice features in proof management. On the other hand, Z/EVES's proof
power is greatly impaired by its deficiency in handling of recursive date types and
recursive function proving. Another formal tool, Isabelle/Isar [2] used mainly in
protocol verification is a good candidate for formalizing secure operating systems.
It is an open source project written by ML. It supports many computational
logics such as HOL (High Order Logic) and FOL (classical and intuitionistic
first order logic). Its good qualities on recursive definition and theorem proving
reflect the characteristic of its underlining ML language. Following is a mutual
recursive definition of Tmach [9] based secure lookup:
constdefs
ReadDirJudgement :: "States => Objects => ('a,'b','c)env => uid
⇒
bool"
"ReadDirJudgement State1 AccessSubject file' Accessuid
≡
(snd (GetRead State1
(
|
SubjectinTriple = AccessSubject, ObjectinTriple =
FileObject(attributes(file')), AccessMode = Readable
|
)
))
∧
