形式化安全模型
在上一节课中，我们讨论了访问控制的基础概念。我们看到了访问控制矩阵、能力列表、ACL等实现方式。但这些实现方式都是非形式化的——它们描述了“如何”实现访问控制，但没有形式化地定义“什么是安全的”。
形式化安全模型使用数学方法精确地定义安全属性。它们不是实现细节，而是安全策略的形式化表达。一个形式化安全模型可以回答这样的问题：在什么条件下，系统是安全的？如何证明系统满足安全属性？如何检测系统是否违反了安全属性？
形式化安全模型的价值在于它们的精确性。非形式化的安全策略可能有歧义，不同的人可能有不同的理解。形式化模型消除了这种歧义，使得安全策略可以被严格地定义、验证和执行。
形式化安全模型是安全领域的“数学语言”。它们用数学的精确性来描述安全属性，使得安全策略可以被严格地分析和验证。
但形式化模型也有局限性。它们往往基于简化的假设，可能无法捕捉现实系统的所有复杂性。一个在理论上安全的模型，在实际实现中可能仍然存在漏洞。
Bell–LaPadula 模型（机密性）
Bell-LaPadula模型是最著名的形式化安全模型之一，它形式化地定义了机密性（Confidentiality）。这个模型最初是为军事信息系统设计的，用于防止信息从高安全级别泄露到低安全级别。
安全级别和格结构
Bell-LaPadula模型基于安全级别（Security Level）的概念。每个主体和客体都有一个安全级别，安全级别形成一个格（Lattice）结构。格结构意味着安全级别可以比较——一个级别可能高于、低于或等于另一个级别，但不能“不可比较”。
在军事系统中，安全级别可能是：公开（Unclassified）、内部（Confidential）、秘密（Secret）、绝密（Top Secret）。这些级别形成一个线性层次：公开 < 内部 < 秘密 < 绝密。
但在更复杂的系统中，安全级别可能有多个维度。比如，一个文档可能同时有分类级别（公开/秘密/绝密）和部门标签（研发/财务/人事）。这种多维度安全级别形成一个格结构，其中两个级别可能不可比较。
简单安全属性（Simple Security Property）
Bell-LaPadula模型的核心是两条规则。第一条是简单安全属性，也称为“不能向上读”（No Read Up）规则：
一个主体只能读取安全级别小于或等于其安全级别的客体。
换句话说，一个低安全级别的主体不能读取高安全级别的信息。这防止了信息从高安全级别泄露到低安全级别。
这个规则是直观的。如果一个用户的安全级别是“秘密”，他们可以读取“公开”和“内部”的信息，但不能读取“绝密”的信息。这确保了高安全级别的信息不会被低安全级别的用户访问。
简单安全属性只防止“读取”，不防止“写入”。一个低安全级别的用户可能无法读取高安全级别的文件，但可能可以向高安全级别的文件写入数据。这可能导致完整性问题，我们稍后会讨论。
*-属性（Star Property）
Bell-LaPadula模型的第二条规则是*-属性，也称为“不能向下写”（No Write Down）规则：
一个主体只能写入安全级别大于或等于其安全级别的客体。
换句话说，一个高安全级别的主体不能向低安全级别的客体写入数据。这防止了信息从高安全级别泄露到低安全级别。
-属性与简单安全属性配合，形成了完整的机密性保护。简单安全属性防止低级别用户读取高级别信息，-属性防止高级别用户向低级别写入信息。两者结合，确保了信息只能在同一安全级别内流动，或者从低级别向高级别流动，但不能从高级别向低级别流动。
实际应用和局限性
Bell-LaPadula模型在理论上很完美，但在实际应用中面临许多挑战。首先，模型假设安全级别是静态的，但实际系统中安全级别可能需要动态变化。一个文档可能最初是“秘密”级别，但随着时间的推移可能降级为“内部”级别。
其次，模型假设所有信息都有明确的安全级别，但实际系统中可能有不适合分类的信息，或者安全级别不明确的信息。如何处理这些信息是一个实际问题。
第三，模型只关注机密性，不关注完整性。一个低安全级别的用户可能无法读取高安全级别的文件，但可能可以向高安全级别的文件写入恶意数据，破坏文件的完整性。这就是为什么需要Biba模型来保护完整性。
Bell-LaPadula模型只保护机密性，不保护完整性。在实际系统中，需要同时考虑机密性和完整性，可能需要结合使用多个安全模型。
尽管有这些局限性，Bell-LaPadula模型仍然是理解机密性保护的重要工具。它帮助我们思考：如何防止信息泄露？如何设计多级安全系统？如何平衡安全性和可用性？
Biba 模型（完整性）
Biba模型是Bell-LaPadula模型的“镜像”，它形式化地定义了完整性（Integrity）。正如Bell-LaPadula模型防止信息从高安全级别泄露到低安全级别，Biba模型防止低完整性级别的信息污染高完整性级别的信息。
完整性级别
Biba模型使用完整性级别（Integrity Level）的概念。每个主体和客体都有一个完整性级别，完整性级别形成一个格结构。高完整性级别意味着信息更可信、更准确、更可靠。
完整性级别可能基于信息的来源、验证程度、可信度等因素。比如，来自可信来源、经过验证的信息可能有高完整性级别，而来自不可信来源、未经验证的信息可能有低完整性级别。
Biba模型的规则
Biba模型有两条主要规则：
简单完整性属性（Simple Integrity Property）：一个主体只能读取完整性级别大于或等于其完整性级别的客体。这防止低完整性信息污染高完整性主体。
*完整性-属性（Integrity Star Property）**：一个主体只能写入完整性级别小于或等于其完整性级别的客体。这防止高完整性主体被低完整性信息污染。
Biba模型是Bell-LaPadula模型的“反向”。Bell-LaPadula防止信息“向上泄露”（从高级别到低级别），Biba防止信息“向下污染”（从低级别到高级别）。
实际应用 —— Biba 模型
Biba模型在实际系统中的应用比Bell-LaPadula模型更少，部分原因是完整性级别比安全级别更难定义和分配。如何确定一个文件的完整性级别？如何确定一个用户的完整性级别？这些问题没有简单的答案。
但在某些场景中，Biba模型仍然有用。比如，在软件系统中，来自可信来源的代码可能有高完整性级别，来自不可信来源的代码可能有低完整性级别。系统可以防止低完整性代码修改高完整性代码，或者防止高完整性进程读取低完整性数据。
Clark–Wilson 模型
Clark-Wilson模型是一个更实用的完整性模型，它专门为商业环境设计。与Biba模型关注信息流不同，Clark-Wilson模型关注数据项（Data Items）的转换和验证。
核心概念
Clark-Wilson模型引入了几个核心概念：
- 受约束数据项（Constrained Data Item，CDI）：需要完整性保护的数据
- 非受约束数据项（Unconstrained Data Item，UDI）：不需要完整性保护的数据（如用户输入）
- 完整性验证过程（Integrity Verification Procedure，IVP）：验证CDI完整性的过程
- 转换过程（Transformation Procedure，TP）：修改CDI的过程
模型规则 —— Clark–Wilson
Clark-Wilson模型有两条主要规则：
认证规则（Certification Rules）：
- IVP必须验证所有CDI的完整性
- TP必须将CDI从一个有效状态转换到另一个有效状态
- TP必须经过认证才能修改CDI
执行规则（Enforcement Rules）：
- 系统必须维护CDI和TP的关联列表
- 只有经过认证的TP才能修改CDI
- 用户必须通过认证和授权才能执行TP
- TP的执行必须被审计
Clark-Wilson模型强调“转换”而不是“直接修改”。数据不能直接被修改，必须通过经过认证的转换过程。这确保了数据的完整性。
实际应用 —— Clark–Wilson
Clark-Wilson模型在商业系统中特别有用，因为它关注实际的数据处理流程。在会计系统中，交易不能直接修改账户余额，必须通过经过验证的交易处理程序。在医疗系统中，患者记录不能直接被修改，必须通过经过认证的医疗程序。
Clark-Wilson模型还强调了职责分离（Separation of Duties）。一个用户可能被允许执行某个TP，但不能执行验证该TP结果的IVP。这防止了单个用户同时执行和验证操作，减少了欺诈和错误的风险。
Chinese Wall 模型
Chinese Wall模型处理利益冲突（Conflict of Interest）的问题。它确保一个主体不能同时访问可能产生利益冲突的信息。
利益冲突
在商业环境中，利益冲突是一个常见问题。比如，一个咨询公司的顾问可能同时为两个竞争客户提供服务。如果顾问可以访问两个客户的机密信息，就可能产生利益冲突——顾问可能无意中或有意地将一个客户的信息泄露给另一个客户。
Chinese Wall模型通过确保主体不能同时访问冲突的信息集来解决这个问题。一旦主体访问了某个信息集，就不能再访问与该信息集冲突的其他信息集。
模型规则 —— Chinese Wall
Chinese Wall模型的基本规则是：
简单Chinese Wall属性：一个主体只能访问与其已访问信息集不冲突的信息集。
这个规则确保了一旦主体“跨过墙”访问了某个信息集，就不能再访问冲突的信息集。这就像在信息集之间建立了一堵“墙”（Chinese Wall），一旦跨过就不能回头。
Chinese Wall模型是动态的。主体的访问权限不是静态的，而是根据其历史访问记录动态调整。一旦访问了某个信息集，就会限制后续的访问。
实际应用 —— Chinese Wall
Chinese Wall模型在金融服务、咨询、法律等行业特别有用。在这些行业中，处理多个客户的信息是常见的，但必须避免利益冲突。
在实际实现中，Chinese Wall模型可能面临挑战。如何定义“冲突”？两个客户在什么情况下会产生利益冲突？这些问题的答案可能不明确，需要根据具体业务场景判断。
信息流安全
信息流安全（Information Flow Security）关注信息如何在系统中流动。它不仅要控制谁可以访问什么信息，还要控制信息如何从一个位置流动到另一个位置。
显式流和隐式流
信息流可以分为显式流（Explicit Flow）和隐式流（Implicit Flow）。显式流是信息通过直接赋值或传递而流动，比如 y = x。隐式流是信息通过控制流而流动，比如 if (x > 0) { y = 1; } else { y = 0; }，即使y的值不直接依赖于x，但y的值仍然泄露了x的信息。
隐式流是信息流安全中最难处理的问题。即使没有直接的数据流，信息仍然可能通过控制流泄露。检测和防止隐式流需要复杂的程序分析技术。
信息流控制
信息流控制需要跟踪信息的"标签"（Label）或"安全级别"。当信息流动时，接收信息的变量或位置必须具有足够高的安全级别。这确保了信息只能流向安全级别足够高的位置。
在实际系统中，信息流控制可能通过以下方式实现：
- 静态分析：在编译时分析程序，检查信息流是否违反安全策略
- 动态跟踪：在运行时跟踪信息的标签，检查信息流
- 类型系统：使用类型系统来编码安全级别，在类型检查时验证信息流
实际挑战 —— 信息流安全
信息流安全在实际应用中面临许多挑战。首先，隐式流很难检测和防止。其次，信息流控制可能影响程序性能，因为需要跟踪和检查标签。第三，信息流控制可能过于严格，阻止合法的信息流动。
尽管有这些挑战，信息流安全仍然是保护敏感信息的重要方法，特别是在处理多级安全系统时。
模型的实际应用与局限性
形式化安全模型提供了精确的安全定义，但在实际应用中，它们往往面临许多挑战和局限性。
模型的简化假设
形式化模型通常基于简化的假设。它们可能假设：
- 安全级别是静态的
- 所有信息都有明确的安全级别
- 系统行为是确定性的
- 没有侧信道攻击
但实际系统往往不满足这些假设。安全级别可能需要动态变化，信息的安全级别可能不明确，系统行为可能有不确定性，侧信道攻击可能泄露信息。
形式化模型的价值在于它们的精确性，但它们的局限性在于它们的简化假设。理解这些假设，以及实际系统在什么程度上满足这些假设，是应用形式化模型的关键。
模型与实现的差距
即使一个系统在理论上满足某个安全模型，在实际实现中可能仍然存在漏洞。实现可能：
- 没有正确实现模型的规则
- 在模型未覆盖的边界情况下存在漏洞
- 受到实现细节（如缓冲区溢出、竞态条件）的影响
这就是为什么需要代码审计、渗透测试、形式化验证等多种方法来确保系统安全。形式化模型是安全设计的重要工具，但不是唯一工具。
多模型组合
在实际系统中，可能需要组合使用多个安全模型。比如：
- 使用Bell-LaPadula模型保护机密性
- 使用Biba模型保护完整性
- 使用Clark-Wilson模型确保数据转换的正确性
- 使用Chinese Wall模型避免利益冲突
但这些模型之间可能有冲突。Bell-LaPadula模型允许高安全级别用户向低安全级别写入（通过*-属性），但Biba模型可能禁止这种行为（如果涉及完整性级别）。如何协调这些模型是一个实际问题。
模型验证
验证系统是否满足形式化安全模型是一个复杂的问题。可能的方法包括：
- 形式化验证：使用数学方法证明系统满足模型
- 模型检查：使用工具自动检查系统是否满足模型
- 运行时监控：在运行时检查系统行为是否违反模型规则
但这些方法都有局限性。形式化验证可能过于复杂，模型检查可能面临状态空间爆炸问题，运行时监控可能影响性能。
总结
形式化安全模型使用数学方法精确地定义安全属性。Bell-LaPadula模型保护机密性，Biba模型保护完整性，Clark-Wilson模型确保数据转换的正确性，Chinese Wall模型避免利益冲突，信息流安全控制信息的流动。
这些模型提供了安全策略的形式化表达，使得安全策略可以被严格地定义、验证和执行。在下一节课中，我们将讨论认证（Authentication），这是实现访问控制的第一步——确认“你是谁”。