|
2 | 2 | * @name Unbounded write |
3 | 3 | * @description Buffer write operations that do not control the length |
4 | 4 | * of data written may overflow. |
5 | | - * @kind problem |
| 5 | + * @kind path-problem |
6 | 6 | * @problem.severity error |
7 | 7 | * @precision medium |
8 | 8 | * @id cpp/unbounded-write |
|
16 | 16 | import semmle.code.cpp.security.BufferWrite |
17 | 17 | import semmle.code.cpp.security.Security |
18 | 18 | import semmle.code.cpp.security.TaintTracking |
| 19 | +import TaintedWithPath |
19 | 20 |
|
20 | 21 | /* |
21 | 22 | * --- Summary of CWE-120 alerts --- |
@@ -54,32 +55,48 @@ predicate isUnboundedWrite(BufferWrite bw) { |
54 | 55 | * } |
55 | 56 | */ |
56 | 57 |
|
| 58 | +/** |
| 59 | + * Holds if `e` is a source buffer going into an unbounded write `bw` or a |
| 60 | + * qualifier of (a qualifier of ...) such a source. |
| 61 | + */ |
| 62 | +predicate unboundedWriteSource(Expr e, BufferWrite bw) { |
| 63 | + isUnboundedWrite(bw) and e = bw.getASource() |
| 64 | + or |
| 65 | + exists(FieldAccess fa | unboundedWriteSource(fa, bw) and e = fa.getQualifier()) |
| 66 | +} |
| 67 | + |
57 | 68 | /* |
58 | 69 | * --- user input reach --- |
59 | 70 | */ |
60 | 71 |
|
61 | | -/** |
62 | | - * Identifies expressions that are potentially tainted with user |
63 | | - * input. Most of the work for this is actually done by the |
64 | | - * TaintTracking library. |
65 | | - */ |
66 | | -predicate tainted2(Expr expr, Expr inputSource, string inputCause) { |
67 | | - taintedIncludingGlobalVars(inputSource, expr, _) and |
68 | | - inputCause = inputSource.toString() |
69 | | - or |
70 | | - exists(Expr e | tainted2(e, inputSource, inputCause) | |
71 | | - // field accesses of a tainted struct are tainted |
72 | | - e = expr.(FieldAccess).getQualifier() |
73 | | - ) |
| 72 | +class Configuration extends TaintTrackingConfiguration { |
| 73 | + override predicate isSink(Element tainted) { unboundedWriteSource(tainted, _) } |
| 74 | + |
| 75 | + override predicate taintThroughGlobals() { any() } |
74 | 76 | } |
75 | 77 |
|
76 | 78 | /* |
77 | 79 | * --- put it together --- |
78 | 80 | */ |
79 | 81 |
|
80 | | -from BufferWrite bw, Expr inputSource, string inputCause |
| 82 | +/* |
| 83 | + * An unbounded write is, for example `strcpy(..., tainted)`. We're looking |
| 84 | + * for a tainted source buffer of an unbounded write, where this source buffer |
| 85 | + * is a sink in the taint-tracking analysis. |
| 86 | + * |
| 87 | + * In the case of `gets` and `scanf`, where the source buffer is implicit, the |
| 88 | + * `BufferWrite` library reports the source buffer to be the same as the |
| 89 | + * destination buffer. Since those destination-buffer arguments are also |
| 90 | + * modeled in the taint-tracking library as being _sources_ of taint, they are |
| 91 | + * in practice reported as being tainted because the `security.TaintTracking` |
| 92 | + * library does not distinguish between taint going into an argument and out of |
| 93 | + * an argument. Thus, we get the desired alerts. |
| 94 | + */ |
| 95 | + |
| 96 | +from BufferWrite bw, Expr inputSource, Expr tainted, PathNode sourceNode, PathNode sinkNode |
81 | 97 | where |
82 | | - isUnboundedWrite(bw) and |
83 | | - tainted2(bw.getASource(), inputSource, inputCause) |
84 | | -select bw, "This '" + bw.getBWDesc() + "' with input from $@ may overflow the destination.", |
85 | | - inputSource, inputCause |
| 98 | + taintedWithPath(inputSource, tainted, sourceNode, sinkNode) and |
| 99 | + unboundedWriteSource(tainted, bw) |
| 100 | +select bw, sourceNode, sinkNode, |
| 101 | + "This '" + bw.getBWDesc() + "' with input from $@ may overflow the destination.", inputSource, |
| 102 | + inputSource.toString() |
0 commit comments