|
It
has been mentioned (Formal specification) that the formal model consists
of a number of operations and some desired properties.
The
model verifies a property if this property is an invariant
of the model. A predicate is an invariant of a given model
if each operation of the model preserves the predicate. An
operation preserves a predicate if, starting from a state
where the predicate is true, this operation takes the system
to a new state where the same predicate holds.
As
a consequence, to verify that a model satisfies a given property
implies to prove that each operation preserves that property.
In other words:
s,t:State · P(s) /\ TR(s,Op,t) -> P(t)
for
each operation Op, where
- State
- is
the set or type of possible system states; s and t are universally
quantified over this set.
- P
- is
the property or predicate to be satisfied; it is noteworthy
that P depends on a state.
- TR
- is
the state transition relation associating two states (s
and t) and one operation (Op). It is interpreted as usual:
operation Op takes the system from state s to state t.
-
Then,
it should be proved that
n:Nat; s1,...,sn:State ·
P(s1) /\ (i:Nat · i < n -> (EX Op:Operation · TR(si,Op,si+1))) -> P(sn)
where
- Nat
- is
the set or type of natural numbers.
- EX
- is
the existential quantifier.
- Operation
- is
the set or type of system operations.
In
Lisex Security Model, these lemmas take a form slightly different.
LSM defines four properties of interest that should be preserved
by the system:
The
first two predicates are combined in one, named SecureState;
the last is a transition property (not a state property) and
so it should not be assumed in the start state. In consequence,
three lemmas per model operation should be proved:
- OpPSS
- acronym
of Op Preserves Secure State (ChmodPSS, for instance); lemmas
of this form state that the operation preserves the first
two properties (DACSecureState and SimpleSecurity)
- OpPSP
- acronym
of Op Preserves Star Property (AddUsrGrpToAclPSP, for instance);
lemmas of this form state that the operation preserves confinement
(remember that star property, *-property and confinement
are synonymous).
- OpPCP
- acronym
of Op Preserves Control Property (ClosePCP, for instance);
lemmas of this form state that the operation preserves the
fourth property
For
example, if lemma OpenPSP is written in Coq then it looks
like:
Lemma OpenPSP:
(s,t:SFSstate; u:SUBJECT)
(FuncPre5 s)
->(StarProperty s)->(TransFunc u s Open t)->(StarProperty t).
where
(FuncPre5
s) is a predicate stating that secmat
is a finite
partial function, what is a requisite to be able to prove
that open preserves confinement. It is noteworthy
that, with respect to the form described above for these lemmas,
/\ is changed for ->, what is
logically equivalent. Also, the transition relation captures
the subject (process) making the call and so it is necessary
to universally quantify over the set of subjects. Thus, one
can be sure that whatever is the start state and the subject
making the call, if this state is "secure" then the after
state will be secure.
These
three lemmas are grouped together in a file for each operation:
The
last step was to prove a lemma ensuring that the system (as
a whole) preserves DACSecureState, SimpleSecurity and StarProperty.
The theory of computer security names this lemma as Basic
Security Theorem (BST). In the same module it is proved
that the initial state is secure.
The
specification source code and the proof scripts ready to be
compiled with Coq 7.3 can be downloaded from this file LSM00.tar.gz.
This
kind of formal verification ensures nothing but correctness
of the model, not the code, with respect to a set of properties.
Functional testing is the kind of activity that gives
some confidence about the correctness of the implementation.
|
