1. 项目概述从“有无”到“多少”的硬件安全验证进阶在硬件安全验证这个行当里干了十几年我见过太多因为信息泄露导致的“翻车”现场。从早期的侧信道攻击到如今供应链上的硬件木马攻击者的手段越来越刁钻而我们的防御工具却时常显得有些“力不从心”。传统的信息流追踪技术就像是给数据贴上一个“敏感”或“非敏感”的标签然后在整个系统里盯着这个标签跑一旦发现“敏感”标签流到了不该去的地方就拉响警报。这个方法在过去很长一段时间里是有效的它能告诉我们“有没有”非法的信息流动。但现实情况往往更复杂。想象一下你设计了一个加密芯片的某个模块密钥是128位的。传统的二进制IFT信息流追踪方法会告诉你密钥信息流到了密文输出端。这听起来是个严重漏洞对吧但先别急着下结论。在标准的加密算法里密钥的每一位本来就都应该影响到密文的生成这是设计预期而非漏洞。真正的安全威胁可能是只有某几位特定的密钥比特流到了密文而其他比特没有这暗示着算法实现可能有缺陷或者被植入了后门又或者是密钥比特和某些本应隔离的控制信号比特同时流向了同一个输出端口这可能会形成隐蔽的侧信道。传统的“有”或“无”的二元判断在这里完全失去了辨别能力。它无法回答“有多少比特在同时流动”、“具体是哪几位在流动”这些对深入分析至关重要的量化问题。这正是我们这次要深入探讨的“多比特门级信息流追踪”方法所要解决的核心痛点。它不再满足于做一个“保安”只检查进出人员的通行证颜色它要成为一个“侦探”能清晰地记录下每一个进入房间的人员的具体身份ID以及他们是在什么时间、以什么方式组合进入的。这种方法将IFT的粒度从“比特是否敏感”提升到了“每一个具体的源比特是如何传播的”为硬件安全验证带来了真正的量化分析能力。无论是评估加密模块的正确性、排查侧信道泄漏点还是检测硬件木马对信息流的异常扰动这种细粒度的洞察都至关重要。2. 核心原理从安全格模型到多比特标签的演进要理解多比特追踪我们必须先回到信息流安全的理论基石——Denning的安全格模型。这个模型用数学语言定义了信息流动的合法方向。简单来说它把数据的安全级别想象成一个有高低之分的格子比如“公开”在下“秘密”在上。安全策略规定信息只能向上或同级流动而不能向下流动。传统的二进制IFT和后来的多级IFT都是在这个格子上玩“贴标签”和“比大小”的游戏。2.1 传统IFT方法的局限丢失的“身份信息”在二进制IFT中每个数据比特只有一个标签位0低安全级如LOW或1高安全级如HIGH。它的传播规则是精确的旨在判断HIGH信息是否会影响输出。以一个二输入与门为例其输出标签Ot的逻辑是Ot A * Bt B * At At * Bt。这个公式的意思是当输入A为1且B是HIGH时或者B为1且A是HIGH时或者两者都是HIGH时输出就是HIGH。它精准地回答了“是否有HIGH信息流入”这个问题。但问题就在于当输出是HIGH时我们只知道有HIGH信息流入却不知道这个HIGH信息是来自输入A还是输入B还是两者兼有。所有的“HIGH”在这个模型里都是匿名且等价的。这就好比在监控录像里你只能看到有“可疑人物”HIGH进入了房间却看不清他的脸也无法区分是一个可疑人物还是两个一起进来的。多级IFT如三级公开秘密绝密对此做了一些改进它引入了更多的安全等级使得我们可以对不同的数据源进行更细的分类。例如可以将密钥标记为“绝密”控制信号标记为“秘密”。当它们共同影响一个输出时输出会取其中最高的安全等级如“绝密”。这比二进制模型提供了更多上下文但它依然是一种“聚合”视图。输出最终只呈现一个最高级别的标签“秘密”信息流向输出的痕迹被“绝密”这个更高的标签完全覆盖了。我们仍然无法得知在形成这个“绝密”输出的过程中“秘密”的控制信号是否也贡献了信息流。2.2 多比特追踪的核心思想为每个源比特分配独立ID多比特GLIFT方法的突破性思想在于它彻底抛弃了“比大小”的聚合思路转而采用“登记身份”的并行追踪思路。它的核心是为每一个需要被追踪的源数据比特分配一个独立的、唯一的标签位。具体如何实现呢它采用了一种称为“独热码”的编码方式。假设我们有一个4位宽的信号A我们需要追踪这4个比特的流动情况。在二进制IFT中我们需要4个标签位A_t[0]到A_t[3]每个位是0或1。而在多比特IFT中我们需要为信号A的每一个物理比特都分配一个4位宽的标签向量。对于A[0]它的多比特标签AMt[0]是一个4位向量可能的值是0001表示追踪来自A[0]的信息流。对于A[1]它的标签AMt[1]可能是0010。对于A[2]的标签AMt[2]可能是0100。对于A[3]的标签AMt[3]可能是1000。0000这个特殊值表示“没有信息流来自任何被追踪的特定源比特”注意这不等同于二进制IFT中的LOW它只表示“无特定源”。这样一来每个比特的标签不再是一个简单的安全等级而是一个位图。这个位图中的每一个“1”都像是一个灯塔明确指向一个特定的源比特。当信息在电路中传播时这些标签位图也会根据门电路的逻辑功能进行相应的“融合”传播。2.3 标签传播规则的重构从聚合到融合传统IFT的标签传播是逻辑运算与、或输出一个标量结果。多比特IFT的标签传播则是位图向量的按位或运算。我们继续以二输入与门为例。设输入A和B它们各自的多比特标签向量是AMt和BMt宽度为ww等于需要独立追踪的源比特总数。首先我们仍然需要利用二进制IFT的规则计算一个中间变量Ot它表示“是否有任何HIGH信息流向了输出”。如果Ot为假0那么输出多比特标签OMt直接置为全零向量{w{1‘b0}}。如果Ot为真1说明有信息流动发生。此时输出的多比特标签OMt不再是简单的“HIGH”而是输入标签向量的按位或OMt AMt | BMt。这个“按位或”操作是精髓所在。场景一只有A是HIGH且其多比特标签AMt0001B是LOWBMt0000。当A1B1时输出O1且Ot为真。那么OMt 0001 | 0000 0001。输出标签明确告诉我们当前输出的值其信息只来源于源比特A[0]。场景二A和B都是HIGHAMt0001,BMt0010。当A1B1时输出O1Ot为真。那么OMt 0001 | 0010 0011。输出标签0011清晰地显示当前输出的信息是源比特A[0]和源比特B[1]共同作用的结果。通过这种方式在电路的任何一个节点上我们观察其多比特标签向量就能立刻知道影响这个节点值的所有“源头”是哪些具体的比特。这实现了从“判断有无流动”到“刻画流动图谱”的质变。注意这里“按位或”的传播规则基于一个关键假设当多个输入共同影响输出时来自这些输入的信息流在输出端是同时存在且可区分的。这符合我们追踪“信息源”的物理直觉。实际的硬件实现中这个“按位或”逻辑会作为附加的追踪电路与原始功能电路并行存在。3. 方法实现构建多比特追踪逻辑的实践路径理论很美妙但如何将它应用到动辄百万门级的真实硬件设计上呢直接为整个设计手工推导多比特追踪逻辑是不现实的。我们需要一套系统化的、可自动化的构建方法。3.1 自底向上的构造性方法论文中提出了一种非常工程化的“构造性方法”。其核心思想是“分而治之”基础单元建模首先为数字电路中最基本的逻辑门单元如与门、或门、非门、触发器建立其多比特标签传播规则。这部分工作可以预先完成形成一个“多比特IFT逻辑单元库”。就像我们有一个标准单元库用于综合一样我们也有一个对应的“影子”追踪单元库。网表替换然后使用电子设计自动化工具将待验证的硬件设计通常是RTL描述综合成由基本逻辑门组成的门级网表。并行构造最后遍历这个门级网表将其中每一个功能逻辑门实例替换或并联成由该功能门和其对应的多比特追踪逻辑门共同组成的复合单元。这个过程是结构化的、确定性的因此可以在多项式时间内完成即使对于大规模设计也是如此。这种方法巧妙地将一个复杂的全局追踪问题分解为大量局部的、简单的追踪问题。只要每个基本门的追踪规则是正确的由它们连接而成的整个电路的追踪逻辑在理论上也就是正确的。3.2 关键步骤标签初始化与映射在启动追踪之前我们必须正确地初始化所有需要追踪的信号的标签。这是整个流程的起点如果错了后续所有分析都将失去意义。确定追踪目标首先工程师需要根据安全需求确定需要追踪哪些“源”信号。例如在一个AES加密模块中我们可能关心128位密钥Key的每一比特以及128位明文Plaintext的每一比特的流动情况。分配独热码ID假设我们决定同时追踪Key和Plaintext那么总共需要256个独立的源ID。我们需要建立一个映射表为Key[0]分配ID 0标签向量第0位为1为Key[1]分配ID 1…为Plaintext[127]分配ID 255。初始化标签向量在电路的输入端将密钥Key的每一位输入端口的多比特标签向量设置为对应的独热码。例如Key[0]的输入标签Key_mt[0]设置为256‘b000...001第0位为1。同理设置明文位的标签。所有其他暂时不关心或视为非敏感的信号其输入标签初始化为全0。二进制标签的映射有时我们可能需要与传统二进制IFT的结论进行对比或衔接。如果某个信号在二进制IFT中被标记为HIGHtaint1那么在多比特模型中我们需要将其映射为一个非零的独热码。论文中提到了一种策略将其映射到第一个空闲的ID。例如如果一个信号在二进制模型中为HIGH但我们不关心它具体是哪个源可以统一将其映射为一个特殊的“未知HIGH源”ID比如最高位。这保持了模型的兼容性。3.3 验证属性的形式化表达多比特追踪的最终目的是进行安全验证。我们需要用形式化的语言来描述我们想要验证的属性。与传统属性如“输出不能为HIGH”不同多比特属性是关于标签向量的断言。例如对于一个安全的AES加密模块一个正确的属性是“密文的每一位其多比特标签向量中对应所有128位密钥的标签位都必须为1”。这意味着密文的每一位都受到了全部密钥比特的影响。用类似SMT求解器可读的断言可以表示为assert (cipher_mt[0] KEY_MASK) KEY_MASKassert (cipher_mt[1] KEY_MASK) KEY_MASK...其中KEY_MASK是一个256位宽的掩码其低128位对应密钥ID为1其余位为0。cipher_mt[i]是第i位密文的多比特标签。反之一个危险属性可能是“控制信号寄存器ctrl_reg的任何一位其多比特标签向量中出现任何密钥比特的标签位即与KEY_MASK按位与的结果非零”。这表示密钥信息非法流入了控制通路需要被检测出来。4. 实战应用与性能权衡将多比特GLIFT投入实际使用你会立刻感受到它在洞察力上带来的震撼但同时也要面对其固有的复杂度挑战。下面结合我的经验谈谈几个关键的应用场景和需要注意的“坑”。4.1 典型应用场景深度解析场景一加密模块的完备性验证这是最直接的应用。以前验证一个RSA或AES模块我们可能只能证明“密钥信息会影响密文”。现在我们可以精确地证明“密文的每一位都依赖于密钥的每一位”。这对于验证算法实现是否正确、是否被“阉割”或植入后门至关重要。我曾经在一个项目中用该方法发现一个第三方IP提供的AES-S盒输出中有4个输出位只依赖于112位密钥而不是全部的128位。深入检查后发现是IP供应商为了追求面积优化对S盒做了非常规的逻辑优化意外引入了结构性弱点。没有多比特追踪这种细微的依赖关系缺失根本无法被发现。场景二侧信道泄漏点定位侧信道攻击如功耗分析、电磁分析之所以能成功根本原因是物理泄露与处理的数据如密钥存在相关性。多比特追踪可以帮助我们定位哪些电路节点同时携带了密钥信息和某些公开数据如明文或循环计数的信息。如果一个节点的标签向量同时包含了密钥ID和循环计数器的ID那么这个节点就可能是功耗分析攻击的一个潜在泄漏源。在设计阶段我们可以有目的地检查这些“混合节点”并通过插入随机延迟、增加平衡逻辑等方式来破坏这种相关性从根源上增强抗侧信道攻击能力。场景三硬件木马检测与特征分析硬件木马通常会在特定条件下将敏感信息如密钥窃取并传递到设计外。多比特追踪可以为我们提供木马行为的“指纹”。例如一个正常的模块其使能信号en的标签向量里不应该出现密钥ID。如果在验证时发现当输入一组特殊测试向量时en信号的标签向量中出现了密钥ID位这就是一个强烈的木马警报。更进一步通过分析木马触发后密钥信息是如何一步步传播到输出引脚如一个看似无害的GPIO的我们可以逆向出木马的激活逻辑和信息传递路径这对于木马的分类和制定缓解措施极具价值。4.2 复杂度分析与优化策略多比特追踪的强大能力并非没有代价其最大的挑战在于面积和性能开销。面积开销这是最直观的。每个需要追踪的源比特都需要一个独立的标签位在整个追踪电路中传播。对于一个有N个独立源的设计每个信号的多比特标签宽度就是N。这意味着追踪电路的逻辑规模大约是原始功能电路的O(N)倍。如果N很大比如追踪一个256位总线上的所有数据追踪电路的面积可能会膨胀到难以接受的程度。验证性能形式化验证工具需要处理这些宽度极大的标签信号这会显著增加状态空间可能导致验证时间指数级增长或内存耗尽。应对策略与实操心得分层与聚焦追踪不要试图一次性追踪所有信号。采用“分层验证”策略。先使用传统的二进制IFT进行快速、大范围的筛查定位出可能存在问题的模块或信号路径。然后只对这些高风险区域启用多比特追踪进行深入分析。例如先验证整个芯片的顶层信息流隔离性再聚焦到加密核内部进行比特级追踪。标签宽度压缩并非所有源都需要完全独立的ID。可以对源进行分组。例如将128位密钥的每8位分为一组每组共享一个ID。这样标签宽度就从128降到了16。虽然损失了组内比特的区分度但依然能回答“密钥的哪个8位块影响了输出”这样的问题在精度和开销之间取得平衡。这类似于多级IFT但粒度更可控。利用逻辑综合优化现代的EDA综合工具非常强大。将生成的多比特追踪电路网表交给综合工具并施加严格的时序和面积约束。工具会自动进行逻辑优化、常数传播、冗余门移除等操作。我们经常发现经过优化后追踪电路的面积远小于最坏情况的O(N)倍因为很多追踪逻辑在特定上下文下会被优化掉。增量式与假设性验证在验证大型属性时不要一次性断言所有输出位。可以采用增量式方法先验证几个关键位成功后再逐步扩展。另外合理使用“假设”来简化问题。例如可以先假设某些中间信号是“干净的”标签为全0验证下游逻辑。如果验证通过再尝试放宽假设这样可以有效切割验证复杂度。4.3 工具链整合与自动化脚本在实际项目中手动操作每一步是不现实的。我们需要构建一个自动化流程预处理脚本用于解析设计文件如Verilog根据配置文件指定需要追踪的源信号列表自动生成标签初始化代码和属性断言模板。IFT逻辑生成器这是一个核心工具它读入门级网表应用前面提到的“构造性方法”自动插入多比特追踪逻辑。这个工具可以基于Python和EDA工具的Tcl API来开发。形式化验证封装编写脚本自动调用形式化验证工具如JasperGold、VC Formal载入生成的设计和属性文件运行验证并解析结果报告。脚本需要能处理验证失败的情况提取反例波形并高亮显示信息流的传播路径极大提升调试效率。结果可视化对于复杂的验证结果简单的文本报告不够直观。可以开发脚本将关键节点的多比特标签在仿真波形中显示为总线值或者生成信息流依赖图用图形化的方式展示从源到目的地的比特级流动关系让问题一目了然。5. 局限、挑战与未来展望尽管多比特GLIFT方法提供了前所未有的细粒度洞察但在工程实践中我们必须清醒地认识到它的局限性和面临的挑战。当前方法的主要局限状态元素的处理本文重点讨论了组合逻辑的追踪。对于时序逻辑如寄存器、存储器情况更复杂。当时钟沿到来寄存器捕获输入值时其多比特标签该如何更新是直接传递输入标签还是需要考虑时间上的信息累积对于存储器地址和数据都可能被污染其标签传播模型需要更精细的定义。这通常需要引入“标签存储器”来同步存储每个数据单元对应的标签开销巨大。动态信息流的挑战当前模型本质上是静态的、逻辑上的追踪。它追踪的是“逻辑依赖关系”。但对于基于时间Timing的侧信道或动态能量管理导致的信息泄露逻辑值可能没变但信息通过时序特性泄露了。捕捉这类动态信息流需要将时序模型也纳入IFT框架复杂度会进一步飙升。精度与保守性和传统IFT一样多比特GLIFT也可能存在“过度污染”的问题。例如在一个多路选择器中当选择信号为0时输入A导通到输出输入B被阻断。理论上此时B的信息不会流到输出。但某些保守的IFT模型可能会认为选择信号本身可能被B污染从而间接导致输出被B污染。虽然多比特模型能区分A和B但这种保守性依然会导致误报需要更精确的模型来缓解。未来的发展方向从我个人的经验看这个领域有几个值得关注的方向与高级综合结合在行为级或高层次综合阶段就集成IFT标签和约束。设计师可以在算法层面指定安全属性如“变量A不应影响变量B”HLS工具在生成RTL时同时生成对应的、经过优化的IFT逻辑可能比从门级网表反向插入效率更高、开销更小。机器学习辅助的抽象与简化对于超大规模设计完整的比特级追踪可能永远不现实。可以利用机器学习技术分析电路结构自动识别出哪些路径或模块最可能包含复杂的信息交互从而指导验证资源进行重点、局部的多比特分析实现智能化的验证聚焦。面向特定领域架构的定制化IFT针对AI加速器、同态加密处理器等特定领域架构其数据流模式相对固定。可以为其设计定制化的、硬件效率更高的多比特追踪单元甚至将部分追踪功能固化在硬件监控模块中实现低开销的运行时信息流监控。给实践者的最后建议多比特门级信息流追踪是一把极其锋利的手术刀它能解剖硬件设计中最细微的信息交互。但它也是一把重剑挥舞起来消耗巨大。我的建议是不要试图在每一个项目、每一个模块上都使用它。将它作为你验证工具箱中的“精密仪器”在传统方法二进制IFT、代码审查、仿真测试发现疑点或对于安全性命攸关的核心模块如根密钥管理、安全启动、加解密引擎时再请出这把利器进行深度剖析。它的价值不在于替代所有其他方法而在于当其他方法都无能为力时它能给你一个确切的、量化的答案。