Proof of separability A verification technique for a class of security kernels

Abstract

A formal model of ‘secure isolation’ between the users of a shared computer system is presented. It is then developed into a security verification technique called ‘Proof of Separability’ whose basis is to prove that the behaviour perceived by each user of the shared system is indistinguishable from that which could be provided by an unshared machine dedicated to his private use. Proof of Separability is suitable for the verification of security kernels which enforce the policy of isolation; it explicitly addresses issues relating to the interpretation of instructions and the flow of control (including interrupts) which have been ignored by previous treatments.