Information Technology Reference
In-Depth Information
verifiable using mechanical theorem provers. This objective has been met by the
current implementation. We expect that it would be straightforward for users
of theorem provers other than HOL to inspect our definitional extensions and
replicate the axioms, soundness proofs, theorems, and examples in the theorem
prover of their choice.
In the course of doing our proofs, we investigated proving a soundness theo-
rem directly:
If statement
ϕ
is derivable from the access-control axioms, then
ϕ
is
satisfied by all Kripke models.
The advantage of having such a theorem would be that users could do all their
reasoning at the level of the access-control logic - instead of at the level of Kripke
structures - and know that their conclusions were sound. In addition, such the-
orem would support using different models of the access-control logic (e.g., the
MSS model) without affecting the proofs done by users: the sole requirement
would be that the appropriate soundness theorem would have to be proved be-
forehand. Unfortunately, the prospects of introducing a derivability predicate
and then proving soundness in HOL did not look promising, due to the de-
pendence based on propositional-logic tautologies. Logical frameworks such as
Isabelle/HOL [7] might better facilitate such an approach.
As stated previously, the access-control logic we have implemented was used
to give a formal interpretation of part of the CSIv2 standard. As the CSIv2 stan-
dard is extended to provide a standard interpretation for the security-attributes
component of the SAS data structure, there will be a need to reason about au-
thorizations and privileges. We anticipate extending the current logic to support
such reasoning. The benefits of such an extension include the ability to give
a precise and accurate interpretation of the standard and a means for formal
assurance of correctness and security.
Acknowledgments
This work was supported in part by the New York State Center for Advanced
Technology in Computer Applications and Software Engineering (CASE).
References
1. Object
Management
Group:
CORBAServices:
Common
Object
Services.
no formal/98-07-05 (July 1998) Available via
http://www.omg.org/cgi-bin/doc?formal/98-07-05
2. Object Management Group: The Common Secure Interoperability Version 2,
no ptc/01-06-17, (June 2001) Available via
http://www.omg.org/cgi-bin/doc?ptc/01-06-17
3. Martin Abadi and Michael Burrows and Butler Lampson and Gordon Plotkin: A
Calculus for Access Control in Distributed Systems. ACM Transactions on Pro-
gramming Languages and Systems, Vol. 15, no 4 (September 1993) 706-734
