@@ -89,45 +89,83 @@ predicate referenceTo(Expr source, Expr use) {
8989 )
9090}
9191
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 ( ) , _)
125120 ) 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 ) {
128126 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 )
131169select use ,
132170 "The $@ being operated upon was previously $@, but the underlying file may have been changed since then." ,
133171 usePath , "filename" , check , "checked"
0 commit comments