From bea38fcd074d4e0079f0ee63de1c43bf1e6057f1 Mon Sep 17 00:00:00 2001 From: Joe Date: Mon, 28 Sep 2020 16:25:45 +0100 Subject: [PATCH 1/5] Java: Add taint modelling for string format methods --- .../dataflow/internal/TaintTrackingUtil.qll | 77 ++++++++++++++++++- .../dataflow/taint-format/A.java | 34 ++++++++ .../dataflow/taint-format/options | 1 + .../dataflow/taint-format/test.expected | 24 ++++++ .../dataflow/taint-format/test.ql | 16 ++++ 5 files changed, 151 insertions(+), 1 deletion(-) create mode 100644 java/ql/test/library-tests/dataflow/taint-format/A.java create mode 100644 java/ql/test/library-tests/dataflow/taint-format/options create mode 100644 java/ql/test/library-tests/dataflow/taint-format/test.expected create mode 100644 java/ql/test/library-tests/dataflow/taint-format/test.ql diff --git a/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll b/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll index eaf7c9d26dc..8d551ecdaff 100644 --- a/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll +++ b/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll @@ -13,6 +13,7 @@ private import semmle.code.java.frameworks.spring.SpringHttp private import semmle.code.java.Maps private import semmle.code.java.dataflow.internal.ContainerFlow private import semmle.code.java.frameworks.jackson.JacksonSerializability +private import semmle.code.java.StringFormat /** * Holds if taint can flow from `src` to `sink` in zero or more @@ -124,6 +125,8 @@ private predicate localAdditionalTaintExprStep(Expr src, Expr sink) { stringBuilderStep(src, sink) or serializationStep(src, sink) + or + formatStep(src, sink) } /** @@ -387,6 +390,11 @@ private predicate taintPreservingQualifierToMethod(Method m) { stringlist.getTypeArgument(0) instanceof TypeString ) ) + or + m instanceof StringFormatMethod + or + m.getDeclaringType() instanceof TypeFormatter and + m.hasName("out") } private class StringReplaceMethod extends Method { @@ -446,7 +454,9 @@ private predicate argToMethodStep(Expr tracked, MethodAccess sink) { */ private predicate taintPreservingArgumentToMethod(Method method) { method.getDeclaringType() instanceof TypeString and - (method.hasName("format") or method.hasName("formatted") or method.hasName("join")) + method.hasName("join") + or + method instanceof StringFormatMethod } /** @@ -625,6 +635,21 @@ private predicate argToQualifierStep(Expr tracked, Expr sink) { tracked = ma.getArgument(i) and sink = ma.getQualifier() ) + or + exists(Method m, MethodAccess ma | + taintPreservingArgumentToQualifier(m) and + ma.getMethod() = m and + tracked = ma.getAnArgument() and + sink = ma.getQualifier() + ) +} + +/** + * Holds if `method` is a method that transfers taint from any of its arguments to its qualifier. + */ +private predicate taintPreservingArgumentToQualifier(Method method) { + method instanceof StringFormatMethod and + not method.getDeclaringType() instanceof TypeString } /** @@ -722,6 +747,56 @@ class ObjectOutputStreamVar extends LocalVariableDecl { } } +/** Flow through string formatting. */ +private predicate formatStep(Expr tracked, Expr sink) { + exists(FormatterVar v, VariableAssign def | + def = v.getADef() and + exists(MethodAccess ma, RValue use | + ma.getAnArgument() = tracked and + ma = v.getAFormatMethodAccess() and + use = ma.getQualifier() and + defUsePair(def, use) + ) and + exists(RValue output, ClassInstanceExpr cie | + cie = def.getSource() and + output = cie.getArgument(0) and + adjacentUseUse(output, sink) and + exists(RefType t | output.getType().(RefType).getASourceSupertype*() = t | + t.hasQualifiedName("java.io", "OutputStream") or + t.hasQualifiedName("java.lang", "Appendable") + ) + ) + ) +} + +/** + * A local variable that is assigned a `Formatter`. + * Writing tainted data to such a formatter causes the underlying + * `OutputStream` or `Appenable` to be tainted. + */ +private class FormatterVar extends LocalVariableDecl { + FormatterVar() { + exists(ClassInstanceExpr cie | cie = this.getAnAssignedValue() | + cie.getType() instanceof TypeFormatter + ) + } + + VariableAssign getADef() { + result.getSource().(ClassInstanceExpr).getType() instanceof TypeFormatter and + result.getDestVar() = this + } + + MethodAccess getAFormatMethodAccess() { + result.getQualifier() = getAnAccess() and + result.getMethod().hasName("format") + } +} + +/** The class `java.util.Formatter`. */ +private class TypeFormatter extends Class { + TypeFormatter() { this.hasQualifiedName("java.util", "Formatter") } +} + private import StringBuilderVarModule module StringBuilderVarModule { diff --git a/java/ql/test/library-tests/dataflow/taint-format/A.java b/java/ql/test/library-tests/dataflow/taint-format/A.java new file mode 100644 index 00000000000..c9bb27c8e99 --- /dev/null +++ b/java/ql/test/library-tests/dataflow/taint-format/A.java @@ -0,0 +1,34 @@ +import java.util.Formatter; +import java.lang.StringBuilder; + +class A { + public static String taint() { return "tainted"; } + + public static void test1() { + String bad = taint(); + String good = "hi"; + + bad.formatted(good); + good.formatted("a", bad, "b", good); + String.format("%s%s", bad, good); + } + + public static void test2() { + String bad = taint(); + Formatter f = new Formatter(); + + f.toString(); + f.format("%s", bad); + f.toString(); + } + + public static void test3() { + String bad = taint(); + StringBuilder sb = new StringBuilder(); + Formatter f = new Formatter(sb); + + sb.toString(); // false positive + f.format("%s", bad); + sb.toString(); + } +} \ No newline at end of file diff --git a/java/ql/test/library-tests/dataflow/taint-format/options b/java/ql/test/library-tests/dataflow/taint-format/options new file mode 100644 index 00000000000..814f667417c --- /dev/null +++ b/java/ql/test/library-tests/dataflow/taint-format/options @@ -0,0 +1 @@ +//semmle-extractor-options: --javac-args --enable-preview -source 14 -target 14 \ No newline at end of file diff --git a/java/ql/test/library-tests/dataflow/taint-format/test.expected b/java/ql/test/library-tests/dataflow/taint-format/test.expected new file mode 100644 index 00000000000..9e0e64f695c --- /dev/null +++ b/java/ql/test/library-tests/dataflow/taint-format/test.expected @@ -0,0 +1,24 @@ +| A.java:8:22:8:28 | taint(...) | A.java:8:22:8:28 | taint(...) | +| A.java:8:22:8:28 | taint(...) | A.java:11:9:11:11 | bad | +| A.java:8:22:8:28 | taint(...) | A.java:11:9:11:27 | formatted(...) | +| A.java:8:22:8:28 | taint(...) | A.java:12:9:12:43 | formatted(...) | +| A.java:8:22:8:28 | taint(...) | A.java:12:9:12:43 | new ..[] { .. } | +| A.java:8:22:8:28 | taint(...) | A.java:12:29:12:31 | bad | +| A.java:8:22:8:28 | taint(...) | A.java:13:9:13:40 | format(...) | +| A.java:8:22:8:28 | taint(...) | A.java:13:9:13:40 | new ..[] { .. } | +| A.java:8:22:8:28 | taint(...) | A.java:13:31:13:33 | bad | +| A.java:17:22:17:28 | taint(...) | A.java:17:22:17:28 | taint(...) | +| A.java:17:22:17:28 | taint(...) | A.java:21:9:21:9 | f [post update] | +| A.java:17:22:17:28 | taint(...) | A.java:21:9:21:27 | format(...) | +| A.java:17:22:17:28 | taint(...) | A.java:21:9:21:27 | new ..[] { .. } | +| A.java:17:22:17:28 | taint(...) | A.java:21:24:21:26 | bad | +| A.java:17:22:17:28 | taint(...) | A.java:22:9:22:9 | f | +| A.java:26:22:26:28 | taint(...) | A.java:26:22:26:28 | taint(...) | +| A.java:26:22:26:28 | taint(...) | A.java:30:9:30:10 | sb | +| A.java:26:22:26:28 | taint(...) | A.java:30:9:30:21 | toString(...) | +| A.java:26:22:26:28 | taint(...) | A.java:31:9:31:9 | f [post update] | +| A.java:26:22:26:28 | taint(...) | A.java:31:9:31:27 | format(...) | +| A.java:26:22:26:28 | taint(...) | A.java:31:9:31:27 | new ..[] { .. } | +| A.java:26:22:26:28 | taint(...) | A.java:31:24:31:26 | bad | +| A.java:26:22:26:28 | taint(...) | A.java:32:9:32:10 | sb | +| A.java:26:22:26:28 | taint(...) | A.java:32:9:32:21 | toString(...) | diff --git a/java/ql/test/library-tests/dataflow/taint-format/test.ql b/java/ql/test/library-tests/dataflow/taint-format/test.ql new file mode 100644 index 00000000000..0a877c0c985 --- /dev/null +++ b/java/ql/test/library-tests/dataflow/taint-format/test.ql @@ -0,0 +1,16 @@ +import java +import semmle.code.java.dataflow.TaintTracking + +class Conf extends TaintTracking::Configuration { + Conf() { this = "qltest:dataflow:format" } + + override predicate isSource(DataFlow::Node n) { + n.asExpr().(MethodAccess).getMethod().hasName("taint") + } + + override predicate isSink(DataFlow::Node n) { any() } +} + +from DataFlow::Node src, DataFlow::Node sink, Conf conf +where conf.hasFlow(src, sink) +select src, sink From eccfa5d26a0041c8c30967829a1092925cca4202 Mon Sep 17 00:00:00 2001 From: Joe Farebrother Date: Tue, 29 Sep 2020 15:34:05 +0100 Subject: [PATCH 2/5] Fix documentation typo Co-authored-by: intrigus-lgtm <60750685+intrigus-lgtm@users.noreply.github.com> --- .../semmle/code/java/dataflow/internal/TaintTrackingUtil.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll b/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll index 8d551ecdaff..02ba42fc2fa 100644 --- a/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll +++ b/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll @@ -772,7 +772,7 @@ private predicate formatStep(Expr tracked, Expr sink) { /** * A local variable that is assigned a `Formatter`. * Writing tainted data to such a formatter causes the underlying - * `OutputStream` or `Appenable` to be tainted. + * `OutputStream` or `Appendable` to be tainted. */ private class FormatterVar extends LocalVariableDecl { FormatterVar() { From efc3a2523790d1c2c8ab739645e543686a5ad873 Mon Sep 17 00:00:00 2001 From: Joe Date: Tue, 29 Sep 2020 16:02:51 +0100 Subject: [PATCH 3/5] Java: Don't pass taint through the format methods of `Console` --- .../code/java/dataflow/internal/TaintTrackingUtil.qll | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll b/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll index 02ba42fc2fa..f9da6342b35 100644 --- a/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll +++ b/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll @@ -456,7 +456,8 @@ private predicate taintPreservingArgumentToMethod(Method method) { method.getDeclaringType() instanceof TypeString and method.hasName("join") or - method instanceof StringFormatMethod + method instanceof StringFormatMethod and + not method.getDeclaringType().hasQualifiedName("java.io", "Console") } /** @@ -649,7 +650,8 @@ private predicate argToQualifierStep(Expr tracked, Expr sink) { */ private predicate taintPreservingArgumentToQualifier(Method method) { method instanceof StringFormatMethod and - not method.getDeclaringType() instanceof TypeString + not method.getDeclaringType() instanceof TypeString and + not method.getDeclaringType().hasQualifiedName("java.io", "Console") } /** From be07d27a4c3594d5de4f77c17de8e6a7d874f4ef Mon Sep 17 00:00:00 2001 From: Joe Date: Tue, 29 Sep 2020 16:36:34 +0100 Subject: [PATCH 4/5] Java: Improve tests --- .../dataflow/taint-format/A.java | 11 ++++ .../dataflow/taint-format/test.expected | 52 ++++++++++--------- 2 files changed, 39 insertions(+), 24 deletions(-) diff --git a/java/ql/test/library-tests/dataflow/taint-format/A.java b/java/ql/test/library-tests/dataflow/taint-format/A.java index c9bb27c8e99..3612c23f950 100644 --- a/java/ql/test/library-tests/dataflow/taint-format/A.java +++ b/java/ql/test/library-tests/dataflow/taint-format/A.java @@ -1,5 +1,7 @@ import java.util.Formatter; import java.lang.StringBuilder; +import java.lang.System; +import java.io.Console; class A { public static String taint() { return "tainted"; } @@ -11,6 +13,7 @@ class A { bad.formatted(good); good.formatted("a", bad, "b", good); String.format("%s%s", bad, good); + String.format("%s", good); } public static void test2() { @@ -31,4 +34,12 @@ class A { f.format("%s", bad); sb.toString(); } + + public static void test4() { + String bad = taint(); + Console c = System.console(); + + c.format(bad); + c.readLine("Enter something: %s", bad); + } } \ No newline at end of file diff --git a/java/ql/test/library-tests/dataflow/taint-format/test.expected b/java/ql/test/library-tests/dataflow/taint-format/test.expected index 9e0e64f695c..c52918fadc5 100644 --- a/java/ql/test/library-tests/dataflow/taint-format/test.expected +++ b/java/ql/test/library-tests/dataflow/taint-format/test.expected @@ -1,24 +1,28 @@ -| A.java:8:22:8:28 | taint(...) | A.java:8:22:8:28 | taint(...) | -| A.java:8:22:8:28 | taint(...) | A.java:11:9:11:11 | bad | -| A.java:8:22:8:28 | taint(...) | A.java:11:9:11:27 | formatted(...) | -| A.java:8:22:8:28 | taint(...) | A.java:12:9:12:43 | formatted(...) | -| A.java:8:22:8:28 | taint(...) | A.java:12:9:12:43 | new ..[] { .. } | -| A.java:8:22:8:28 | taint(...) | A.java:12:29:12:31 | bad | -| A.java:8:22:8:28 | taint(...) | A.java:13:9:13:40 | format(...) | -| A.java:8:22:8:28 | taint(...) | A.java:13:9:13:40 | new ..[] { .. } | -| A.java:8:22:8:28 | taint(...) | A.java:13:31:13:33 | bad | -| A.java:17:22:17:28 | taint(...) | A.java:17:22:17:28 | taint(...) | -| A.java:17:22:17:28 | taint(...) | A.java:21:9:21:9 | f [post update] | -| A.java:17:22:17:28 | taint(...) | A.java:21:9:21:27 | format(...) | -| A.java:17:22:17:28 | taint(...) | A.java:21:9:21:27 | new ..[] { .. } | -| A.java:17:22:17:28 | taint(...) | A.java:21:24:21:26 | bad | -| A.java:17:22:17:28 | taint(...) | A.java:22:9:22:9 | f | -| A.java:26:22:26:28 | taint(...) | A.java:26:22:26:28 | taint(...) | -| A.java:26:22:26:28 | taint(...) | A.java:30:9:30:10 | sb | -| A.java:26:22:26:28 | taint(...) | A.java:30:9:30:21 | toString(...) | -| A.java:26:22:26:28 | taint(...) | A.java:31:9:31:9 | f [post update] | -| A.java:26:22:26:28 | taint(...) | A.java:31:9:31:27 | format(...) | -| A.java:26:22:26:28 | taint(...) | A.java:31:9:31:27 | new ..[] { .. } | -| A.java:26:22:26:28 | taint(...) | A.java:31:24:31:26 | bad | -| A.java:26:22:26:28 | taint(...) | A.java:32:9:32:10 | sb | -| A.java:26:22:26:28 | taint(...) | A.java:32:9:32:21 | toString(...) | +| A.java:10:22:10:28 | taint(...) | A.java:10:22:10:28 | taint(...) | +| A.java:10:22:10:28 | taint(...) | A.java:13:9:13:11 | bad | +| A.java:10:22:10:28 | taint(...) | A.java:13:9:13:27 | formatted(...) | +| A.java:10:22:10:28 | taint(...) | A.java:14:9:14:43 | formatted(...) | +| A.java:10:22:10:28 | taint(...) | A.java:14:9:14:43 | new ..[] { .. } | +| A.java:10:22:10:28 | taint(...) | A.java:14:29:14:31 | bad | +| A.java:10:22:10:28 | taint(...) | A.java:15:9:15:40 | format(...) | +| A.java:10:22:10:28 | taint(...) | A.java:15:9:15:40 | new ..[] { .. } | +| A.java:10:22:10:28 | taint(...) | A.java:15:31:15:33 | bad | +| A.java:20:22:20:28 | taint(...) | A.java:20:22:20:28 | taint(...) | +| A.java:20:22:20:28 | taint(...) | A.java:24:9:24:9 | f [post update] | +| A.java:20:22:20:28 | taint(...) | A.java:24:9:24:27 | format(...) | +| A.java:20:22:20:28 | taint(...) | A.java:24:9:24:27 | new ..[] { .. } | +| A.java:20:22:20:28 | taint(...) | A.java:24:24:24:26 | bad | +| A.java:20:22:20:28 | taint(...) | A.java:25:9:25:9 | f | +| A.java:29:22:29:28 | taint(...) | A.java:29:22:29:28 | taint(...) | +| A.java:29:22:29:28 | taint(...) | A.java:33:9:33:10 | sb | +| A.java:29:22:29:28 | taint(...) | A.java:33:9:33:21 | toString(...) | +| A.java:29:22:29:28 | taint(...) | A.java:34:9:34:9 | f [post update] | +| A.java:29:22:29:28 | taint(...) | A.java:34:9:34:27 | format(...) | +| A.java:29:22:29:28 | taint(...) | A.java:34:9:34:27 | new ..[] { .. } | +| A.java:29:22:29:28 | taint(...) | A.java:34:24:34:26 | bad | +| A.java:29:22:29:28 | taint(...) | A.java:35:9:35:10 | sb | +| A.java:29:22:29:28 | taint(...) | A.java:35:9:35:21 | toString(...) | +| A.java:39:22:39:28 | taint(...) | A.java:39:22:39:28 | taint(...) | +| A.java:39:22:39:28 | taint(...) | A.java:42:18:42:20 | bad | +| A.java:39:22:39:28 | taint(...) | A.java:43:9:43:46 | new ..[] { .. } | +| A.java:39:22:39:28 | taint(...) | A.java:43:43:43:45 | bad | From ca4781eb78e572fd9e18d8e3bb7c2155d2fd7f37 Mon Sep 17 00:00:00 2001 From: Joe Date: Thu, 1 Oct 2020 15:58:32 +0100 Subject: [PATCH 5/5] Java: Remove use of StringFormatMethod in TaintTrackingUtils --- .../dataflow/internal/TaintTrackingUtil.qll | 21 +++++++------------ 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll b/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll index f9da6342b35..8ce4ca66ec6 100644 --- a/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll +++ b/java/ql/src/semmle/code/java/dataflow/internal/TaintTrackingUtil.qll @@ -13,7 +13,6 @@ private import semmle.code.java.frameworks.spring.SpringHttp private import semmle.code.java.Maps private import semmle.code.java.dataflow.internal.ContainerFlow private import semmle.code.java.frameworks.jackson.JacksonSerializability -private import semmle.code.java.StringFormat /** * Holds if taint can flow from `src` to `sink` in zero or more @@ -391,10 +390,8 @@ private predicate taintPreservingQualifierToMethod(Method m) { ) ) or - m instanceof StringFormatMethod - or m.getDeclaringType() instanceof TypeFormatter and - m.hasName("out") + m.hasName(["format", "out"]) } private class StringReplaceMethod extends Method { @@ -454,10 +451,10 @@ private predicate argToMethodStep(Expr tracked, MethodAccess sink) { */ private predicate taintPreservingArgumentToMethod(Method method) { method.getDeclaringType() instanceof TypeString and - method.hasName("join") + (method.hasName("format") or method.hasName("formatted") or method.hasName("join")) or - method instanceof StringFormatMethod and - not method.getDeclaringType().hasQualifiedName("java.io", "Console") + method.getDeclaringType() instanceof TypeFormatter and + method.hasName("format") } /** @@ -637,9 +634,8 @@ private predicate argToQualifierStep(Expr tracked, Expr sink) { sink = ma.getQualifier() ) or - exists(Method m, MethodAccess ma | - taintPreservingArgumentToQualifier(m) and - ma.getMethod() = m and + exists(MethodAccess ma | + taintPreservingArgumentToQualifier(ma.getMethod()) and tracked = ma.getAnArgument() and sink = ma.getQualifier() ) @@ -649,9 +645,8 @@ private predicate argToQualifierStep(Expr tracked, Expr sink) { * Holds if `method` is a method that transfers taint from any of its arguments to its qualifier. */ private predicate taintPreservingArgumentToQualifier(Method method) { - method instanceof StringFormatMethod and - not method.getDeclaringType() instanceof TypeString and - not method.getDeclaringType().hasQualifiedName("java.io", "Console") + method.getDeclaringType() instanceof TypeFormatter and + method.hasName("format") } /**