如何在Dafny中实现常量时间与运算以防范侧信道攻击？

要避免短路求值引发的分支差异，核心是确保两个条件都会被完整求值后再进行合取判断。可以通过先将两个条件的结果存储到独立布尔变量中，再判断它们的逻辑与——这种方式会强制Dafny计算两个变量的值，不会触发短路行为。

修改后的代码如下：

method IndexOf( s: seq<int>, value: int) returns (index: int)
    // Answers the index of value in s:
    requires value in s
    ensures 0 <= index < |s|
    ensures s[index] == value
    ensures value !in s[0..index]
{
    ghost var numIterations := 0;
    ghost var numFirstBranch := 0;

    var result := -1;
    for i := 0 to |s|
        invariant result == -1 ==> value !in s[0..i]
        invariant result < |s|
        invariant result >= 0 ==> value !in s[0..result]
        invariant result >= 0 ==> s[result] == value
        invariant numIterations == i
        invariant result != -1 ==> numFirstBranch==1
        invariant result == -1 ==> numFirstBranch==0
        { 
            numIterations := numIterations + 1;
            // 先分别计算两个条件，确保均被求值
            var matchesValue := s[i] == value;
            var stillSearching := result == -1;
            if matchesValue && stillSearching 
            { 
                numFirstBranch := numFirstBranch + 1;
                result := i;
            }
        }
    assert numIterations == |s|;
    assert numFirstBranch == 1;
    return result;
}

关键说明： #

• 通过matchesValue和stillSearching两个变量分别存储两个条件的结果，Dafny会在进入if判断前完整计算这两个变量的值，不会因第一个条件为假就跳过第二个条件的求值。
• 这种写法保证了循环每一次迭代的执行路径固定：无论s[i]是否匹配目标值、result是否已找到结果，两个条件都会被执行，消除了短路带来的侧信道泄露风险。
• 原有的循环不变量和断言依然有效，因为变量存储的是原条件的等价结果，逻辑上与原代码完全一致，但执行时序的稳定性更强。

内容的提问来源于stack exchange，提问作者CharlesW