1616
1717import cpp
1818import semmle.code.cpp.security.Overflow
19- import semmle.code.cpp.security.Security
20- import semmle.code.cpp.ir.dataflow.internal.DefaultTaintTrackingImpl
19+ import semmle.code.cpp.dataflow.new.TaintTracking
20+ import semmle.code.cpp.ir.IR
21+ import semmle.code.cpp.controlflow.IRGuards as IRGuards
2122
2223predicate isMaxValue ( Expr mie ) {
2324 exists ( MacroInvocation mi |
2425 mi .getExpr ( ) = mie and
25- (
26- mi .getMacroName ( ) = "CHAR_MAX" or
27- mi .getMacroName ( ) = "LLONG_MAX" or
28- mi .getMacroName ( ) = "INT_MAX" or
29- mi .getMacroName ( ) = "SHRT_MAX" or
30- mi .getMacroName ( ) = "UINT_MAX"
31- )
26+ mi .getMacroName ( ) = [ "CHAR_MAX" , "LLONG_MAX" , "INT_MAX" , "SHRT_MAX" , "UINT_MAX" ]
3227 )
3328}
3429
3530predicate isMinValue ( Expr mie ) {
3631 exists ( MacroInvocation mi |
3732 mi .getExpr ( ) = mie and
38- (
39- mi .getMacroName ( ) = "CHAR_MIN" or
40- mi .getMacroName ( ) = "LLONG_MIN" or
41- mi .getMacroName ( ) = "INT_MIN" or
42- mi .getMacroName ( ) = "SHRT_MIN"
43- )
33+ mi .getMacroName ( ) = [ "CHAR_MIN" , "LLONG_MIN" , "INT_MIN" , "SHRT_MIN" ]
4434 )
4535}
4636
47- class SecurityOptionsArith extends SecurityOptions {
48- override predicate isUserInput ( Expr expr , string cause ) {
37+ predicate isSource ( DataFlow :: Node source , string cause ) {
38+ exists ( Expr expr | expr = source . asExpr ( ) |
4939 isMaxValue ( expr ) and cause = "max value"
5040 or
5141 isMinValue ( expr ) and cause = "min value"
52- }
53- }
54-
55- predicate taintedVarAccess ( Expr origin , VariableAccess va , string cause ) {
56- isUserInput ( origin , cause ) and
57- tainted ( origin , va )
42+ )
5843}
5944
6045predicate causeEffectCorrespond ( string cause , string effect ) {
@@ -65,16 +50,79 @@ predicate causeEffectCorrespond(string cause, string effect) {
6550 effect = "underflow"
6651}
6752
68- from Expr origin , Operation op , VariableAccess va , string cause , string effect
69- where
70- taintedVarAccess ( origin , va , cause ) and
71- op .getAnOperand ( ) = va and
72- (
53+ predicate isSink ( DataFlow :: Node sink , VariableAccess va , string effect ) {
54+ exists ( Operation op |
55+ sink . asExpr ( ) = va and
56+ op .getAnOperand ( ) = va
57+ |
7358 missingGuardAgainstUnderflow ( op , va ) and effect = "underflow"
7459 or
7560 missingGuardAgainstOverflow ( op , va ) and effect = "overflow"
76- ) and
77- causeEffectCorrespond ( cause , effect )
61+ )
62+ }
63+
64+ predicate hasUpperBoundsCheck ( Variable var ) {
65+ exists ( RelationalOperation oper , VariableAccess access |
66+ oper .getAnOperand ( ) = access and
67+ access .getTarget ( ) = var and
68+ // Comparing to 0 is not an upper bound check
69+ not oper .getAnOperand ( ) .getValue ( ) = "0"
70+ )
71+ }
72+
73+ predicate constantInstruction ( Instruction instr ) {
74+ instr instanceof ConstantInstruction or
75+ constantInstruction ( instr .( UnaryInstruction ) .getUnary ( ) )
76+ }
77+
78+ predicate readsVariable ( LoadInstruction load , Variable var ) {
79+ load .getSourceAddress ( ) .( VariableAddressInstruction ) .getAstVariable ( ) = var
80+ }
81+
82+ predicate nodeIsBarrierEqualityCandidate ( DataFlow:: Node node , Operand access , Variable checkedVar ) {
83+ exists ( Instruction instr | instr = node .asInstruction ( ) |
84+ readsVariable ( instr , checkedVar ) and
85+ any ( IRGuards:: IRGuardCondition guard ) .ensuresEq ( access , _, _, instr .getBlock ( ) , true )
86+ )
87+ }
88+
89+ module Config implements DataFlow:: ConfigSig {
90+ predicate isSource ( DataFlow:: Node source ) { isSource ( source , _) }
91+
92+ predicate isSink ( DataFlow:: Node sink ) { isSink ( sink , _, _) }
93+
94+ predicate isBarrier ( DataFlow:: Node node ) {
95+ // Block flow if there's an upper bound check of the variable anywhere in the program
96+ exists ( Variable checkedVar , Instruction instr | instr = node .asInstruction ( ) |
97+ readsVariable ( instr , checkedVar ) and
98+ hasUpperBoundsCheck ( checkedVar )
99+ )
100+ or
101+ // Block flow if the node is guarded by an equality check
102+ exists ( Variable checkedVar , Operand access |
103+ nodeIsBarrierEqualityCandidate ( node , access , checkedVar ) and
104+ readsVariable ( access .getDef ( ) , checkedVar )
105+ )
106+ or
107+ // Block flow to any binary instruction whose operands are both non-constants.
108+ exists ( BinaryInstruction iTo |
109+ iTo = node .asInstruction ( ) and
110+ not constantInstruction ( iTo .getLeft ( ) ) and
111+ not constantInstruction ( iTo .getRight ( ) ) and
112+ // propagate taint from either the pointer or the offset, regardless of constantness
113+ not iTo instanceof PointerArithmeticInstruction
114+ )
115+ }
116+ }
117+
118+ module Flow = TaintTracking:: Global< Config > ;
119+
120+ from DataFlow:: Node source , DataFlow:: Node sink , VariableAccess va , string cause , string effect
121+ where
122+ Flow:: flow ( source , sink ) and
123+ isSource ( source , cause ) and
124+ causeEffectCorrespond ( cause , effect ) and
125+ isSink ( sink , va , effect )
78126select va ,
79127 "$@ flows to an operand of an arithmetic expression, potentially causing an " + effect + "." ,
80- origin , "Extreme value"
128+ source , "Extreme value"
0 commit comments