Download complete thesis as PDF

Next, the theorem transition_state_secure is formulated as in Figure 67.
This theorem states that given an initial secure state, for any input, the state transited to
will be secure based on the defined transition operation.
%% Theorem stating change of state is secure
theorem transition_state_secure is
fa(S: State, input:Input)
securestate?(S) => securestate?((transition input S).2)
Figure 67
Theorem Transition State Secure
It should not be difficult then to conclude that given an initial empty state,
which is secure by the theorem EmptySecure, the system state will always be secure as a
direct result from transition_state_secure.
i.
Proving in Isabelle
During the session at Kestrel, the specification was translated to the
Isabelle language and Kestrel provided examples of how to use the Isabelle theorem
prover. The proof steps are performed using the Isabelle graphical interface, as described
above, which can later by copied into the Specware specification itself to facilitate reproof. From this experience, we learned that interactive theorem proving is an intense
effort that requires detailed knowledge of both the target specification’s logic and the
proof system — our BLP model and the Isabelle theorem prover, in this case. One
example, to establish that the dominates operation is a linear ordering, was not completed
due to time limitations of the visit, but illustrated how different specification styles, as
well as proof strategies, can effect the elegance of the proof.
3.
Discussion and Lessons Learned
Many of the lessons learned in the building of this submodel have been
documented and discussed in the previous section. The most important takeaway was
that the proving on Isabelle platform is not trivial, and would take more than just simple
predicate and theorem proofing knowledge and basic understanding of Isabelle to
complete the proof. Experience would be another key asset, as we saw how the Kestrel
56