Third European Symposium on Research in Computer Security (ESORICS 94)
Non-interference through Determinism
A.W. Roscoe, J.C.P. Woodcock, L. Wulf
Keywords : security, non-interference, formal methods, process algebra, determinism, automatic verification
Abstract : The standard approach to the specification of a secure system is to present a (usually state-based) abstract security model separately from the specification of the system's functional requirements, and establishing a correspondence between the two specifications. This complex treatment has resulted in development methods distinct from those usually advocated for general applications. We provide a novel and intellectually satisfying formulation of security properties in a process algebraic framework, and show that these are preserved under refinement. We relate the results to a more familiar state-based (Z) specification methodology. There are efficient algorithms for verifying our security properties using model checking.
(Pages 3-18)