关键词:
硬件设计
信息流跟踪
安全漏洞
时间侧信道
硬件木马
摘要:
长期以来硬件作为计算机系统的信任根备受信任且被视为安全可靠的。但是,近年来不断涌现的硬件安全问题却揭示出硬件系统中存在众多安全漏洞。若攻击者利用这些安全漏洞攻击计算机系统时,可能会造成关键信息的泄露、篡改、系统功能的丧失甚至损毁等。目前,硬件设计验证技术多针对设计功能正确性检查,由于缺乏相应安全模型,难以检测违反安全策略的安全漏洞。因而,亟待研究能够在硬件设计早期验证可建模设计安全行为与分析设计安全性检测安全漏洞的方法和技术。本文在信息流理论框架下采用信息流跟踪技术研究高抽象层次硬件设计的安全模型和检测安全漏洞的方法。主要内容如下:
(1)在门级抽象层次研究硬件设计的安全模型,构建可捕捉有害信息流的硬件设计安全模型和检测设计安全漏洞的形式化验证方法。本文在门级抽象层次提出了混合属性概念,结合信息流跟踪技术从信息流安全角度对设计安全行为进行建模,构建门级设计的混合属性安全模型。该模型为门级设计网表的每个逻辑单元分配包含安全属性和时域属性的混合属性标签,并依照一定的标签传播策略由设计输入向输出传播混合属性标签并计算输出的混合属性标签。通过跟踪混合属性标签的传播,该模型能够有效捕捉由设计安全漏洞所引发有害时间信息流、显式流、隐式流。此外,基于门级抽象层次的混合安全属性模型,本文提出了通过验证系统执行时间不变性属性和安全属性检测硬件安全漏洞,能够解决基于门级信息流安全模型的安全验证方法无法有效甄别时间侧信道安全漏洞与其它安全漏洞的短板。实验结果表明,该方法能够在设计早期有效的检测和甄别设计内潜藏的硬件时间侧信道安全漏洞。
(2)在寄存器抽象层次研究硬件设计的安全模型,构建可捕捉有害信息流的硬件设计安全模型和检测设计安全漏洞的形式化验证方法。本文在二级安全理论下,以信息流分析方法为基础研究寄存器传输级设计安全模型的精确标签传播规则,构建了寄存器传输级设计复杂操作语句的安全标签跟踪逻辑。该逻辑可附加在原始设计中,在不改变设计功能的情况下,精确捕捉设计内全部的隐式流和显式流,建模设计的安全行为。在此基础上,本文进一步提出了大规模寄存器传输级设计安全标签跟踪逻辑模型的建模方法。该方法能够解析寄存器传输级设计的抽象语法树,并从数据流和控制流角度按照精确标签传播规则对设计语句插入相应的安全标签跟踪逻辑,自动化地生成设计的寄存器传输级设计安全标签跟踪逻辑模型。此外,本文基于寄存器传输级设计安全标签跟踪逻辑模型,提出了通过安全属性检测安全漏洞的形式化验证方法。该方法利用寄存器传输级设计安全标签跟踪逻辑模型的安全行为描述能力,结合基于断言的安全属性验证方法,利用EDA测试验证工具,验证设计中是否存在违反信息流安全策略的情况,检测设计内潜藏的安全漏洞。实验结果表明,该方法能够在设计早期有效检测和甄别设计内潜藏的硬件安全漏洞。