This chapter discusses several security models as well as the Department of Defense's well-established criteria for what constitutes a secure computer system. For systems requiring the highest degree of security, a formal specification and verification is essential in addition to the formal security model. To develop a secure system, a formal model for the security should be included as part of the top-level definition of the system. The Bell and LaPadula (BLP) model addresses the military security policy's goal of unauthorized disclosure and declassification of information. The Clark-Wilson model was developed to address the commercial environment. The Goguen-Meseguer model introduces the concept of noninterference between users. Discretionary Access Control requirements can be thought of as separating users from information on a need-to-know basis. Mandatory access controls are required to implement multi-level security. The Department of Defense's Trusted Computer System Evaluation Criteria (TCSEC) provides requirements and specific criteria to develop a system that implements a chosen security model.