The trusted computing base (TCB) of a secure operating system can have its security policy enforced by a small, provably correct security manager. The design of the Secure TUNIS (Toronto University system) operating system divides security concerns into policy (implemented by its security manager) and mechanism (implemented by the rest of the operating system). It is shown that this separation is a key concept in allowing Secure TUNIS to be validated, due to the isolation of security critical code and data in a small module. This design provides the basis of an implementation of a POSIX (Unix) kernel that can be certified at security levels of B3 and above. The security policy, as implemented by Secure TUNIS, is given.>