基于进程的无干扰可信模型

提出了一种适应于可信计算平台系统设计的抽象模型,该模型借鉴信息流的基本无干扰理论,利用进程代数和逻辑推理方法,将系统抽象为进程、动作、状态和输出,形式化地定义了进程运行可信,给出进程运行可信的条件和性质,推出进程运行可信隔离定理,在进程运行可信基础上给出系统运行可信的定义,并证明了系统运行可信判定定理。该模型建立在逻辑推理基础上,不依赖于特定的安全机制和实现方法,任何一种符合这个模型的实现方法,都可以达到系统运行可信的目标。

基于可信进程的文档加解密系统

为实现适用于所有应用程序所产生数据文件的加解密方案,提出基于可信进程读写的文档加解密系统。将文件加密属性以一定长度的信息块写入文件尾部,构成文件的加解密识别标志。采用固定算法的安全套接层通信机制,确保在客户/服务器模式下可信通道建立时的高效性和数据传递的安全性。

基于高效可信进程认证的文档加解密系统

为提高目前文档加解密系统可信进程的认证效率,解决文档易损毁的缺陷,提出基于高效可信进程认证的文档加解密系统。利用进程映像文件的哈希值与进程PID的唯一性,构成可信进程认证方案的基本要素,同时将文件加密属性标识存放于文件头部,以降低文档损毁风险。实验结果表明该方案中可信进程认证效率明显提高,文档损毁风险大幅降低。

基于无干扰理论的信任链传递模型

针对现有的信任链传递模型可用性不强、缺乏将信任链扩展到网络环境的缺点,提出了一种新的基于无干扰理论的信任链传递模型。该模型将系统抽象为进程、动作和执行,从可信根出发,通过度量程序及其动态库完整性来保证进程静态可信;分析交互进程之间的关系,利用无干扰理论判定其合法性;通过对接入终端的可信度量,将信任链扩展到整个网络系统。最后给出了相应的形式化定义及安全性证明。

基于可变标签的访问控制策略设计与实现

仅提供了自主访问控制级安全防护能力的Windows操作系统的安全性受到用户广泛关注,而作为一项重要的信息安全技术,强制访问控制能够有效实现操作系统安全加固。访问控制策略的选择与设计是成功实施强制访问控制的关键。针对安全项目的需要,分析了结合经典访问控制模型BLP与Biba的优势,提出了依据进程可信度动态调整的可变标签访问控制策略,解决了因BLP与Biba模型的简单叠加而导致的系统可用性问题,最终实现了对进程访问行为进行控制的简单原型系统。实验表明,可变标签访问控制策略的引入在对操作系统安全加固的基础上显著提高了系统的可用性。

Isabelle在分析安全操作系统状态机模型中的应用

为了解决已有的状态机模型的形式化框架在分析安全操作系统状态机模型时不够直观、简洁的问题,提出了一套使用Isabelle工具对安全操作系统模型状态中的类型、变量、常量、关系、映射、函数,以及模型中的安全不变量和状态迁移规则进行形式化描述的新方法。通过实际验证一种典型的安全操作系统状态机模型——可信进程模型,总结出了有效地使用Isabelle辅助形式化设计、分析、验证模型的策略。

基于微过滤驱动的安全软件文件保护

针对安全软件忽视自身文件安全、容易被恶意软件破坏的问题,提出了基于MiniFilter的安全软件文件保护的方法。首先利用攻击树原理建立恶意软件操作安全软件文件的评估模型,提出应对策略,然后通过微软最新文件过滤驱动框架MiniFilter实现。其中,安全软件的文件操作权限采用策略库和可信进程验证。