1。システムのセキュリティポリシーの数学的に正確なステートメントを実行します。いくつかの正式なモデリング手法が含まれます：状態遷移モデル、時相論理モデル、外延的意味モデル、代数仕様モデル。 2。セキュリティポリシーの数学的に正確なステートメントを実行します。十分正確には、このようなモデルは、システムの初期状態を表している必要があります、そのシステムが別の状態から進行方法、およびシステムの"安全な"状態の定義。 TCBのための基礎として許容されるには、モデルが正式に証明でサポートされている必要があることを、システムの初期状態との"安全な"状態の定義を満たす場合に、モデルホールドに必要なすべての前提条件、将来のすべての状態システムのセキュリティで保護されます。いくつかの正式なモデリング手法が含まれます：状態遷移モデルを、時相論理モデル、外延的意味モデル、代数仕様モデル。例では、リファレンスのベルとLaPadulaで説明されたモデルです。も参照してください：ベルLaP​​adulaモデル、セキュリティポリシーのモデル。