| 摘要 | 第10-12页 |
| ABSTRACT | 第12-14页 |
| 第一章 绪论 | 第15-25页 |
| 1.1 研究背景 | 第15-18页 |
| 1.1.1 面向形式化验证的可满足问题求解 | 第15-16页 |
| 1.1.2 开放计算环境下数据安全威胁 | 第16-18页 |
| 1.2 研究意义 | 第18-22页 |
| 1.2.1 开放计算环境下可满足问题求解的数据安全问题 | 第18-21页 |
| 1.2.2 已有工作的局限 | 第21-22页 |
| 1.3 本文的主要工作 | 第22-23页 |
| 1.3.1 研究内容与创新点 | 第22-23页 |
| 1.4 论文组织结构 | 第23-25页 |
| 第二章 相关研究 | 第25-45页 |
| 2.1 混淆技术研究 | 第25-29页 |
| 2.1.1 混淆理论研究 | 第25-27页 |
| 2.1.2 程序混淆 | 第27-28页 |
| 2.1.3 电路混淆 | 第28-29页 |
| 2.2 外包计算的隐私保护研究 | 第29-33页 |
| 2.2.1 基于同态加密的方法 | 第30-32页 |
| 2.2.2 基于数据伪装的方法 | 第32-33页 |
| 2.3 可验证计算技术研究 | 第33-34页 |
| 2.4 可满足问题以及相关概念 | 第34-39页 |
| 2.4.1 可满足问题定义 | 第34-35页 |
| 2.4.2 Tseitin编码 | 第35页 |
| 2.4.3 可满足问题求解 | 第35-38页 |
| 2.4.4 可满足赋值遍历 | 第38-39页 |
| 2.5 基于可满足问题求解的对偶综合设计研究 | 第39-44页 |
| 2.5.1 早期的充分非完备算法 | 第39-41页 |
| 2.5.2 完备停机算法 | 第41-43页 |
| 2.5.3 基于迁移关系(函数)展开的形式化验证算法的一般性原理 | 第43-44页 |
| 2.6 本章小结 | 第44-45页 |
| 第三章 基于合取范式混淆的可满足问题求解 | 第45-63页 |
| 3.1 引言 | 第45页 |
| 3.2 问题描述 | 第45-47页 |
| 3.3 基于CNF混淆的SAT求解方法 | 第47-53页 |
| 3.3.1 SAT求解框架 | 第47-48页 |
| 3.3.2 单一Husk公式产生算法 | 第48-49页 |
| 3.3.3 解空间保持的混淆算法 | 第49-52页 |
| 3.3.4 映射和验证算法 | 第52-53页 |
| 3.4 理论分析 | 第53-61页 |
| 3.4.1 正确性证明 | 第53-59页 |
| 3.4.2 有效性分析 | 第59-60页 |
| 3.4.3 算法复杂性分析 | 第60-61页 |
| 3.5 实验评估 | 第61-62页 |
| 3.5.1 实验设计 | 第61页 |
| 3.5.2 实验结果分析 | 第61-62页 |
| 3.6 本章小结 | 第62-63页 |
| 第四章 解空间投影等价的合取范式混淆算法 | 第63-75页 |
| 4.1 引言 | 第63页 |
| 4.2 问题描述 | 第63-64页 |
| 4.2.1 可满足赋值遍历 | 第63-64页 |
| 4.2.2 基于ALLSAT求解和分区的攻击 | 第64页 |
| 4.3 解空间投影等价的混淆算法 | 第64-69页 |
| 4.3.1 部分赋值Husk公式的产生 | 第65-66页 |
| 4.3.2 解空间投影等价的混淆 | 第66-69页 |
| 4.3.3 解恢复和验证算法 | 第69页 |
| 4.4 理论分析 | 第69-73页 |
| 4.4.1 正确性证明 | 第69-73页 |
| 4.4.2 安全性分析 | 第73页 |
| 4.5 本章小结 | 第73-75页 |
| 第五章 带噪音解的结构感知合取范式混淆算法 | 第75-99页 |
| 5.1 引言 | 第75页 |
| 5.2 问题描述 | 第75-76页 |
| 5.3 威胁模型 | 第76页 |
| 5.4 系统设计 | 第76-85页 |
| 5.4.1 基于混淆的SAT求解框架 | 第76-78页 |
| 5.4.2 Husks公式的产生 | 第78页 |
| 5.4.3 解空间上估计的混淆 | 第78-84页 |
| 5.4.4 真实解的恢复 | 第84-85页 |
| 5.5 理论分析 | 第85-94页 |
| 5.5.1 正确性证明 | 第85-92页 |
| 5.5.2 有效性分析 | 第92-93页 |
| 5.5.3 安全性分析 | 第93-94页 |
| 5.5.4 算法复杂性分析 | 第94页 |
| 5.6 实验评估 | 第94-97页 |
| 5.6.1 实验方案设计 | 第94-95页 |
| 5.6.2 实验结果分析 | 第95-97页 |
| 5.7 结论 | 第97-99页 |
| 第六章 基于可满足问题的流控感知对偶综合 | 第99-125页 |
| 6.1 引言 | 第99-100页 |
| 6.2 背景知识 | 第100-103页 |
| 6.2.1 有限状态机 | 第100-101页 |
| 6.2.2 Craig插值的原理和实现 | 第101-103页 |
| 6.2.3 非迭代的特征化算法 | 第103页 |
| 6.3 基于余因子和Craig插值的迭代特征化算法 | 第103-106页 |
| 6.3.1 迭代的特征化算法 | 第105-106页 |
| 6.3.2 小结 | 第106页 |
| 6.4 识别流控变量 | 第106-108页 |
| 6.4.1 识别流控变量f | 第106-107页 |
| 6.4.2 使用增量SAT求解器加速识别算法 | 第107-108页 |
| 6.5 推导唯一化谓词 | 第108-116页 |
| 6.5.1 计算valid(f)的单调增长的下估计 | 第110-111页 |
| 6.5.2 计算valid(f)的单调递减上估计 | 第111-113页 |
| 6.5.3 计算valid(f)的算法 | 第113页 |
| 6.5.4 停机和正确性证明 | 第113-116页 |
| 6.6 压缩迁移关系展开序列的长度 | 第116页 |
| 6.7 产生解码器函数 | 第116-119页 |
| 6.7.1 产生流控f的解码函数 | 第116-118页 |
| 6.7.2 产生数据d的解码函数 | 第118-119页 |
| 6.8 实验结果 | 第119-124页 |
| 6.8.1 测试集 | 第119页 |
| 6.8.2 PCI Express 2.0编码器 | 第119-120页 |
| 6.8.3 10G以太网编码器XGXS | 第120-121页 |
| 6.8.4 UltraSPARC T2以太网编码器 | 第121-122页 |
| 6.8.5 针对不具备流控机制的编码器比较我们的算法和Liu etal.[165]算法 | 第122-123页 |
| 6.8.6 在我们的算法和手工书写的解码器之间比较电路面积和延迟 | 第123-124页 |
| 6.9 结论 | 第124-125页 |
| 第七章 结束语 | 第125-127页 |
| 7.1 工作总结 | 第125-126页 |
| 7.2 研究展望 | 第126-127页 |
| 致谢 | 第127-129页 |
| 参考文献 | 第129-151页 |
| 作者在学期间取得的学术成果 | 第151-152页 |
