As part of the general goal of providing secure computer systems, the design of verifiably secure operating systems is one of the most important tasks. This paper addresses the problem by defining security in terms of a model and proposing a set of principles which we feel should be satisfied in a secure operating system. Informally, an operating system is secure if its users completely control the use of all information which they introduce. Four key partitions are identified: user interface functions, user invoked services, background services, and the security kernel. Principles are then defined to insure that interface functions provide a safe initial environment for executing user programs, user called services are confined, background services have no access to user information, and the security kernel adequately protects information storage.