Specification and verification of the UCLA Unix security kernel