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

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

NISTが、NIST IR 8539 (初公開ドラフト）遷移モデルによるセキュリティ特性の検証を公表し、意見募集をしていますね...

ちょっと力をいれて読まないと...

● NIST - ITL

・2024.10.08 NIST IR 8539 (Initial Public Draft) Security Property Verification by Transition Model

NIST IR 8539 (Initial Public Draft) Security Property Verification by Transition Model	NIST IR 8539 (初公開ドラフト）遷移モデルによるセキュリティ特性の検証
Announcement	発表
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 prove 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）言語の観点からの特性仕様について、両者の比較を交えて説明する。最後に、検証プロセスと利用可能なツールについて説明し、比較する。
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 prove 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.ipd

目次...

Executive Summary	エグゼクティブサマリー
1. Introduction	1. 序文
2. Formal Models and ACPs	2. 形式モデルと ACP
2.1. Model Fundamentals	2.1. モデルの基礎
2.2. ACP Automata	2.2. ACP オートマトン
2.2.1. Static ACPs	2.2.1. 静的ACP
2.2.2. Dynamic ACPs	2.2.2. 動的ACP
2.3. ACP combinations	2.3. ACP の組み合わせ
2.3.1. Nonconcurrent ACP Combinations	2.3.1. 非同期ACP組み合わせ
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 (LT	3.1.1. 線形時間論理 (LT
3.1.2. Computation Tree Logic (CTL)	3.1.2. 計算ツリー論理（CTL）
3.1.3. Computation Tree Logic Star (CT)	3.1.3. Computation Tree Logic Star (CT)
3.1.4. LTL vs. CTL (and CTL*)	3.1.4. LTL vs. 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. 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.	フォールトは、アクセス管理ポリシーの設計や実装における誤りや弱点であり、深刻な脆弱性につながる可能性がある。これは特に、異なるアクセス管理ポリシーが組み合わされている場合に当てはまる。特にクラウドや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 then focuses on discussing 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）の観点から、両者の比較を交えながら特性仕様について論じる。最後に、検証プロセスと利用可能なツールについて説明し、比較する。
1. Introduction	1. 序文
Faults can lead to serious vulnerabilities, particularly when different access control policies (ACPs) are combined. This 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. NIST Special Publication (SP) 800-192 [SP192] provides an overview of ACP verification using the model-checking method. However, it does not formally define the automata of transition models and properties, nor does it detail the processes and considerations for verifying access control security properties.	障害は、特に異なるアクセス管理ポリシー（ACP）が組み合わされた場合に、深刻な脆弱性につながる可能性がある。この問題は、システムが複雑化するにつれて、特にクラウドやIoTのような分散環境で、洗練された構造に組織化された大量の機密情報やリソースを管理する場合に、ますます重要になる。NIST 特別刊行物（SP）800-192 [SP192]は、モデル検査法を用いた ACP 検証の概要を提供している。しかし、遷移モデルのオートマトンやプロパティを正式に定義しているわけではなく、アクセス管理セキュリ ティプロパティを検証するためのプロセスや考慮事項について詳述しているわけでもない。
Instead of evaluating and analyzing ACPs solely at the mechanism level, formal models are typically developed to describe their security properties. An ACP transition model is a formal representation of the ACP as enforced by the mechanism and is valuable for proving the system’s theoretical limitations. This ensures that access control mechanisms are designed to adhere to the properties of the model. Generally, transition models are effective for modeling non-discretionary ACPs.	ACP をメカニズム・レベルのみで評価・分析する代わりに、そのセキュリティ特性を記述するための形式モデルを開発するのが一般的である。ACP 遷移モデルは、機構によって強制される ACP の形式的表現であり、システムの理論的限界を証明するために価値がある。これにより、アクセス管理機構がモデルの特性を遵守するように設計されていることが保証される。一般に、遷移モデルは非裁量的な ACP をモデル化するのに有効である。
An automaton is an abstraction of a self-operating transition model that follows a predetermined sequence of operations or responses. To formally verify the properties of ACP transition models through model checking, these models need to be converted into automata. This allows the rules of the ACP to be represented as a predetermined set of instructions within the automaton.	オートマトンとは、あらかじめ決められた操作や応答のシーケンスに従う、自己動作型の遷移モデルを抽象化したものである。モデル検査によってACPの遷移モデルの特性を正式に検証するには、これらのモデルをオートマトンに変換する必要がある。これにより、ACP の規則をオートマトン内の所定の命令セットとして表現することができる。
This document explains model-checking techniques for verifying access control security properties using the automata of ACP transition models. It briefly introduces the fundamentals of model checking and demonstrates how access control policies are converted into automata from transition models. The document then delves into discussions of property specifications using linear temporal logic (LTL) and computation tree logic (CTL) languages with comparisons between the two. The process of verification and the available tools are also described and compared. This document is organized as follows:	本文書では、ACP 遷移モデルのオートマトンを用いてアクセス制御のセキュリティ特性を検証する ためのモデル検査技法について説明する。簡単にモデル検査の基礎を紹介し、アクセス制御ポリシーを遷移モデルからオートマトンに変換する方法を示す。その後、線形時相論理（LTL）言語と計算ツリー論理（CTL）言語を使用したプロパティ仕様について、両者の比較を交えて説明する。検証のプロセスと利用可能なツールについても説明し、比較する。本書の構成は以下の通りである：
• Section 1 is the introduction.	・セクション1は序文である。
• Section 2 provides an overview of formal models and ACPs.	・セクション2では形式モデルとACPの概要を説明する。
• Section 3 describes properties.	・セクション3ではプロパティを説明する。
• Section 4 explains the property verification process.	・セクション4ではプロパティの検証プロセスを説明する。
• Section 5 is the conclusion.	・セクション5は結論である。
• The References section lists cited publications and sources.	・参考文献の項では引用文献と出典を示す。