CWE190_Integer_Overflow

[ch4rli3kop]

add, multiply, sub 등의 연산과정에서 발생하는 integer overflow

• [x] Add
• [x] Multiply
• [ ] Square
• [ ] User Input Tracking

[ch4rli3kop]

ssa form에서는 하나의 연산에 대해서 새로운 변수를 만들기 때문에, 항상 a = b + c 형태를 가짐. 따라서, SET_VAR_SSA operation으로 먼저 찾았고, 그 뒤 우항의 operation이 ADD인 경우를 찾음. 세 변수의 possible range value를 구하여 비교함. source #11

    for func in bv.functions:
        for inst in func.mlil.ssa_form.instructions:
            if inst.operation == MediumLevelILOperation.MLIL_SET_VAR_SSA:
                #print(inst)
                if inst.src.operation == MediumLevelILOperation.MLIL_ADD:

                    # FIXME: 우항이 상수일 때 추가

                    if type(inst.src.right) == binaryninja.mediumlevelil.MediumLevelILVarSsa:
                        # a = b + c
                        a = inst.dest
                        b = inst.src.left.src
                        c = inst.src.right.src
                        #print(a, b, c)
                        a_range = inst.get_ssa_var_possible_values(a)
                        b_range = inst.get_ssa_var_possible_values(b)
                        c_range = inst.get_ssa_var_possible_values(c)

                        if a.var.type.get_string() == 'char':
                            a_range = a_range.signed_range_value([ValueRange(-128, 127, 1)])
                            # print(f'{func.start:#x}', inst, a_range, b_range, c_range)
                            try:
                                # FIXME: sometimes it can be RegisterValueType.InSetOfValues type
                                if a_range.ranges[0].end < b_range.ranges[0].end + c_range.ranges[0].end:
                                    #print('integer overflow!')
                                    result.append(func)
                            except:
                                pass

세 변수의 타입이 다를 경우와 한 변수가 상수일 경우, range 타입이 아닌 InSetOfValues 타입일 경우에 대해서는 구현 예정.

cpp binaries : 10
result [File]: 
good: 22/38     missed: 4/38    false positive: 16/38
result [Vulnerabilities]: 
good: 22/46     missed: 4/46    false positive: 20/46

[ch4rli3kop]

z3 solver 사용해서 타입에서 지정된 범위 넘어가는 식이 존재하는지 확인하는 형태로 탐지루틴 수정.

14

  if inst.src.operation == MediumLevelILOperation.MLIL_ADD:
      # FIXME: Range의 경우가 path에 영향을 받을 때, 현재 path를 구분하지 못하므로 false positive가 많음.
      # TODO: a = 상수 + 상수 형태는 바이너리 닌자 LLIL -> MLIL 과정에서 a = value 형태로 최적화됨. 해당 경우 LLIL로 탐지해야 함.

      if type(inst.src.right) == MediumLevelILConst and type(inst.src.left) == MediumLevelILVarSsa:
          # a = b + c(constant value)
          a = inst.dest
          b = inst.src.left.src
          c = inst.src.right.constant

          pv_b = inst.get_ssa_var_possible_values(b)
          pv_a = return_a_range(a.type.get_string())
          if pv_a is None:
              continue

          solver = Solver()
          b = Int('b')                            
          b_type = pv_b.type

          if b_type in { RegisterValueType.SignedRangeValue, RegisterValueType.UnsignedRangeValue }:
              pv_b = pv_b.ranges[0]
              bi = Int('bi')
              solver.add(b == pv_b.start + bi * pv_b.step)
              solver.add(0 <= bi, bi <= (pv_b.end - pv_b.start)/pv_b.step)
          elif b_type in { RegisterValueType.InSetOfValues }:
              solver.add(Or([b == value for value in pv_b.values]))

          if b_type in {RegisterValueType.SignedRangeValue, RegisterValueType.UnsignedRangeValue, RegisterValueType.InSetOfValues}:
              solver.push()
              solver.add( b+c < pv_a.start )
              if solver.check() == sat:
                  print('integer overflow!')
                  result.append(func)
              else:
                  solver.pop()
                  solver.add( b+c > pv_a.end )
                  if solver.check() == sat:
                      print('integer overflow!')
                      result.append(func)