通过静态分析检测缺少 if/else 语句

Question

我试图捕获 if 语句中缺少的未处理的 expressiong 条件。

第一个示例

if (a < 5) {
    // Do something
} else {
    // handled else condition
}

第二个示例

if (a < 5) {
    // Do something
} else if (a >= 5){
    // handled else if condition
}

这两个示例是正确的，并且处理了所有可能性。

但我正在尝试解决类似的条件

if ((a < 5) && b > 10) {
    // Do something
} else if ((a >= 5) && (b > 10)){
    // handled else condition
} else if((a < 5) && (b <= 10)) {
    // handled else condition
}

，但这种条件并不能处理所有可能性，并且缺少条件，

} else if ((a >= 5) && (b <= 10)) {
   // missing condition which is not handled
}

我正在尝试通过静态分析和使用源代码的抽象语法树来查找此类漏洞。有没有任何算法、方法或任何论文研究这样的问题？

Answer 1

如果您有类似的代码

if(A) { ... }
else if (B) { ... }
else if (C) { ... }

并且希望确保处理所有可能性，那么您必须证明公式 A 或 B 或 C 的计算结果始终为 true。如果您所做的只是检查范围，那么我会将此公式转换为联合范式。

经过此转换后，您将得到以下形式的公式

(F1 or F2 or ...) and (G1 or G2 or G3) and (H1 or H2 or H3) ...

，其中每个原子命题的形式为 (x < c), (x ≤ c), (x > c) 或 (x ≥ c)，其中 x 是变量，c 是常量。这些命题可以通过使用以下转换进行组合：

1. (x < c1) 与 (x > c2) 一起转换为 true 如果(c1 > c2)
2. (x < c1) 与 (x ≥ c2) 一起转换为 true if (c1 ≥ c2)
3. (x ≤ c1) 与 (x > c2) 一起转换为 true if (c1 ≥ c2)
4. (x ≤ c1) 与 (x ≥ c2) 一起转换为 true if (c1 ≥ c2)

现在看看子句(F1 or F2 or ...)。一旦您能够执行其中一个转换，整个子句就有效，您可以开始检查下一个子句。

如果所有子句都有效，则处理所有可能性。

通用解决方案（其中 if 语句中的条件可以是任何内容）并不是那么简单。例如，如果您想检查 if(f(x) || g(x))，则可能是 f() 或 g() 有副作用，或者执行非常复杂的计算。

Answer 2

如果您希望将问题简化为更普遍的问题，可以将代码转换

if ((a < 5) && b > 10) {
    // Do something
} else if ((a >= 5) && (b > 10)){
    // handled else condition
} else if((a < 5) && (b <= 10)) {
    // handled else condition
}

为：

if ((a < 5) && b > 10) {
    // Do something
} else if ((a >= 5) && (b > 10)){
    // handled else condition
} else if((a < 5) && (b <= 10)) {
    // handled else condition
} else {
/*@ assert false ; */
}

合理的编译器会为转换后的版本发出与原始版本相同的代码，现在您可以使用静态分析或测试生成来验证 assert 是否成立，这与验证最后的else永远不会被采用，这正是您感兴趣的属性。

如果上述代码是Java（断言可以是JML注释），C（断言可以是ACSL注释），则存在工具) 或 C#（断言可以是 Spec# 注释）。 Elian Ebbing 的算法很好，但我建议另一种选择，让用作这些工具后端的自动定理证明器来完成这项工作，而无需重新实现确定给定逻辑命题是否为同义反复的轮子。现有的轮子很可能比您所能得到的更好。

C 语言示例，使用 Frama-C 和 Jessie：

int a, b;

main(){
  if ((a < 5) && b > 10) {
    // Do something
  } else if ((a >= 5) && (b > 10)){
    // handled else condition
  } else if((a < 5) && (b <= 10)) {
    // handled else condition
  } else {
    /*@ assert \false ; */
  } 
}

断言未验证，表明 Jessie 无法验证最后一个案例是否无法访问。添加 } else if ((a >= 5) && (b <= 10)) {，断言得到验证。