[!abstract] 核心摘要
HRU 模型 (1976) 是计算机安全领域的里程碑。它基于访问控制矩阵，证明了一个令人绝望但也至关重要的结论：在通用的复杂系统中，判定系统是否“安全”（权限是否会泄漏）在数学上是不可判定的 (Undecidable)。

1. 系统的形式化定义 (Static View)

一个 HRU 系统由七元组构成：
$$ \mathcal{S} = (R, SUB, OBJ, S_0, O_0, M_0, C) $$

符号 英文全称 含义
$R$ Rights 权限集合 (e.g., ${r, w, x, own}$)
$OBJ$ Objects 客体集合 (所有资源)
$SUB$ Subjects 主体集合 (用户/进程)
注意： $SUB \subseteq OBJ$
$S_0$ Initial Subjects 初始主体 ($S_0 \subseteq SUB$)
$O_0$ Initial Objects 初始客体 ($O_0 \subseteq OBJ$)
$M_0$ Initial Matrix 初始矩阵。$M[s, o]$ 表示主体 $s$ 对 $o$ 的权限
$C$ Commands 改变状态的命令集

2. 状态变更机制 (Dynamic View)

系统状态通过 命令 (Commands) 进行迁移。每个命令由 条件 (Condition) 和 基本原语 (Primitive Operations) 组成。

A. 六种基本原语 (Primitive Operations)

这是修改矩阵 $M$ 的最小原子操作：

  1. create_subject(s): 若 $s \notin OBJ$，则矩阵增加一行一列。
  2. create_object(o): 若 $o \notin OBJ$，则矩阵增加一列。
  3. destroy_subject(s): 若 $s \in SUB$，则矩阵删除一行一列。
  4. destroy_object(o): 若 $o \in OBJ$，则矩阵删除一列。
  5. enter(d, s, o): 授予权限。 $$M[s, o] \leftarrow M[s, o] \cup {d}$$
  6. delete(d, s, o): 移除权限。 $$M[s, o] \leftarrow M[s, o] \setminus {d}$$

B. 命令结构 (The Command)

仅当矩阵满足特定条件时，才执行操作序列：

$$
\begin{align}
& \textbf{command } \alpha(x_1, \dots, x_k) \
& \quad \textbf{if } r_1 \in M[x_{i_1}, x_{j_1}] \land \dots \land r_m \in M[x_{i_m}, x_{j_m}] \
& \quad \textbf{then } \
& \quad \quad op_1; \
& \quad \quad \dots \
& \quad \quad op_p; \
& \textbf{end}
\end{align}
$$

3. 安全性与泄漏 (Safety & Leaking)

我们要解决的核心问题是：某个权限 $d$ 是否会泄漏给未授权的主体？

定义：泄漏 (Leak)

给定初始状态 $(S_0, O_0, M_0)$，如果存在一个命令序列 $c_1, \dots, c_n$ 执行后，导致：
$$ \exists s \in S_n, o \in O_n \text{ such that } d \in M_n[s, o] $$
且在之前的状态中 $s$ 并不拥有该权限（或 $s,o$ 未创建），则称 权限 $d$ 发生了泄漏。

[!NOTE] 提示
根据定义，如果一个命令在内部 enter 后立即 delete 了权限，通常不被视为泄漏（视命令执行为原子操作）。

定义：安全 (Safety)

  • (d)-safety: 权限 $d$ 永远不会泄漏。
  • (s, o, d)-safety: 特定主体 $s$ 永远无法获取特定客体 $o$ 的权限 $d$。

4. 核心结论 (The HRU Result)

[!FAILURE] 不可判定性定理 (Undecidability)
Harrison, Ruzzo 和 Ullman 证明了：
对于一般的 HRU 系统（允许复杂的命令逻辑），判定一个给定的初始配置是否安全，在图灵机意义上是“不可判定”的 (Undecidable)。

这意味着不存在一个通用算法能检查任意系统的安全性。

[!SUCCESS] 特例：单操作命令 (Mono-operational)
如果系统被限制为：每个命令只能包含 1 个基本原语。
那么，系统的安全性是 可判定 (Decidable) 的。

5. 总结

HRU 模型揭示了灵活性与安全性之间的权衡：

  1. 如果我们允许系统有非常灵活的权限变更规则（复杂的 if-then），我们就无法自动验证它是安全的。
  2. 如果我们想保证能够验证安全性，我们就必须限制系统的复杂度（例如限制命令的结构）。

#Security #AccessControl #FormalMethods #LearningNote