《可信计算平台信任链安全性分析.pdf》由会员分享，可在线阅读，更多相关《可信计算平台信任链安全性分析.pdf（12页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、书书书第 卷第期 年月计 算 机 学 报 收 稿 日 期：；最 终 修 改 稿 收 到 日 期：本 课 题 得 到 国 家“八 六 三”高 技 术 研 究 发 展 计 划 项 目 基 金（）、国家 自 然 科 学 基 金（）资 助徐 明 迪，男，年 生，博 士，工 程 师，主 要 研 究 方 向 为 可 信 计 算 与 系 统 安 全 ：张 焕 国，男，年 生，教 授，博 士 生 导 师，主 要 研 究 领 域 为 信 息 安 全 与 可 信 计 算赵恒，女，年 生，博 士，高 级 工 程 师，主要 研 究 方 向 为 软 件 工 程 技 术 与 应 用李 峻 林，男，年 生，研 究 员，主
2、要 研 究 领 域 为 软 件 工 程 技 术 与 应 用严飞，男，年 生，讲 师，主 要 研 究 方 向 为 可 信 计 算可 信 计 算 平 台 信 任 链 安 全 性 分 析徐 明 迪张 焕 国赵恒李 峻 林严飞（武 汉 数 字 工 程 研 究 所武 汉 ）（武 汉 大 学 计 算 机 学 院武 汉 ）（空 天 信 息 安 全 与 可 信 计 算 教 育 部 重 点 实 验 室武 汉 ）摘要可 信 计 算 规 范 是 指 导 可 信 计 算 产 品 研 制 的 依 据，可 信 计 算 规 范 本 身 的 安 全 性 需 要 得 到 验 证信 任 链 是 可信 计 算 平 台 中 保 障
3、系 统 安 全 可 靠 的 主 要 技 术 手 段，它 是 可 信 计 算 平 台 整 个 系 统 安 全 的 中 心 问 题针 对 可 信 计 算 平台 信 任 链 规 范 的 信 息 流 安 全 问 题，文 中 通 过 安 全 进 程 代 数 对 信 任 链 系 统 接 口 进 行 形 式 化 建 模，用 可 复 合 的 不 可 演绎 模 型 刻 画 信 任 链 实 体 间 的 交 互 关 系，把 规 范 定 义 的 信 任 链 行 为 特 性 抽 象 为 多 级 安 全 输 入 输 出 集，在 讨 论 高 级 和低 级 输 入 输 出 依 赖 关 系 的 基 础 之 上，对 信 任 链
4、复 合 系 统 进 行 信 息 流 分 析，并 给 出 结 论 和 证 明关 键 词信 任 链；安 全 进 程 代 数；可 复 合 的 不 可 演 绎 模 型中 图 法 分 类 号 犇 犗 犐号：犛 犲 犮 狌 狉犻狋 狔 犃 狀 犪犾狔 狊犻狊 狅 狀 犜 狉 狌 狊狋 犆 犺 犪犻 狀 狅 犳 犜 狉 狌 狊狋犲 犱 犆 狅 犿 狆 狌 狋犻 狀 犵 犘 犾犪 狋犳 狅 狉 犿 （犠 狌 犺 犪 狀 犇 犻 犵 犻狋 犪 犾 犪 狀 犱 犈 狀 犵 犻 狀 犲 犲 狉犻 狀 犵 犐 狀 狊狋犻狋 狌 狋犲，犠 狌 犺 犪 狀 ）（犛 犮 犺 狅 狅 犾 狅 犳 犆 狅 犿 狆 狌 狋犲 狉
5、，犠 狌 犺 犪 狀 犝 狀 犻 狏 犲 狉 狊犻狋 狔，犠 狌 犺 犪 狀 ）（犓 犲 狔 犔 犪 犫 狅 狉 犪 狋 狅 狉 狔 狅 犳 犃 犲 狉 狅 狊 狆 犪 犮 犲 犐 狀 犳 狅 狉 犿 犪 狋犻 狅 狀 犛 犲 犮 狌 狉犻狋 狔 犪 狀 犱 犜 狉 狌 狊狋 犆 狅 犿 狆 狌 狋犻 狀 犵，犕 犻 狀 犻狊狋狉 狔 狅 犳 犈 犱 狌 犮 犪 狋犻 狅 狀，犠 狌 犺 犪 狀 ）犃 犫 狊狋狉 犪 犮狋 ，犓 犲 狔 狑 狅 狉 犱 狊 ；引言目 前，可 信 计 算 的 相 关 研 究 已 成 为 当 前 国 内 外信 息 安 全 方 面 的 研 究 热 点 和 趋 势 之
6、 一一 方 面，可 信计 算 在 计 算 机 系 统 上 有 着 具 体 的 实 现 和 应 用，如 操 作 系 统 的 通 过 信 任 链 机 制 保 护加 密 分 区 和 卷 主 密 钥，为 了 实 现 对 虚 拟 机 的 动 态 度量，和 生 产 的 增 加 了 支 持 动 态 可信 度 量 根 的 指 令另 一 方 面，可 信 计 算 产 品 的 安 全 测评 也 是 业 界 所 关 注 的 问 题，可 信 计 算 组 织 （）针 对 可 信 平 台 模 块 （）的 设 计 安 全，给 出了 相 应 的 保 护 轮 廓，并 通 过 了 国 际 通 用 标 准 认 证（）公 司 的 产
7、品 通 过 了 认 证 实 验 室 的 认 证 公 司 已 经 开 始 对 生 产 的 进 行 最 严 格 的 硬 件 安 全 评 估 流 程 审 核，计 划 要 达 到 硬 件 安 全 水 平从 其 保 护 轮 廓 的 文 档 描 述 来看，其 主 要 讨 论 的 是 与 平 台 的 唯 一 关 联 性 问题，对 于 其 它 安 全 性 目 标 并 未 涉 及可 信 计 算 产 品 的 设 计 依 据 源 于 规 范 说 明，因 此可 信 计 算 产 品 的 安 全 程 度 和 规 范 说 明 有 着 直 接 联系一 般 来 说，规 范 通 常 是 采 用 自 然 语 言 或 者 非 形 式
8、化 语 言 的 一 种 描 述，很 难 直 接 从 规 范 中 发 现 其 潜 在的 安 全 缺 陷 或 漏 洞目 前，尚 未 对 其 规 范 和 产品 的 安 全 性 进 行 全 面 的 分 析 和 验 证从 公 开 的 文 献来 看，技 术 规 范 中 仅 对 直 接 匿 名 认 证 （）等 协 议 进 行 了 较为 严 格 的 安 全 性 分 析信 任 链 的 交 互 模 型 建 立 过 程 是 将 信 任 链 由 可 信计 算 规 范 进 行 粗 粒 度 抽 取 的 过 程在 这 方 面，国 内 外已 经 有 了 少 量 工 作，和 在 文 献中使 用 授 权 逻 辑 对 下 一 代
9、安 全 计 算 基 的 基 本框 架 和 函 数 进 行 了 形 式 化 描 述，等 人 用谓 词 逻 辑 分 析 了 可 信 启 动 过 程 存 在 的 信 任 链 传 递 所带 来 的 信 任 损 失 问 题，并 提 出 一 种 集 中 式 度 量 的 改进 启 动 模 型，但 该 文 所 提 出 的 模 型 无 法 应 用 于 信任 链 的 测 试 研 究 工 作 等 人 使 用 模 型 检 查器 对 的 若 干 协 议 进 行 了 分 析，发 现 了 授 权 协议 和 远 程 证 明 协 议 中 存 在 的 问 题 等 人 开发 了 一 个 符 号 模 型 检 查 器 来 描 述 可
10、信 启 动 过 程 中 内 部 组 件、和 平 台 其 它 组 件 之 间 的 信 任关 系，但 该 文 主 要 围 绕 的 度 量 问 题 对 信 任 启动 过 程 进 行 建 模，并 未 讨 论 信 任 链 的 具 体 交 互 问 题 使 用 和 分 析 中 调 用 序列 的 安 全 性文 献 通 过 安 全 进 程 代 数 （）和 时 序 逻 辑 对 信 任 链中 的 静 态 度 量 根 （）和 动 态 度 量 根 （）进 行 了 形 式 化 建 模和 证 明，但 是 该 文 对 于 的 一 些 前 提 假 设，如 平 台 配 置 寄 存 器 （）的 写 操 作 问 题、内 存 写 保
11、护 问 题，在 现 有系 统 中 过 于 理 想同 时，信 任 链 由 系 统 中 的 多 个 组 件 构 成，它 建 立于 原 有 计 算 机 硬 件 系 统 基 础 之 上，但 不 是 以 整 体 形式 存 在 于 系 统 中，而 是 各 组 件 与 原 有 系 统 存 在 时 间、空 间 上 的 交 错 状 态，这 种 空 间 上 的 离 散 型，时 间 上的 并 行 性 使 得 信 任 链 的 建 模 变 得 困 难另 一 方 面，信任 链 和 系 统 之 间 通 过 相 互 作 用 形 成 一 个 复 杂 的 系 统整 体 结 构，、和 都 有 各 自 的 输 入、输 出 和 安 全
12、 策 略，从 信 息 流 的 角 度 来 看，复 合 系 统 中不 应 出 现 直 接 或 间 接 的 信 息 泄 露安 全 性 质 的 可 复 合 性 很 重 要，一 方 面 分 解 与 结 合是 构 造 复 杂 系 统 的 有 效 方 法；另 一 方 面，复 杂 的 计 算机 系 统 是 开 放 的，系 统 配 置 可 以 随 时 间 变 化，因 此，复合 安 全 性 质 对 于 定 义 安 全 系 统 是 非 常 必 要 的 本 文 从 可 复 合 的 不 可 演 绎 模 型 出 发，对 可 信 计算 信 任 链 规 范 进 行 形 式 化 建 模，描 述 信 任 链 传 递 过程 中
13、的 实 体 交 互 关 系，通 过 描 述 信 任 链 系 统 的信 息 流 性 质，刻 画 信 任 链 实 体 动 作，抽 象 出 高 低 安 全级 进 程 的 输 入 和 输 出，最 后 用 工 具 对 安 全 属性 进 行 验 证，找 出 规 范 中 存 在 的 安 全 缺 陷 研 究 背 景 基 于 语 言 的 安 全 模 型现 有 的 基 于 语 言 的 安 全 模 型 大 致 上 都 是 扩 展 无干 扰 安 全 的 思 想，在 不 同 层 次 上 刻 划 不 同 安 全 等 级的 访 问 主 体 之 间 的 无 干 扰 关 系，如 等 人扩 展 了 的 建 立 了 安 全 进 程
14、 代 数，将系 统 中 的 名 赋 予“高”、“低”两 种 安 全 级 别，对 无 干 扰模 型 进 行 重 新 定 义 及 分 类，分 析 不 同 安 全 属 性 的 强度 和 使 用 得 出 多 个 无 干 扰 安全 属 性 的 定 义，并 提 出 一 个 建 立 统 一 无 干 扰 定 义 属性 的 构 想 等 人 将 系 统 的 可 靠 性 视 为 某 种无 干 扰 属 性，通 过 证 明 标 准 程 序 语 义 建 立 系 统 的 可靠 性，使 得 所 有 类 型 定 义 良 好 的 程 序 都 具 有 无 干 扰安 全 属 性 安 全 进 程 代 数 的 基 本 语 法安 全 性
15、质 是 信 息 流 性 质 直 接 或 间 接 的 信 息泄 露 都 被 看 作 系 统 中 的 信 息 流 动，都 可 以 使 用 信 息流 分 析 的 技 术 找 到 系 统 中 潜 在 的 各 种 安 全 问 题，对于 信 息 流 安 全 而 言，安 全 属 性 刻 画 了 一 个 安 全 的 多级 系 统 应 该 满 足 的 属 性，信 息 流 分 析 的 技 术 源 于 基本 无 干 扰（）模 型，后 来 又 相 继 出 现 了 不 可 推 断（）模 型、输 入 不 可 演 绎（）模 型 但这 些 安 全 属 性 都 是 不 可 复 合 的后 来 又 有 学 者 提 出计 算 机 学
16、 报 年了 策 略 不 可 演 绎（）模 型 和 可 复 合 的 不 可 演 绎（）模 型 进 程 代 数 作 为 描 述 互 作 用 系 统 的 一 般 框 架，适合 于 研 究 安 全 信 息 流 性 质在 进 程 代 数 框 架 内 研 究信 息 流 性 质，不 仅 可 以 对 其 进 行 概 括 和 比 较，而 且 还可 以 利 用 进 程 代 数 中 的 某 些 结 果 更 抽 象 更 深 刻 地 理解 安 全 性 及 其 结 合 性 质 本 文 使 用 的 安 全 进 程 代数 语 言 ，是 的 简 单 扩 展 的 基 本 语 法符 号 包 括：（）进 程 动 作 集犃 犮狋它 由
17、部 分 组 成：无 穷 名集犐，犐的 伴 名 集犗，一 个 称 为 哑 名 的 元 素其 中，犐犪，犫，表 示 输 入 动 作 集；犗珔犪，珔犫，表 示 输出 动 作 集；?犐犗表 示 可 见 动 作 集 合，表 示 不 可见 动 作更 进 一 步，为 了 描 述 多 级 安 全 系 统 中 不 同 安全 级 之 间 的 信 息 流 关 系，将 可 见 动 作 集?划 分为 两 个 安 全 级：高 安 全 级 动 作犃 犮狋犎和 低 安 全 级 动 作犃 犮狋犔，并 且犃 犮狋犎犃 犮狋犎 犐犃 犮狋犎 犗，犃 犮狋犔犃 犮狋犔 犐犃 犮狋犔 犗，犃 犮狋犎犃 犮狋犔?，犃 犮狋犎犃 犮狋犔，
18、犃 犮狋犃 犮狋犎犃 犮狋犔，通 常 用表 示 进 程 动 作 集（）进 程 变 量 集，并 以犡，犢，犣等 表 示 进 程 变量；进 程 常 量 集?，并 以犃，犅等 表 示 进 程 变 量（）算 子 符 号，分 别 表 示 前缀 算 子、选 择 算 子、并 行 算 子、复 合 算 子、限 制 算 子 和隐 藏 算 子定 义 无 穷 名 集犐与 伴 名 集犗之 间 的 二 元 关系：?为犪犐犪犗，犪犗犪犪犐根 据 定 义，对 于 集 合犔，犔?的 伴 名 集珚犔，有珚犔：犔，为 了 表 示 方 便，以 后 我 们 用犳表 示二 元 关 系，对 于犃 犮狋有犳（）犳（），如 果，那 么犳（）进
19、 程 项 集 合?是 如 下 语 法 构 造 的 集 合：犈 犈犈犈犈犈犈犔犈犐犔犈犔犈犳，其 中犔?符 号用 于 表 示 不 做 任 何 动 作 的 空 进 程；犈表 示 做 完 动 作后 的 系 统 行 为犈；犈犈表 示 选 择犈或 者犈；犈犈表 示 系 统犈和犈之 间 进 行 交 织并 发，并 且 对 互 补 的 输 入输 出 动 作 进 行 同 步，将 其作 为 一 个 内 部 动 作；犈犔执 行 属 于犈但 不 属 于犔珚犔集 合 的 动 作；犈犐犔执 行 属 于犈但 不 属 于犔犐集 合 的 动 作；犈犔将犈中 所 有 属 于犔的 动 作 转 换为 内 部 动 作；如 果犈可 以
20、执 行 动 作，那 么犈犳执 行犳（）；常 量的 定 义 为 犈，也 就 是具 有犈的 所 有 功 能 除 了 对 中 的 动 作 集犔进 行 高 低 安 全等 级 划 分 以 外，还 引 入 了 两 种 算 子：限 制 算 子 和 隐 藏算 子限 制 算 子犈犔执 行 属 于 集 合犈犔珚犔的 动作，带 输 入 限 制 的 算 子犈犐犔执 行 属 于 集 合犈犔犐的 动 作；隐 藏 算 子犈犔把 在 集 合犈犔中 的动 作 转 换 为 不 可 见 动 作用?（犈）表 示 进 程犈所 有 的 动 作 执 行 迹，那 么 高安 全 级 进 程 和 低 安 全 级 进 程 分 别 被 定 义 为?
21、犎 犈?（犈）犃 犮狋犎 和?犔 犈?（犈）犃 犮狋犔 的 操 作 语 义 的 操 作 语 义 模 型 是 标 记 变 迁 系 统 模 型（?，犃 犮狋，），其 中 二 元 关 系?犃 犮狋?的 结 构化 操 作 语 义，如 图所 示前 缀 犈犈选 择犈犈 犈犈犈 犈犈 犈犈犈 并 行犈犈 犈犈犈 犈 犈犈 犈犈犈犈 犈犈，犈犈 犈犈犈 犈 限 制犈犈 犈犔犈 犔，犔珚犔输 入 限 制犈犈 犈犐犔犈 犐犔，犔犐隐 藏犈犈 犈犔犈 犔，犔 犈犈 犈犔犈 犔，犔转 换犈犈 犈犳犳（）犈 犳常 量犈犈 犃犈，犃 犈图 的 结 构 化 操 作 语 义期徐 明 迪 等：可 信 计 算 平 台 信 任 链
22、 安 全 性 分 析除 了 图中 对 常 用 操 作 算 子 的 描 述 以 外，文 献 还 提 出 了 使 用 并 行 算 子 和 限 制 算 子 来 实 现 复 合算 子 的 功 能复 合 算 子 要 求 两 个 系 统犈和犉通 过 并行 方 式 构 成 一 个 新 的 复 合 系 统，并 同 步犈，犉之 间 的互 补 动 作定 义 系 统犈和犉的 复 合 系 统 为犈犉 （犈犉）（?（犈）?（犉）的 迹 语 义 和 互 模 拟 语 义迹 是 理 论 中 的 重 要 概 念，它 是 系 统 中 可 观察 动 作 所 组 成 的 一 个 有 限 序 列定 义 犈?，犈的 迹犜（犈）?犈犈 其
23、 中狀?犈犈 当 且 仅 当犈，犈，犈狀?犈犈狀犈狀，其 中犈狀犈 犈犈 表 示犈（）犈犈（）犈（）表示 内 部 动 作 序 列当犈犈 成 立，我 们 认 为 系 统 从 状 态犈到 达 状态犈，从 观 察 的 角 度 来 看，系 统 从 状 态犈到 状 态犈 所 执 行 的 动 作 轨 迹 是，狀定 义 犈，犉?，犈和犉迹 等 价 当 且 仅 当犜（犈）犜（犉），记 为犈犜犉为 了 能 比 较 迁 移 系 统 的 中 间 状 态，文 献 提出 了 互 模 拟 等 价 的 概 念互 模 拟 刻 画 了 两 个 系 统 之间 的 单 步 模 拟 思 想，也 就 是 说，当 进 程犈执 行 一 个
24、动 作 到 达犈 后，进 程犉也 必 须 能 够 通 过 执 行 同 样 的动 作 到 达犉，进 而 模 拟犈所 完 成 的 单 步 过 程，进 程犈 和犉 继 续 重 复 进 行 接 下 来 的 单 步 过 程定 义 二 元 关 系犚?是 弱 互 模 拟，如 果（犈，犉）犚，犃 犮狋（）无 论 何 时犈犈，都 存 在犉?使 得犉犉 和（犈，犉）犚成 立（）无 论 何 时犉犉，都 存 在犈?使 得犈犈 和（犈，犉）犚成 立两 个 进 程 项犈，犉?的 观 察 等 价 记 为犈犅犉，如 果 存 在 着 一 个 包 含（犈，犉）的 弱 互 模 拟 二 元 关系犚 信 任 链 规 范 安 全 性 分
25、 析 可 复 合 的 不 可 演 绎 安 全 性 质复 合 安 全 性 质 是 构 成 复 合 系 统 安 全 理 论 的 基础，可 复 合 安 全 性 是 在 分 析 复 合 系 统安 全 性 时 引 入 的 一 个 概 念 可 复 合 性 是 安 全 性 质的 重 要 特 性，所 谓 一 种 安 全 性 质是 可 复 合 的，是指 两 个 或 多 个 满 足 性 质的 进 程，通 过 复 合 算 子 构成 的 复 合 进 程犘时，这 个 复 合 进 程犘仍 满 足在对 不 可 演 绎 模 型 进 行 形 式 化 描 述 之 前，我 们 先 给 出相 关 的 符 号 说 明：犜：系 统 的
26、执 行 序 列犞：系 统 执 行 序 列狋，狋犜后 的 值犳：犜犞：从 执 行 序 列犜到 值犞的 信 息 函 数，表 示 系 统 当 前 视 图，或 者 是 一 组 值 或 变 量 （犳）：所 有 执 行 序 列 的 视 图 集 合，即狋犜，犳（狋）（犳）定 义 令，（?）是 两 个 迹，是的一 个 子 序 列（用 表 示）当 且 仅 当 和满 足 关系：狀，犽，（）犽，（犿），其 中犿狀，犽，：，犿，狀是 一 个 单 调 递 增 函 数，犻表示犻出 现 在 序 列中定 义 视 图 函 数犾 狅 狑，犺 犻 犵 犺 犻 狀 狆 狌 狋，犾 狅 狑 犻 狀 狆 狌 狋，犻 狀 狆 狌 狋分 别
27、 被 定 义 为（）犾 狅 狑：?犃 犮狋犔那 么 有 犾 狅 狑（），如 果犻，犻犃 犮狋犔 犼：犻犽，（犼）（）犺 犻 犵 犺 犻 狀 狆 狌 狋：?（犃 犮狋犎犐）那 么 有 犺 犻 犵 犺 犻 狀 狆 狌 狋（），如 果犻，犻犃 犮狋犎犐 犼：犻犽，（犼）（）犾 狅 狑 犻 狀 狆 狌 狋：?（犃 犮狋犔犐）那 么 有 犾 狅 狑 犻 狀 狆 狌 狋（），如 果犻，犻犃 犮狋犔犐 犼：犻犽，（犼）（）犻 狀 狆 狌 狋：?犐那 么 有 犻 狀 狆 狌 狋（），如 果犻，犻犐 犼：犻犽，（犼）犾 狅 狑得 到 动 作 序 列 中 的 所 有 低 安 全 级 动 作，犺 犻 犵 犺 犻 狀
28、 狆 狌 狋得 到 动 作 序 列 中 的 高 安 全 级 输 入 动 作，犾 狅 狑 犻 狀 狆 狌 狋得 到 动 作 序 列 中 的 低 安 全 级 输 入 动 作，犻 狀 狆 狌 狋得 到 动 作 序 列 中 的 所 有 输 入 动 作定 义 令犳和犳是 两 个 信 息 函 数 且狑 （犳）对 于 视 图狑而 言，信 息 从犳流 向犳当 且 仅 当狏 （犳），狋犜，犳（狋）狏犳（狋）狑定 义假 定 了犳和犳分 别 对 应 着 高 安 全 级 进程 和 低 安 全 级 进 程，如 果 存 在 从犳和犳的 信 息 流，那 么 对 于 系 统 中 的 任 意 迹狋来 说，即 使 曾 有狑 （犳
29、），但 由 于 低 安 全 级 进 程犳的 当 前 视 图 已经 被 高 安 全 级 进 程犳所 影 响，因 此 导 致 了犳（狋）狑定 义的 另 外 一 层 含 义 是：如 果 信 息 从犳流 向 了计 算 机 学 报 年犳，说 明 了犳的 输 入 影 响 了犳的 输 出，那 么 就 认 为犳能 够 演 绎 出犳的 输 入那 么 在 什 么 情 况 下犳不 能 演 绎 出犳的 输 入 呢？我 们 给 出 如 下 定 义定 义 给 定犜，犳和犳，信 息 没 有 从犳流 向犳当 且 仅 当 联 合 函 数（犳，犳）与 视 图 积 （犳）（犳）之 间 满 足 映 成 关 系（）这 里 的 映 成
30、关 系 指（犳，犳）与 （犳）（犳）满 足 一 一 映 射换 句 话 说，如 果 对 于 每 一个犃 犮狋犔，都 存 在 着 迹狋犜（犈）使 得犾 狅 狑（狋），并 且 对 于 每 一 个（犃 犮狋犎犐），也 都 存 在 着 迹狋犜（犈）使 得 犺 犻 犵 犺 犻 狀 狆 狌 狋（狋），那 么 一 定 存 在 着一 条 迹狋，其 低 安 全 级 视 图 是，高 安 全 级 视 图是 输 入 不 可 演 绎 模 型 源 自 提 出 的 信息 流 安 全 理 论 根 据 输 入 不 可 演 绎 模 型，所 谓 不存 在 信 息 流，意 味 着 从 进 程 行 为 的 低 级 观 察 中，不 能演
31、绎 地 推 导 出 关 于 进 程 高 级 行 为 的 任 何 性 质，或 者说 进 程犈具 有 不 可 演 绎 性 质，如 果 进 程 的 任 何 低 级可 观 察 行 为犾 狅 狑都 不 能 推 导 出 高 级 输 入犺 犻 犵 犺 犻 狀 狆 狌 狋的 任 何 信 息前 面 我 们 对 输 入 不 可 演 绎 模 型 进 行 了 定 义，下面 我 们 用 给 出 可 复 合 的 不 可 演 绎 性 质 的 定 义定 义 安 全 性 质是 可 复 合 的，如 果犘，犙犘犙定 义 令犎犃 犮狋犎，犈?，那 么犈具 有 可复 合 的 不 可 演 绎 性 质 当 且 仅 当?犎犾 狅 狑 狏 犻
32、犲 狑 狊（犈）犾 狅 狑 狏 犻犲 狑 狊（犈）犎），这 里 的犾 狅 狑 狏 犻犲 狑 狊（）函 数 是犾 狅 狑（）函 数 的 幂 集：犾 狅 狑 狏 犻犲 狑 狊（犈）犃 犮狋犔 犜（犈）信 任 链 规 范 说 明我 们 在 文 献中 提 出 了 可 信 计 算 规 范 说明 模 型，将 可 信 计 算 平 台 抽 象 为 、和 个 实 体 间 的 交 互 模 型，该 模 型 描 述 了 信 任链 建 立 过 程 中 的 实 体 交 互 关 系从 安 全 进 程 代 数 的 角 度 考 虑，为 了 能 够 分 析 信任 链 建 立 过 程 的 信 息 流 安 全，我 们 需 要 进 一
33、 步 对 实体 的 交 互 关 系 进 行 细 化，定 义 出 实 体 间 的 输 入 和 输出，从 安 全 的 角 度 对 这 些 输 入 输 出 进 行 等 级 划 分，验证 信 任 链 系 统 所 符 合 的 安 全 属 性可 信 计 算 规 范 给 出 了 静 态 可 信 度 量 根（）的 实 现 流 程 和 方 法，图刻 画 了 运行 期 间个 进 程 间 的 输 入 和 输 出其 中 包 括了 、和 通 过 所 提 供 的 服 务 接 口 对 进 行 访 问 请 求；包 含 了种 访 问 的 方 式：应 用 层 驱 动、驱 动 和 驱 动，会 自 动 把来 自 的 应 用 层 驱
34、动 请 求 转 换 为 驱 动 方 式 发 送 给 ，驱 动 通 过 （）通 道 与 进 行 通 信，驱 动 通 过 （）通道 与 进 行 通 信图给 出 了 这 些 输 入 输 出 接口 的 函 数，可 以 看 出，驱 动 不 对 外 提 供 任何 服 务，仅 完 成 阶 段 的 完 整 性 度 量，而 驱 动 则 更 多 地 处 理 来 自 内 部 或 外 部 的 访问 请 求下 面 我 们 用 语 法 对 这个 进 程 实 体 做进 一 步 说 明首 先，为 了 精 确 刻 画 文 献中 对 、和 个 实 体 间 的 交 互 关 系，我 们 需 要 细 化 信任 链 规 范 说 明 中个
35、 实 体 交 互 时 的 输 入 输 出定 义 令 表 示 信 任 链 规 范 说 明，则 （）犛 狔，其 中 限 制 集 合犛 狔用 于 实 体 间 的 动 作 同 步 主 要 包 含 了 迭 代（犲 狓 狋犲 狀 犱）、度 量（狉 犲 犪 犱）内 存 代 码、建 立（犾 狅 犵）度 量 日 志 和 执 行（犮 犪 犾犾）被 度 量 代 码 等 操 作，这 里，我 们 把狉 犲 犪 犱、犲 狓 狋犲 狀 犱、犮 犪 犾犾和犾 狅 犵动 作 分 别 定 义 为 读（狉）、写（狑）、执 行（犲）和 追加（犪）操 作，并 将 图中 的 接 口 函 数 进 行 归 纳，那 么可 以 得 到 如 下
36、描 述：狉犘 犗 犛 犜 犅 犐 犗 犛犿 犪犎 犪 狊 犺 犃 犾犾 犈 狓 狋犲 狀 犱 犜 犘 犕犲犘 犗 犛 犜 犅 犐 犗 犛 犪犛 犢 犛 犜 犈 犕犃 犆 犘 犐狊 犿 犻 犝 狆 犱 犪 狋犲 犔 狅 犵 犈 狏 犲 狀 狋 犪犚 犜 犕犃 犆 犘 犐狊 犿 犻 犝 狆 犱 犪 狋犲 犔 狅 犵 犈 狏 犲 狀 狋 犲犘 犗 犛 犜 犅 犐 犗 犛狉犗 狆 狋犻 狅 狀 犚 狅 犿 狊犿 狆犜 犘 犕 犜 狉 犪 狀 狊 犿 犻狋犪犚 犜 犕犃 犆 犘 犐犲犗 狆 狋犻 狅 狀 犚 狅 犿 狊狉犐 犘 犔犿 狆犜 犘 犕 犜 狉 犪 狀 狊 犿 犻狋犪犚 犜 犕犃 犆 犘 犐犲
37、犐 犘 犔 犲犗 狆 狋犻 狅 狀 犚 狅 犿 狊犲犐 犘 犔狉犌 犚 犝 犅狋犮 犵犘 犪 狊狊 犜 犺 狉 狅 狌 犵 犺 犜 狅 犜 犘 犕犪犛 狔 狊狋犲 犿犃 犆 犘 犐犲犌 犚 犝 犅 狋犮 犵犘 犪 狊狊 犜 犺 狉 狅 狌 犵 犺 犜 狅 犜 犘 犕狑犘 犆 犚 犿 犪犎 犪 狊 犺 犃 犾犾 犈 狓 狋犲 狀 犱 犜 犘 犕狑犘 犆 犚 犿 狆犜 犘 犕 犜 狉 犪 狀 狊 犿 犻狋狑犘 犆 犚 期徐 明 迪 等：可 信 计 算 平 台 信 任 链 安 全 性 分 析图 可 信 计 算 平 台 规 范 说 明 输 入 输 出 接 口 中 的 动 作犪犛 狔 狊狋犲 犿犃 犆
38、犘 犐和狋犮 犵犘 犪 狊狊 犜 犺 狉 狅 狌 犵 犺 犜 狅 犜 犘 犕分 别 表 示 创 建 度 量 日 志 请 求 和 应 用 层 访 问 请求；中 的 动 作犿 犪犎 犪 狊 犺 犃 犾犾 犈 狓 狋犲 狀 犱 犜 犘 犕和犿 狆犜 犘 犕 犜 狉 犪 狀 狊 犿 犻狋表 示 层 访 问 请 求；对 于 前 面 和 的 输 出 动 作，对 应的 有个 同 步 动 作：犿 犪犎 犪 狊 犺 犃 犾犾 犈 狓 狋犲 狀 犱 犜 犘 犕狑犘 犆 犚 、犿 狆犜 犘 犕 犜 狉 犪 狀 狊 犿 犻狋狑犘 犆 犚 和狋犮 犵犘 犪 狊狊 犜 犺 狉 狅 狌 犵 犺 犜 狅 犜 犘 犕狑犘 犆
39、犚 其 余 同 步动 作 用 于 保 证 代 码 和 数 据 的 完 整 性，防 范 攻 击 安 全 性 分 析我 们 在 文 献中 刻 画 出 了 信 任 链 交 互 模 型，其中 与 组 成 ，与 之 间 通过 位 于 高 端 内 存 的 两 个 驱 动 程 序 进 行 通 信，其 动 作对 于 来 说 是 不 可 见 的我 们 再 对 做 进一 步 细 化，被 划 分 为 和 ，与 在 内 部 进 行 复 合，其 内部 动 作 对 于 和 来 说 也 是 不 可 见 的并且 我 们 认 为 和 是 绝 对 可 信 的，所 有 的 动作 都 属 于 高 安 全 级 动 作另 一 方 面，与
40、 组 成 的 需 要 再 次 与 进 行 复 合，由 于计 算 机 学 报 年 中 的 所 有 组 件 的 安 全 级 别 都 要 比 低，因 此 中 的 所 有 动 作 都 属 于 低 安 全 级 动 作，这 里 我 们 考 虑 的 问 题 是：能 够 观 察 出 中 的 高 安 全 级 动 作 或 者 输 出 策 略 吗？在 分 析 该 问 题之 前，我 们 先 给 出 相 关 的 符 号 定 义犻 狀犈犻：系 统犈的 外 部 输 入 序 列；狅 狌 狋犈犼：系 统犈的 外 部 输 出 序 列犮犿：系 统犈的 指 令 输 入 序 列；犮犿：系 统犈的 指 令 输 出 序 列犱狀：系 统犈的
41、 数 据 输 入 序 列；珚犱狀：系 统犈的 数 据 输 出 序 列狊狔：系 统犈的 同 步 输 入 序 列；狊狔：系 统犈的 同 步 输 出 序 列狉犽：系 统犈的 结 果 输 入 序 列；狉犽：系 统犈的 结 果 输 出 序 列这 里 的 外 部 输 入 和 外 部 输 出 序 列 是 指 系 统 通 过吸 收 外 部 激 励 动 作 或 事 件 而 产 生 的 外 部 输 出 动 作 或事 件对 于 信 任 链 复 合 模 型 而 言，以 触 发 相关 动 作 与 进 行 通 信 而 完 成 某 种 功 能，如 通过 来 访 问 ，进 而 完 成 对 的 完 整性 度 量 和 完 整 性
42、 存 储因 此 的 输 入 事 件 对 于 来 说 就 是 一 种 外 部 激 励 输 入，经 过 内 部 对 该输 入 动 作 的 处 理，完 成 与 之 间 的 内 部 同步 并 将 结 果 作 为 外 部 输 出 返 还 给 下 面 我 们 对 与 的 复 合、与 的 复 合、与 的 复 合 分 别进 行 讨 论 与 的 复 合在 信 任 链 建 立 初 期，需 要 通 过 驱 动 对 进 行 完 整 性 度 量 和 完 整 性存 储，为 了 方 便 表 示，这 里 我 们 用犻 狀 ，狅 狌 狋 分别 表 示 完 整 性 度 量 输 入 和 输 出，犻 狀 ，狅 狌 狋 分 别表 示
43、完 整 性 存 储 输 入 和 输 出，它 们 都 是 对 外所 呈 现 的 视 图；犮，犮表 示 发 给 的 指 令序 列 输 入 和 输 出，犱，珚犱表 示 发 给 的数 据 序 列；狊狔，狊狔表 示 与 之 间 的 同 步 信号，对 于 实 际 的 信 任 链 系 统 而 言 同 步 信 号 通 常 是 硬件 总 线；符 号狉，狉，狉，狉对 应 着 所 完 成 的 完整 性 度 量 结 果 和 完 整 性 存 储 结 果我 们 在 前 面 已 经 说 明 了 和 中 的所 有 动 作 都 属 于 高 安 全 级 动 作，因 此 当 与 进 行 复 合 之 后，需 要 同 步 的 高 安
44、全 级 动 作 统 统都 转 换 为 内 部 动 作，该 动 作 和 高 安 全 级 动 作 对 于低 安 全 级 视 图 是 不 可 见 的 与 的 复 合模 型 如 图所 示图 与 的 复 合 模 型用 进 行 描 述 的 与 复 合 系 统的 表 示 如 下 所 示：（）犛 狔；犻 狀 狊狔犮 犻 狀 狊狔珚犱 狉狅 狌 狋 狉狅 狌 狋 ；狊狔犮狉 狊狔犱狉 狊狔犮狉 狊狔犱狉 ；犛 狔狊狔，狊狔，犮，犮，犱，珚犱，狉，狉，狉，狉；犃 犮狋犎狊狔，狊狔，犮，犮，犱，珚犱，狉，狉，狉，狉，犻 狀 ，狅 狌 狋 ，犻 狀 ，狅 狌 狋 经 过 复 合 算 子 操 作 后 的 系 统 如 图
45、所 示，为 了图 形 显 示 方 便，我 们 只 选 取 了 并 发 系 统 中 的 一 条 分支，可 以 看 出，该 分 支 中 含 有个 内 部 动 作和 两 个高 安 全 级 动 作犻 狀 ，狅 狌 狋 图 与 的 系 统 与 的 复 合当 对 度 量 完 毕 后，需 要 对 的 第 一 个 启 动 组 件 进 行 完 整性 度 量 和 完 整 性 存 储这 里 的 符 号 描 述 和 描 述与 上 一 小 节 基 本 相 同，不 再 赘 述 与 的 复 合从 上 面 两 小 节 可 以 知 道，、和 所 组 成 的 中 所 有 的 输 入 输 出 动期徐 明 迪 等：可 信 计 算 平
46、 台 信 任 链 安 全 性 分 析作 都 是 高 安 全 级 动 作那 么 对 于 动 作 序 列犻 狀 狅 狌 狋 和犻 狀 狅 狌 狋 来说，由 于犻 狀 和狅 狌 狋 是 高 安 全 级 动 作，且 没 有 低安 全 级 输 入输 出 对 高 安 全 级 动 作 的 依 赖，因 此 复 合系 统 、都 满 足 和 安 全 属 性那 么 满 足 和 安 全 性 质 的 与 复 合 之 后 是 否 仍 然 满 足 和 安 全属 性 呢？我 们 先 给 出 与 的 复 合 模 型，如图所 示该 模 型 和 上 面 两 个 复 合 模 型 的 不 同 之 处在 于，由 于 中 的 所 有 动
47、作 都 是 低 安 全 级 动作，因 此，当 与 进 行 复 合 的 时 候，完 成完 整 性 度 量 和 完 整 性 存 储 任 务 的 指 令 输 入 输 出 序列、数 据 输 入 输 出 序 列 和 结 果 输 入 输 出 序 列，不 能 简单 地 将 它 们 视 为 同 步 操 作 而 化 简 为 内 部 动 作，因 此这 里 需 要 对 这 些 序 列 进 行 安 全 视 图 上 的 区 分图 与 的 复 合 这 里 我 们 将 同 步 动 作 集犛 狔仅 包 含 信 号 同 步 动 作狊狔，狊狔，系 统 与 进 行 交 互 的 动 作 集 包 括犮 ，珚犱 ，狉，狉，分 别 表 示
48、 指 令 序 列、数 据 序 列、完 整 性 度 量 结 果 序 列 和 完 整 性 存 储 结 果 序 列 的输 入 输 出 集 分 别 为犻 狀 ，犻 狀 ，狅 狌 狋 ，狅 狌 狋 ，复 合 系 统 的 描 述 如 下 所 示 （）犛 狔；犻 狀 狊狔犮 狉狅 狌 狋 犻 狀 狊狔犱 狉狅 狌 狋 犻 狀 狊狔犮 狉狅 狌 狋 犻 狀 狊狔犱 狉狅 狌 狋 ；狊狔犻 狀 狅 狌 狋 狊狔犻 狀 狅 狌 狋 狊狔犻 狀 狅 狌 狋 狊狔犻 狀 狅 狌 狋 ；犛 狔狊狔，狊狔；犃 犮狋犎狊狔，犻 狀 ，狅 狌 狋 ，犻 狀 ，狅 狌 狋 若 考 虑 所 有 的 动 作 集 合 那 么 最 终
49、 的 系 统将 异 常 庞 大，根 据 上 述 描 述，我 们 只 考 虑 动 作 集 合犻 狀 ，狅 狌 狋 ，狊狔，狊狔，犮 ，狉为 了 显 示 方 便，我们 对 变 迁 系 统 的 片 段 进 行 分 析，如 图所 示可 以 看出，当 系 统 处 于 状 态狅 狌 狋 狅 狌 狋 犛狔时，可 以 选 择 动 作狅 狌 狋 或 者狅 狌 狋 ，由 于 动 作狅 狌 狋 是 一 个 低 安 全 级 输 出，到达 状 态狅 狌 狋 狅 狌 狋 犛狔是 通 过动 作狉或 者犻 狀 ，而 动 作犻 狀 是 一 个 高 安全 级 输 入，也 就 是 低 安 全 级 输 出 依 赖 高 安 全 级 输
50、 入，因 此 复 合 系 统 不 再 符 合 安 全 属性，对 于 实 际 的 信 任 链 系 统 而 言，我 们 将 在 节 详细 说 明 中 的 哪 些 动 作 依 赖 于 中 的动 作图 与 的 部 分 系 统计 算 机 学 报 年 进 一 步 的 分 析通 过 节 对 信 任 链 复 合 模 型 的 分 析 得 知，与 的 复 合 系 统 既 然 不 满足 安 全 属 性，同 样 也 就 不 满 足 属 性那 么究 竟 要 满 足 什 么 样 的 条 件 才 能 达 到 这一 要 求 呢？定 义 对 进 程犈的 可 复 合 不 可 演 绎 性质 定 义 采 用 的 是 模 型，并 采