可信任系统是美国国防部定义的安全操作系统标准，该标准共分为A、B、C、D四个大的安全级别。
D级不具备安全特征。
C级支持自主式访问控制和对象复用。C1级中，将用户和数据分离，每个用户可以通过认证和访问控制等手段保护其隐私信息，但不能保护系统中的敏感信息；C2级中，系统对用户进行识别和认证，通过登录过程和安全审计对系统中的敏感信息实时保护，这是处理敏感信息的最低安全级别。
B级属于强制式信息保护。B1级为带有敏感标记的信息保护，必须给出安全策略模型的非正规描述；B2级为结构式保护，系统中的所有对象都要实施（自主或强制式）访问控制，必须给出安全策略的形式化模型；B3级（安全域）中，对所有对象的访问控制是防篡改并可测试的，且支持安全管理员的功能，具有安全审计和报警功能。
A级形式化技术贯穿于真个开发过程，实现了可验证的安全策略模型，例如，可以用形式化技术分析隐含信道。
