Juliet测试用例Integer Underflow缺陷有效性及Facebook Infer未检出问询

结论 #

该风险是100%有效的确定性整数下溢缺陷，符合CWE-191整数下溢弱点的判定标准，合格的静态分析工具应当识别该问题并告警。

缺陷验证逻辑 #

对应的问题代码如下：

public void bad() throws Throwable
  {
      int data;

      /* POTENTIAL FLAW: Use the maximum value for this type */
      data = Integer.MIN_VALUE;

      if(data < 0) /* ensure we won't have an overflow */
      {

      /* POTENTIAL FLAW: if (data * 2) < Integer.MIN_VALUE, this will underflow */
      int result = (int)(data * 2);
      IO.writeLine("result: " + result);
     }
  }

Java平台中int是32位有符号整数，取值范围为-2^31 ~ 2^31 -1，也就是Integer.MIN_VALUE = -2147483648：

• 代码中data被显式赋值为Integer.MIN_VALUE，必然命中if(data < 0)分支
• 执行data * 2时，计算结果为-4294967296，远小于int类型的最小值，触发整数下溢，结果会被截断为不符合业务预期的异常值
• 若该计算结果后续用于数组下标、内存分配、权限校验等场景，会直接引发越界访问、逻辑绕过等安全问题。

Facebook Infer未检出的原因 #

Infer默认启用的检测规则不包含整数算术溢出/下溢检查，该检测能力属于可选的专项Checker，需要执行扫描时显式开启--integer-overflow-type参数才会触发检测，默认扫描不会覆盖这类问题。

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