工业控制系统中安全访问控制建模与验证

### 工业控制系统中安全访问控制建模与验证 #### 1. 引言 在工业控制系统（SCADA）中，访问控制的安全性至关重要。为了明确系统参数的访问权限，我们可以基于系统安全的关键性、系统当前状态以及预期访问操作的安全性来定义。本文将形式化安全感知的基于角色的访问控制（RBAC），并提出一种基于契约的系统方法来定义系统参数的访问权限。 #### 2. 安全感知的RBAC ##### 2.1 RBAC基本概念 基于角色的访问控制（RBAC）是确保各类计算机系统数据完整性的主要机制之一。它根据用户在系统组织环境中的角色来规范用户对计算机资源的访问。 RBAC围绕用户、角色、权限和受保护的系统资源等概念构建。在SCADA系统中，资源通常是被监控、控制和分析的系统参数，如传感器测量值、执行器设置、系统运行模式和日志等。用户可根据分配的角色访问参数。对于人类用户（系统操作员），角色通常是其工作职能；对于子系统，角色定义了该子系统在特定角色下执行的操作集。权限则定义了可应用于参数的具体操作。 RBAC在SCADA系统中的元素包括： - USERS：用户集合 - ROLES：可用用户角色集合 - PARAMETERS：受保护的系统参数集合 - RIGHTS：参数的所有可能权限集合 - PERMISSIONS：参数的权限集合 此外，US_ASSIGN定义用户到角色的分配，RO_PERM定义角色到权限的分配。 传统（静态）RBAC的访问控制通过静态权限实现。权限是权限持有者在系统中执行某些操作的能力。我们通过以下关系来形式化定义所有可能的权限： PERMISSIONS : PARAMETERS ↔ RIGHTS 它描述了系统参数与可应用于该参数的权限之间的关系。角色的权限分配基于工作权限和职责。我们定义函数RO_PERM将每个用户角色映射到参数的允许权限集合： RO_PERM : ROLES → P(PERMISSIONS) 在本文中，权限被视为对参数的基本操作，如读取和写入。操作通常需要对资源行使特定权限。例如，“删除日志”操作需要对日志状态参数具有“写入”权限，以及对日志文件参数具有“删除”权限。 传统RBAC对每个角色的访问权限提供静态视图，即不考虑系统状态来定义操作某些参数的权限。因此，权限仅定义了操作执行的必要条件，但对于SCADA系统而言，这些条件是不够的，还应考虑系统的动态状态。 ##### 2.2 动态RBAC 每个参数都有其状态，我们引入集合STATES = {st1, ..., stj}来定义资源的所有可能状态。然后，我们将动态（状态相关）权限定义为以下函数： DYN_PERM : PARAMETER × STATES → P(RIGHTS) 对于每个参数及其特定状态，DYN_PERM返回该参数在每个状态下适用的访问权限。动态角色权限可以定义为函数DYN_RO_PERM： DYN_RO_PERM : ROLES → P(DYN_PERM) 动态和静态的RBAC视图是相互依存的。静态和动态约束定义的权限构成了用户执行操作的充要条件。 ##### 2.3 安全感知的RBAC 安全感知的RBAC旨在定义条件，使系统功能操作能够在RBAC定义的静态访问权限和安全条件定义的动态约束下有效且安全地执行。 SCADA系统的行为通常用函数（操作）来描述。操作通过相应的权限改变系统参数的状态。执行操作的用户必须拥有完成操作所需的所有权限。因此，我们需要验证定义的RBAC与操作所需的访问权限之间的一致性。 我们采用基于契约的设计方法，将每个操作的正确性条件定义为契约，包括前置条件（操作输入的条件）和后置条件（操作执行结果需满足的条件）。操作是状态转换，会使变量值从v变为v'。 为确保操作从安全角度也是允许的，我们需要保证所有最终可达状态满足安全条件。在安全感知的RBAC中，操作的定义如下表所示： | 部分 | 描述 | | ---- | --