NIST内部报告

NIST IR 8539

基于转换模型的安全属性验证

Vincent C. Hu

计算机安全处信息技术实验室

本出版物可从以下网站免费获取：https://doi.org/10.6028/NIST.IR.8539

2025年1月

执行摘要

故障可能是访问控制策略的设计或实施中的错误或弱点，可能导致严重的漏洞。当组合不同的访问控制策略时尤其如此。随着系统变得越来越复杂，这个问题变得越来越关键，特别是在云和物联网等分布式环境中，这些环境管理着大量敏感信息和资源，这些信息和资源被组织成复杂的结构。访问控制策略及其实现通常不会明确表达其底层语义，这些语义可能隐含地嵌入策略规则的逻辑流中。

形式化转换模型用于证明策略的安全属性，并确保访问控制机制的设计满足安全要求。本报告解释了如何应用模型检查技术来验证访问控制策略转换模型中的安全属性。它简要介绍了模型检查的基本原理，并演示了访问控制策略如何从其转换模型转换为自动机。该报告还讨论了线性时间逻辑（LTL）和计算树逻辑（CTL）的属性规范，并对两者进行了比较。最后，对验证过程和可用工具进行了描述和比较。

1.导言

故障可能导致严重的漏洞，特别是在组合不同的访问控制策略（ACP）时。随着系统变得越来越复杂，这个问题变得越来越重要，特别是在云和物联网等分布式环境中，这些环境管理着大量敏感信息和资源，这些信息和资源被组织成复杂的结构。NIST特别出版物（SP）800-192[SP192]概述了使用模型检查方法进行ACP验证。然而，它没有正式定义转换模型和属性的自动机，也没有详细说明验证访问控制安全属性的过程和注意事项。

通常会开发形式化模型来描述ACP的安全属性，而不是仅在机制级别评估和分析ACP。ACP转换模型是由该机制强制执行的ACP的形式化表示，对于证明该系统的理论局限性具有重要价值。这确保了访问控制机制的设计符合模型的属性。一般来说，过渡模型对于非自主ACP的建模是有效的。

自动机是遵循预定操作或响应序列的自操作转换模型的抽象。为了通过模型检查正式验证ACP转换模型的属性，这些模型需要转换为自动机。这允许ACP的规则被表示为自动机内的一组预定指令。

本文解释了使用ACP转换模型的自动机验证访问控制安全属性的模型检查技术。它简要介绍了模型检查的基本原理，并演示了如何将访问控制策略从转换模型转换为自动机。然后，该文档深入讨论了使用线性时序逻辑（LTL）和计算树逻辑（CTL）的属性规范，并对两者进行了比较。还描述并比较了验证过程和可用工具。

本文件组织如下：

l第1节是引言。

l第2节概述了正式模型和ACP。

l第3节描述了属性。

l第4节解释了财产核实过程。

l第5节是结论。

原文始发于微信公众号（老烦的草根安全观）：基于转换模型的安全属性验证