基于细粒度信息流分析的高可靠系统安全验证方法研究

Designing high-assurance systems is a costly endeavor.The main difficulty lies in formal verification of critical security properties.However, existing language, process algebra and network based methods target too high a level of abstraction to detect hardware-specific timing channels or to capture underministic system behaviors caused by hardware-software interference. This project addresses the high-assurance system security verification problem from the perspective of information flow security.It aims to formally verify security properties through the construction of precise mathematic information flow model for the underlying hardware. To ahieve such a goal, this project studies circuit level fine granularity information flow analysis method. It uses mathematic approaches to formulate information flow model for the underlying hardware to capture all digital information flows, especially harmful flows of information resulting from hardware-specific timing channels. Further, this project studies information security property mapping and verification methods. Critical security properties are formally verified with support of information flow measurement capability from the underlying hardware under specific information flow security policies; potential security vulnerabilities, including hardware-specific timing channels, can be identified by capturing illegal flows of information among security domains at the early system design phase. In addition, our method can provide information flow measurement capability to higher abstraction levels and support for hardware and software security verification in the high-assurance system development process.

高可靠系统设计是一个代价极高的过程。其主要难点在于安全属性的形式化验证。然而，现有的基于语言、过程代数和网络的安全验证方法大多针对较高的抽象层次，无法检测到硬件中的时间隐通道，也无法捕捉由软硬件交互所引发的不确定性系统行为。本项目从信息流安全角度研究高可靠系统的安全验证问题，通过构建底层硬件精确的信息流数学模型来对系统的安全属性进行验证。项目研究电路层面上的细粒度信息流分析方法，采用数学手段为底层硬件构建精确的信息流模型，从硬件电路抽象层次捕捉硬件中全部的逻辑信息流，尤其是硬件相关时间隐通道所引发的有害信息流；研究上层安全属性的映射及验证方法，在给定的信息流安全策略下基于底层硬件的信息流度量能力实现系统关键安全属性的形式化验证，通过捕捉安全域之间的有害信息流动在设计阶段即检测系统中潜在的安全漏洞,包扩硬件相关的时间隐通道，并可向上层提供信息流度量能力，为高可靠系统软硬件安全验证提供支撑。

高可靠系统设计是一个代价极高的过程。其主要难点在于安全属性的测试与验证。本项目从信息流安全角度研究高可靠系统的安全验证问题，通过构建底层硬件精确的信息流数学模型来实现系统的安全属性进行度量和验证。. 项目研究了门级抽象层次上的细粒度信息流分析方法，构建了基本逻辑门在任意安全格下的细粒度信息流模型，提出了复杂硬件电路精确细粒度信息流模型的生成算法，并采用布尔逻辑函数对基本逻辑门和复杂硬件电路的细粒度信息流模型进行了形式化描述，为硬件设计安全性度量及验证提供了一种形式化模型。项目进一步研究了门级细粒度信息流分析方法的复杂度与精确性理论，从静态逻辑冒险和扇出重汇聚等角度对信息流模型的不精确性进行了研究，提出了多种消除硬件细粒度信息流模型中误报项的算法，给出了在门级细粒度信息流分析精确性与复杂度之间平衡的有效方法。项目以IWLS集成电路测试基准为研究对象，对多级安全格下的门级细粒度信息流模型的复杂度进行了评估，并对精确性与复杂度平衡算法的有效性进行了验证。. 项目研究了硬件电路需要满足的关键安全属性，包括保密性、完整性、隔离特性、时间信道、硬件木马等，提出了一种语言对上述安全属性进行描述，并进一步设计了一个安全属性编译器将其映射至底层硬件的信息流安全模型，从而实现安全属性形式化验证的方法。项目进而采用细粒度信息流安全验证手段，研究并提出了硬件设计中设计漏洞、时间信道以及硬件木马的检测方法。项目以采用不同高层综合优化策略和时间迁移算法所产生的RSA密码算法核为研究对象，给出了基于定性和定量信息流分析的时间信道的检测和度量方法；项目以Trust-HUB硬件木马测试基准为研究对象，给出了基于门级信息流安全验证的硬件木马检测方法，以及基于信息流逆向追踪的木马设计定位方法。. 项目的研究工作可实现高可靠系统硬件安全漏洞的检测，并可向上层应用提供安全属性的度量与验证手段，为高可靠系统软硬件安全验证提供支撑。