米国 NIST IR 8539 遷移モデルによるセキュリティ特性の検証 (2025.01.31)

こんにちは、丸山満彦です。

NISTが、IR 8539 Security Property Verification by Transition Model（遷移モデルによるセキュリティ特性の検証）を公表していますね...

昨年の10月にドラフトを公表し、意見募集をしていたものですね...結局十分に読み込んでいなくて、よく理解していないままです...(^^;;

複雑、多様化しているシステムのアクセス管理について、遷移モデル（状態遷移を表現するための数学的フレームワーク）を利用して、アクセスポリシーを検証する方法ということなのですかね...

遷移モデルを具体化するオートマトンについても詳細に検討されていますね...

特性仕様については、線形時相論理（LTL）と計算木論理（CTL）が説明につかわれていますね...

● NIST - ITL

・2025.01.31 Security Property Verification by Transition Model | NIST Publishes IR 8539

Security Property Verification by Transition Model | NIST Publishes IR 8539	移行モデルによるセキュリティ特性検証｜NISTがIR 8539を発行
NIST Internal Report (IR) 8539, Security Property Verification by Transition Model, is now available.	NIST内部報告書（IR）8539「移行モデルによるセキュリティ特性検証」が公開された。
Verifying the security properties of access control policies is a complex and critical task. Often, the policies and their implementation do not explicitly express their underlying semantics, which may be implicitly embedded in the logic flows of policy rules, especially when policies are combined. Instead of evaluating and analyzing access control policies solely at the mechanism level, formal transition models can describe these policies and prove the system’s security properties,  ensuring that access control mechanisms are designed to meet security requirements.	アクセス管理ポリシーのセキュリティ特性の検証は、複雑かつ重要な作業である。 ポリシーとその実装は、その基礎となるセマンティクスを明示的に表現していないことが多く、特にポリシーが組み合わされる場合には、ポリシー・ルールの論理フローに暗黙的に組み込まれている可能性がある。 アクセス管理ポリシーをメカニズム・レベルのみで評価・分析するのではなく、形式遷移モデルを使用してポリシーを記述し、システムのセキュリティ特性を証明することで、アクセス管理メカニズムがセキュリティ要件を満たすように設計されていることを保証できる。
This document explains how to apply model-checking techniques to verify security properties in transition models of access control policies. It provides a brief introduction to the fundamentals of model checking and demonstrates how access control policies are converted into automata from their transition models. The document also discusses property specifications in terms of linear temporal logic (LTL) and computation tree logic (CTL) languages with comparisons between the two. Finally, the verification process and available tools are described and compared.	本書では、アクセス管理ポリシーの遷移モデルにおけるセキュリティ特性を検証するためにモデル検査技術を適用する方法について説明する。また、モデル検査の基礎について簡単な序文を提供し、アクセス管理ポリシーがその遷移モデルからオートマトンに変換される方法を説明する。さらに、線形時相論理（LTL）と計算木論理（CTL）言語の観点から特性仕様について論じ、両者を比較する。最後に、検証プロセスと利用可能なツールについて説明し、比較する。

・2025.01.31 NIST IR 8539 Security Property Verification by Transition Model

NIST IR 8539 Security Property Verification by Transition Model	NIST IR 8539 遷移モデルによるセキュリティ特性の検証
Abstract	要約
Verifying the security properties of access control policies is a complex and critical task. The policies and their implementation often do not explicitly express their underlying semantics, which may be implicitly embedded in the logic flows of policy rules, especially when policies are combined. Instead of evaluating and analyzing access control policies solely at the mechanism level, formal transition models are used to describe these policies and verify the system’s security properties. This approach ensures that access control mechanisms can be designed to meet security requirements. This document explains how to apply model-checking techniques to verify security properties in transition models of access control policies. It provides a brief introduction to the fundamentals of model checking and demonstrates how access control policies are converted into automata from their transition models. The document then focuses on discussing property specifications in terms of linear temporal logic (LTL) and computation tree logic (CTL) languages with comparisons between the two. Finally, the verification process and available tools are described and compared.	アクセス管理ポリシーのセキュリティ特性の検証は、複雑かつ重要な作業である。ポリシーとその実装は、その基礎となるセマンティクスを明示的に表現していないことが多く、特にポリシーが組み合わされる場合には、ポリシー・ルールの論理フローに暗黙的に組み込まれている可能性がある。アクセス管理ポリシーをメカニズム・レベルのみで評価・分析するのではなく、形式遷移モデルを使用してポリシーを記述し、システムのセキュリティ特性を検証する。このアプローチにより、アクセス管理メカニズムをセキュリティ要件を満たすように設計できることが保証される。本書では、アクセス管理ポリシーの遷移モデルにおけるセキュリティプロパティを検証するためにモデル検査技術を適用する方法について説明する。また、モデル検査の基本について簡単に紹介し、アクセス管理ポリシーが遷移モデルからオートマトンに変換される方法を説明する。さらに、線形時間論理（LTL）と計算木論理（CTL）の言語におけるプロパティ仕様について、両者を比較しながら重点的に説明する。最後に、検証プロセスと利用可能なツールについて説明し、比較する。

・[PDF] NIST.IR.8539

目次...

Executive Summary	エグゼクティブサマリー
1. Introduction	1. 序文
2. Formal Models and ACPs	2. 形式モデルとアクセス制御ポリシー
2.1. Model Fundamentals	2.1. モデルの基本
2.2. ACP Automata	2.2. アクセス制御オートマトン
2.2.1. Static ACPs	2.2.1. 静的アクセス制御ポリシー
2.2.2. Dynamic ACPs	2.2.2. 動的アクセス制御ポリシー
2.3. ACP combinations	2.3. アクセス制御ポリシーの組み合わせ
2.3.1. Nonconcurrent ACP Combinations	2.3.1. 非並行アクセス制御ポリシーの組み合わせ
2.3.2. Concurrent ACP Combinations	2.3.2. 同時実行ACPの組み合わせ
3. Properties	3. プロパティ
3.1. Property Specifications	3.1. プロパティ仕様
3.1.1. Linear Temporal Logic	3.1.1. 線形時相論理
3.1.2. Computation Tree Logic	3.1.2. 計算木論理
3.1.3. Computation Tree Logic Star	3.1.3. 計算木論理スター
3.1.4. LTL vs. CTL (and CTL*)	3.1.4. LTL対CTL（およびCTL*
3.2. Security Properties	3.2. セキュリティプロパティ
3.2.1. Safety	3.2.1. 安全
3.2.2. Liveness	3.2.2. ライブネス
4. Verification Process	4. 検証プロセス
4.1. General Method	4.1. 一般的手法
4.2. NuSMV Tool	4.2. NuSMV ツール
4.3. Comparison With Other Model-Checking Methods	4.3. 他のモデル制御手法との比較
5. Conclusion	5. 結論
References	参考文献
List of Tables	表一覧
Table 1. CTL vs. CTL* formulae	表1. CTL対CTL*式
List of Figures	図一覧
Fig. 1. Example automaton of a random rules ACP	図1. ランダムルールACPのオートマトン例
Fig. 2. Example automaton of a Chinese Wall ACP	図2. チャイニーズウォールACPのオートマトン例
Fig. 3. Example automaton of a Workflow ACP	図3. ワークフローACPのオートマトン例
Fig. 4. Example automaton of an N-person Control ACP	図4. N人制御ACPのオートマトン例
Fig. 5. Intersection concept using an example of two automata	図5. 2つのオートマトンの例による交点の概念
Fis. 6. Union concept using an example of twoautoma	図6. 2つのオートマトンの例によるユニオンの概念
Fig. 7. Concatenation concept using an example of two automata	図7. 2つのオートマトンの例による連結概念
Fig. 8. Example of a combination of two interleaving automata	図8. 2つのインターリーブ・オートマトンの組み合わせの例
Fig. 9. Shared variables concept with an example of two automata	図9. 2つのオートマタの例による共有変数の概念
Fig. 10. Shared actions concept with an example of two automata	図10. 2つのオートマトンの例による共有作用の概念
Fig. 11. Example of E(EX p) U (AG q) in CT.	図11. CTにおけるE(EX p) U (AG q)の例。
Fig. 12. Relationships among LTL, CTL, and CTL	図12. LTL, CTL, CTLの関係
Fig. 13. Example of the ACP transition model that satisfies EG p but not AF q	図13. EG pは満たすがAF qは満たさないACP遷移モデルの例
Fig. 14. A mutual exclusion access system	図14. 相互排他アクセスシステム

エグゼクティブサマリー...

Executive Summary	エグゼクティブサマリー
Faults may be errors or weaknesses in the design or implementation of access control policies that can lead to serious vulnerabilities. This is particularly true when different access control policies are combined. The issue becomes increasingly critical as systems grow more complex, especially in distributed environments like the cloud and IoT, which manage large amounts of sensitive information and resources that are organized into sophisticated structures. Access control policies and their implementation often do not explicitly express their underlying semantics, which may be implicitly embedded in the logic flows of policy rules.	障害とは、アクセス管理ポリシーの設計や実装におけるエラーや弱点であり、深刻な脆弱性につながる可能性がある。これは、異なるアクセス管理ポリシーが組み合わされる場合に特に当てはまる。システムが複雑になるにつれ、この問題はますます深刻化する。特に、クラウドやIoTのような分散環境では、大量の機密情報やリソースを高度な構造に編成して管理しているため、この傾向が顕著である。アクセス管理ポリシーとその実装では、その基盤となるセマンティクスが明示的に表現されていないことが多く、ポリシー・ルールの論理フローに暗黙的に組み込まれている場合がある。
Formal transition models are used to prove the policy’s security properties and ensure that access control mechanisms are designed to meet security requirements. This report explains how to apply model-checking techniques to verify security properties in transition models of access control policies. It provides a brief introduction to the fundamentals of model checking and demonstrates how access control policies are converted into automata from their transition models. The report also discusses property specifications in terms of linear time logic (LTL) and computation tree logic (CTL) with comparisons between the two. Finally, the verification process and available tools are described and compared.	形式遷移モデルは、ポリシーのセキュリティ特性を証明し、アクセス管理メカニズムがセキュリティ要件を満たすように設計されていることを確認するために使用される。本レポートでは、アクセス管理ポリシーの遷移モデルにおけるセキュリティ特性を検証するためにモデル検査技術を適用する方法について説明する。また、モデル検査の基礎について簡単に紹介し、アクセス管理ポリシーがその遷移モデルからオートマトンに変換される方法を説明する。さらに、線形時間論理（LTL）と計算木論理（CTL）の観点から特性仕様について論じ、両者を比較する。最後に、検証プロセスと利用可能なツールについて説明し、比較する。

---

● まるちゃんの情報セキュリティ気まぐれ日記

・2024.10.10 米国 NIST IR 8539 (初公開ドラフト）遷移モデルによるセキュリティ特性の検証