Name: Infinite loop with unsatisfiable exit condition

Description:

A loop with an unsatisfiable exit condition could prevent the program from terminating, making it vulnerable to a denial of service attack.

ID: cpp/infinite-loop-with-unsatisfiable-exit-condition

Kind: problem

Severity: warning

/**
 * @name Infinite loop with unsatisfiable exit condition
 * @description A loop with an unsatisfiable exit condition could
 *              prevent the program from terminating, making it
 *              vulnerable to a denial of service attack.
 * @kind problem
 * @id cpp/infinite-loop-with-unsatisfiable-exit-condition
 * @problem.severity warning
 * @tags security
 *       external/cwe/cwe-835
 */
import cpp
import semmle.code.cpp.controlflow.BasicBlocks
private import semmle.code.cpp.rangeanalysis.PointlessComparison
import semmle.code.cpp.controlflow.internal.ConstantExprs

/**
 * Holds if there is a control flow edge from `src` to `dst`, but
 * it can never be taken due to `cmp` always having value `value`.
 */
predicate impossibleEdge(
  ComparisonOperation cmp, boolean value, BasicBlock src, BasicBlock dst) {
  cmp = src.getEnd() and
  reachablePointlessComparison(cmp, _, _, value, _) and
  if value = true
    then dst = src.getAFalseSuccessor()
    else dst = src.getATrueSuccessor()
}

BasicBlock enhancedSucc(BasicBlock bb) {
  result = bb.getASuccessor() and not impossibleEdge(_, _, bb, result)
}

/**
 * Holds if `cmp` always has value `value`, and if that will cause
 * non-termination.
 *
 * It only holds if the function exit is reachable using
 * the standard `getASuccessor` relation, but not using
 * `enhancedSucc`. This means that it does not hold for
 * comparison operations which are trivially true or false, such as
 * ```
 * while (1) { ... }
 * ```
 * Since this loop is obviously infinite, we assume that it was written
 * intentionally.
 */
predicate impossibleEdgeCausesNonTermination(
  ComparisonOperation cmp, boolean value) {
  exists (BasicBlock src
  | impossibleEdge(cmp, value, src, _) and
    src.getASuccessor+() instanceof ExitBasicBlock and
    not (enhancedSucc+(src) instanceof ExitBasicBlock) and
    // Make sure that the source is reachable to reduce
    // false positives.
    exists (EntryBasicBlock entry | src = enhancedSucc+(entry)))
}

from ComparisonOperation cmp, boolean value
where impossibleEdgeCausesNonTermination(cmp, value)
select
  cmp,
  "Function exit is unreachable because this condition is always " +
  value.toString() + "."

Loops can contain multiple exit conditions, either directly in the loop condition or as guards around break or return statements. If none of the exit conditions can ever be satisfied, then the loop will never terminate. A program containing an infinite loop could be vulnerable to a denial of service attack if it is possible for an attacker to trigger the loop.

Recommendation

When writing a loop that is intended to terminate, make sure that all the necessary exit conditions can be satisfied and that loop termination is clear.

Example

The following example shows an infinite loop. The value of variable i is always zero, so the condition guarding the break is always false.

     1void test(int n) {
     2  int i = 0;
     3  if (n <= 0) {
     4    return;
     5  }
     6  while (1) {
     7    // BAD: condition is never true, so loop will not terminate.
     8    if (i == n) {
     9      break;
    10    }
    11  }
    12}
void test(int n) {
  int i = 0;
  if (n <= 0) {
    return;
  }
  while (1) {
    // BAD: condition is never true, so loop will not terminate.
    if (i == n) {
      break;
    }
  }
}

The error has been fixed below by incrementing i in the body of the loop.

     1void test(int n) {
     2  int i = 0;
     3  if (n <= 0) {
     4    return;
     5  }
     6  while (1) {
     7    // GOOD: condition is true after n iterations.
     8    if (i == n) {
     9      break;
    10    }
    11    i++;
    12  }
    13}
void test(int n) {
  int i = 0;
  if (n <= 0) {
    return;
  }
  while (1) {
    // GOOD: condition is true after n iterations.
    if (i == n) {
      break;
    }
    i++;
  }
}
References