@@ -89,45 +89,83 @@ predicate referenceTo(Expr source, Expr use) {
89
89
)
90
90
}
91
91
92
- from Expr check , Expr checkPath , FunctionCall use , Expr usePath
93
- where
94
- // `check` looks like a check on a filename
95
- (
96
- (
97
- // either:
98
- // an access check
99
- check = accessCheck ( checkPath )
100
- or
101
- // a stat
102
- check = stat ( checkPath , _)
103
- or
104
- // access to a member variable on the stat buf
105
- // (morally, this should be a use-use pair, but it seems unlikely
106
- // that this variable will get reused in practice)
107
- exists ( Expr call , Expr e , Variable v |
108
- call = stat ( checkPath , e ) and
109
- e .getAChild * ( ) .( VariableAccess ) .getTarget ( ) = v and
110
- check .( VariableAccess ) .getTarget ( ) = v and
111
- not e .getAChild * ( ) = check // the call that writes to the pointer is not where the pointer is checked.
112
- )
113
- ) and
114
- // `op` looks like an operation on a filename
115
- use = filenameOperation ( usePath )
116
- or
117
- // another filename operation (null pointers can indicate errors)
118
- check = filenameOperation ( checkPath ) and
119
- // `op` looks like a sensitive operation on a filename
120
- use = sensitiveFilenameOperation ( usePath )
121
- ) and
122
- // `checkPath` and `usePath` refer to the same SSA variable
123
- exists ( SsaDefinition def , StackVariable v |
124
- def .getAUse ( v ) = checkPath and def .getAUse ( v ) = usePath
92
+ pragma [ noinline]
93
+ predicate statCallWithPointer ( Expr checkPath , Expr call , Expr e , Variable v ) {
94
+ call = stat ( checkPath , e ) and
95
+ e .getAChild * ( ) .( VariableAccess ) .getTarget ( ) = v
96
+ }
97
+
98
+ predicate checksPath ( Expr check , Expr checkPath ) {
99
+ // either:
100
+ // an access check
101
+ check = accessCheck ( checkPath )
102
+ or
103
+ // a stat
104
+ check = stat ( checkPath , _)
105
+ or
106
+ // access to a member variable on the stat buf
107
+ // (morally, this should be a use-use pair, but it seems unlikely
108
+ // that this variable will get reused in practice)
109
+ exists ( Expr call , Expr e , Variable v |
110
+ statCallWithPointer ( checkPath , call , e , v ) and
111
+ check .( VariableAccess ) .getTarget ( ) = v and
112
+ not e .getAChild * ( ) = check // the call that writes to the pointer is not where the pointer is checked.
113
+ )
114
+ }
115
+
116
+ pragma [ nomagic]
117
+ predicate checkPathControlsUse ( Expr check , Expr checkPath , Expr use ) {
118
+ exists ( GuardCondition guard | referenceTo ( check , guard .getAChild * ( ) ) |
119
+ guard .controls ( use .getBasicBlock ( ) , _)
125
120
) and
126
- // the return value of `check` is used (possibly with one step of
127
- // variable indirection) in a guard which controls `use`
121
+ checksPath ( pragma [ only_bind_into ] ( check ) , checkPath )
122
+ }
123
+
124
+ pragma [ nomagic]
125
+ predicate fileNameOperationControlsUse ( Expr check , Expr checkPath , Expr use ) {
128
126
exists ( GuardCondition guard | referenceTo ( check , guard .getAChild * ( ) ) |
129
- guard .controls ( use .( ControlFlowNode ) .getBasicBlock ( ) , _)
130
- )
127
+ guard .controls ( use .getBasicBlock ( ) , _)
128
+ ) and
129
+ pragma [ only_bind_into ] ( check ) = filenameOperation ( checkPath )
130
+ }
131
+
132
+ predicate checkUse ( Expr check , Expr checkPath , FunctionCall use , Expr usePath ) {
133
+ // `check` is part of a guard that controls `use`
134
+ checkPathControlsUse ( check , checkPath , use ) and
135
+ // `check` looks like a check on a filename
136
+ checksPath ( check , checkPath ) and
137
+ // `op` looks like an operation on a filename
138
+ use = filenameOperation ( usePath )
139
+ or
140
+ // `check` is part of a guard that controls `use`
141
+ fileNameOperationControlsUse ( check , checkPath , use ) and
142
+ // another filename operation (null pointers can indicate errors)
143
+ check = filenameOperation ( checkPath ) and
144
+ // `op` looks like a sensitive operation on a filename
145
+ use = sensitiveFilenameOperation ( usePath )
146
+ }
147
+
148
+ pragma [ noinline]
149
+ predicate isCheckedPath (
150
+ Expr check , SsaDefinition def , StackVariable v , FunctionCall use , Expr usePath , Expr checkPath
151
+ ) {
152
+ checkUse ( check , checkPath , use , usePath ) and
153
+ def .getAUse ( v ) = checkPath
154
+ }
155
+
156
+ pragma [ noinline]
157
+ predicate isUsedPath (
158
+ Expr check , SsaDefinition def , StackVariable v , FunctionCall use , Expr usePath , Expr checkPath
159
+ ) {
160
+ checkUse ( check , checkPath , use , usePath ) and
161
+ def .getAUse ( v ) = usePath
162
+ }
163
+
164
+ from Expr check , Expr checkPath , FunctionCall use , Expr usePath , SsaDefinition def , StackVariable v
165
+ where
166
+ // `checkPath` and `usePath` refer to the same SSA variable
167
+ isCheckedPath ( check , def , v , use , usePath , checkPath ) and
168
+ isUsedPath ( check , def , v , use , usePath , checkPath )
131
169
select use ,
132
170
"The $@ being operated upon was previously $@, but the underlying file may have been changed since then." ,
133
171
usePath , "filename" , check , "checked"
0 commit comments