可信任系統

可信任系統是美國國防部定義的安全作業系統標準，該標準共分為A、B、C、D四個大的安全級別。
D級不具備安全特徵。
C級支持自主式訪問控制和對象復用。C1級中，將用戶和數據分離，每個用戶可以通過認證和訪問控制等手段保護其隱私信息，但不能保護系統中的敏感信息；C2級中，系統對用戶進行識別和認證，通過登錄過程和安全審計對系統中的敏感信息實時保護，這是處理敏感信息的最低安全級別。
B級屬於強制式信息保護。B1級為帶有敏感標記的信息保護，必須給出安全策略模型的非正規描述；B2級為結構式保護，系統中的所有對象都要實施（自主或強制式）訪問控制，必須給出安全策略的形式化模型；B3級（安全域）中，對所有對象的訪問控制是防篡改並可測試的，且支持安全管理員的功能，具有安全審計和報警功能。
A級形式化技術貫穿於整個開發過程，實現了可驗證的安全策略模型，例如，可以用形式化技術分析隱含信道。