基于门级信息流分析的集成电路设计安全漏洞检测技术研究

集成电路设计中的缺陷,如设计错误、脆弱点以及第三方嵌入的恶意代码，通常会引发难以检测的安全漏洞，成为攻击者入侵系统的切入点。项目从信息流安全的角度研究硬件安全漏洞检测问题，利用门级抽象层次上所有逻辑信息流均以二进制位为粒度显式流动的特点，捕捉电路中全部逻辑信息流，包括显式流、隐式流以及硬件相关隐通道所引发的敏感信息泄露；通过逆向追踪有害信息流的传播路径，检测电路设计中隐含的安全漏洞。项目研究门级电路抽象层次上的细粒度信息流分析方法，能够实现对硬件中全部逻辑信息流的精确度量；构建集成电路在多级安全格下的信息流模型，以满足多级安全验证需求；研究信息流传播的反问题，提出门级信息流逆向追踪方法，通过有害信息流传播路径逆向分析，检测电路设计中潜在的安全缺陷，研究工作为集成电路设计的安全漏洞检测与验证提供基础理论与方法。

Security vulnerabilities such as integrated circuit design faults, flaws and malicious code injected by third party residing in hardware design are known to expose hard-to-detect security holes, which enable attackers to get a foothold into the system to perform malicious activities. This research project addresses the integrated circuit security hole detection problem from the perspective of information flow security. We take advantage of the property that logical information flows all flow explicitly in the granularity of binary bits at the abstraction level of Boolean gates, and thus can capture all logical information flows in the hardware, including explicit flows, implicit flows as well as sensitive information leakage resulting from hardware-specific covert channels. Further, security holes can be identified through back-tracking along the propagation path of harmful information flows. This research project aims to formalize fine granularity information flow analysis method at the level of Boolean gates to precisely measure all logical flows of information in the underlying hardware. It constructs information flow models for digital circuits under multi-level security lattices in order to prove multi-level security (MLS). It also studies the inverse problem of information flow propagation to propose back-tracking algorithms that can identify potential security vulnerabilities by tracking backwards along the propagation path of harmful information flows. Our research work can provide support for design and verification of secure circuit involved in high-assurance and safety-critical systems. Research work can provide theory and methodology for secure integrated circuit design and verification.