常数时间的泄漏轨迹模型

形式陈述

密码学中的constant-time不是算法复杂度 $O(1)$ 。先固定执行模型，将输入分为公开量l与秘密量h，程序返回允许公开的结果 $O(l,h)$ ，并产生攻击者可观察的泄漏轨迹 $L(l,h)$ 。轨迹可包括分支方向、访存地址以及某些变时指令的操作数；选哪些观察，决定要抵御哪类攻击。

对确定性、在规定输入上总终止的程序， $O$ 与 $L$ 都是规定输入上的函数。先采用固定公开输入下的秘密无关泄漏合同：

\forall l,h_1,h_2,\quad L(l,h_1)=L(l,h_2).

它允许程序计算依赖秘密的结果，却不允许所选执行观察随秘密改变。实现固定长度密钥比较时可用这种纪律。若应用另有明确的输出去密政策，还可以考察较弱的合同：

\forall l,h_1,h_2,\quad O(l,h_1)=O(l,h_2)\Longrightarrow L(l,h_1)=L(l,h_2).

后一个合同只要求泄漏不区分本来具有相同公开结果的秘密。若允许输出释放信息，必须先声明输出等价类所代表的去密政策，不能为了让证明通过把所有秘密都列成公开输出。

这条按输出等价类比较的合同较弱，不能直接推出计算保密。设公开输出 $O(h)=f(h)$ 是一个单射单向映射，则 $O(h_1)=O(h_2)$ 已迫使 $h_1=h_2$ ，即便额外泄漏取 $L(h)=h$ ，该合同也会真空式地通过；但攻击者本来难以反演f，看到L后立即得到秘密。故不能因为密文或摘要要发送，就把完整输出当成允许释放它背后全部信息的依据。密码程序通常还需固定公开输入下的秘密无关泄漏纪律，或具有明确计算安全语义的去密证明。下面相等比较器只允许公开一个相等/不等结果，不把散列值或密文的计算隐藏性偷换为信息论公开。

这里比较两次执行，是超性质的具体实现安全应用。功能正确性只说输出值算对了，不能推出两条泄漏轨迹相等；密码原语的黑盒游戏通常也没有自动提供这些内部观察。

直觉

如果比较器在遇到第一个不同字节时立即返回，攻击者虽然总看到“错误”，却可能从耗时估出已经匹配了多少字节。两次运行的业务结果相同，执行路径却透露了更细的信息。

把返回延迟加一个随机睡眠不等于建立轨迹独立性；重复测量可能平均掉噪声。无秘密分支也不是充分条件：用秘密作查表索引会让内存地址泄漏，缓存观察者可能分辨它。

例子与边界

公开候选固定为两个字节 00 00，秘密分别是 01 00 与 00 01。提前返回比较器都输出false，前者只访问第0位，后者访问第0、1位。两条泄漏轨迹分别含一轮和两轮比较，因此违反上述合同。攻击者不必已经知道秘密，只需利用这种可区别性构造猜测。

一种抽象修复在公开长度n上执行全部n轮：累积 diff |= secret[i] XOR candidate[i]，最后输出 diff == 0。在规定的固定宽度字操作模型中，循环分支只依赖公开i、n，地址只依赖i，且异或/或的耗时不依赖值，于是任意两次相同n的运行产生同样的地址和控制轨迹。归纳证明每轮访问同一i并执行同一指令序列；这仍是模型级证明。

若底层把大整数运算实现为按数值长度变化的过程，或者编译器将累积式重新优化为早退，上述假设可能失效。Python代码看起来没有条件分支，也不能据此认证机器级constant-time。处理长度不同的输入也要先说明长度是否允许公开；不能把需要隐藏的长度直接放进循环界。

同样，无分支的 table[secret_byte] 在地址观察模型中明显不安全。若模型还包括推测执行、功耗或电磁泄漏，只有分支与地址相同也可能不足；证明的范围必须随硬件与攻击观察扩展。

推论与应用

验证常数时间需要同时列出公开/秘密分类、泄漏函数、终止假设、编译阶段与目标机器。乘积程序或自组合把两次执行放到一个检查任务中，要求对应观察相同；ct-verif原论文对输出不敏感乘积给出定理与Coq形式化，对输出敏感乘积另外给出Theorem 2，并在优化后的LLVM层验证实例，其保证仍依赖该层泄漏模型能覆盖目标机器相关行为。

时间统计测试适合发现差异，未检出不能证明全输入轨迹独立。源码审计、编译后检查、形式证明和目标平台测量可以提供不同证据，不能互相冒称。本单元检查器调用可信密码库并使用专门比较接口，但没有进行ct-verif、汇编验证或真实侧信道测量，因此不把测试通过标作constant-time认证。

参考资料

José Bacelar Almeida等，Verifying Constant-Time Implementations，USENIX Security 2016，§2：控制/地址/操作数观察；§3及Definition 1：公开输入输出与泄漏；§4：乘积程序；§5：LLVM实现与边界
该论文官方出版页提供作者、出版信息及全文，pp.53–70

形式陈述 ​

反向链接

形式陈述