From 8e9ed5eb6b658470d2a7b97b84c9a59a8816bd83 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 19 Nov 2015 09:20:31 -0800 Subject: [PATCH] adding model for verifying sockets before reading from them Reviewed By: jeremydubreil Differential Revision: D2665885 fb-gh-sync-id: 4f821ef --- .../facebook/infer/models/InferBuiltins.java | 6 ++ infer/models/java/src/java/lang/Object.java | 3 + infer/models/java/src/java/net/Socket.java | 9 ++- .../java/src/javax/net/SocketFactory.java | 41 +++++++++++ .../src/javax/net/ssl/HostnameVerifier.java | 38 ++++++++++ .../src/javax/net/ssl/SSLSocketFactory.java | 38 ++++++++++ infer/tests/ant_report.json | 15 ++++ infer/tests/buck_report.json | 15 ++++ .../java/infer/TaintExample.java | 69 ++++++++++++++++++- .../tests/endtoend/java/infer/TaintTest.java | 5 +- 10 files changed, 235 insertions(+), 4 deletions(-) create mode 100644 infer/models/java/src/javax/net/SocketFactory.java create mode 100644 infer/models/java/src/javax/net/ssl/HostnameVerifier.java create mode 100644 infer/models/java/src/javax/net/ssl/SSLSocketFactory.java diff --git a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java b/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java index e1f743405..57c509df4 100644 --- a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java +++ b/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java @@ -26,6 +26,12 @@ public class InferBuiltins { __infer_assume(condition); } + // use this instead of "assume o != null". being non-null and allocated are different to Infer + public static void assume_allocated(Object o) { + assume(o != null); + o.hashCode(); + } + public native static String __split_get_nth(String s, String sep, int n); public native static void __set_taint_attribute(Object o); diff --git a/infer/models/java/src/java/lang/Object.java b/infer/models/java/src/java/lang/Object.java index 852209644..01c05dace 100644 --- a/infer/models/java/src/java/lang/Object.java +++ b/infer/models/java/src/java/lang/Object.java @@ -19,4 +19,7 @@ public class Object { return c; } + public int hashCode() { + return InferUndefined.int_undefined(); + } } diff --git a/infer/models/java/src/java/net/Socket.java b/infer/models/java/src/java/net/Socket.java index ac22caaf3..d1af6551e 100644 --- a/infer/models/java/src/java/net/Socket.java +++ b/infer/models/java/src/java/net/Socket.java @@ -13,6 +13,8 @@ import java.io.IOException; import java.io.InputStream; import java.io.OutputStream; +import com.facebook.infer.models.InferBuiltins; + public class Socket { SocketImpl impl; @@ -65,14 +67,17 @@ public class Socket { } public InputStream getInputStream() throws IOException { - return ((PlainSocketImpl) impl).getInputStream(); + InferBuiltins.assume(!InferBuiltins.__state_untainted(this)); + return ((PlainSocketImpl) impl).getInputStream(); } public OutputStream getOutputStream() throws IOException { - return ((PlainSocketImpl) impl).getOutputStream(); + InferBuiltins.assume(!InferBuiltins.__state_untainted(this)); + return ((PlainSocketImpl) impl).getOutputStream(); } public synchronized void close() throws IOException { ((PlainSocketImpl) impl).close(); } + } diff --git a/infer/models/java/src/javax/net/SocketFactory.java b/infer/models/java/src/javax/net/SocketFactory.java new file mode 100644 index 000000000..277a0947a --- /dev/null +++ b/infer/models/java/src/javax/net/SocketFactory.java @@ -0,0 +1,41 @@ +/* +* Copyright (c) 2015 - present Facebook, Inc. +* All rights reserved. +* +* This source code is licensed under the BSD style license found in the +* LICENSE file in the root directory of this source tree. An additional grant +* of patent rights can be found in the PATENTS file in the same directory. +*/ + +package javax.net; + +import java.net.Socket; + +import com.facebook.infer.models.InferBuiltins; + +public class SocketFactory { + + // using recency abstraction to remember the last Socket created + private static Socket sLast; + + public static Socket getLastSocket() { + return sLast; + } + + // proxy for Socket of undefined type + private native Socket genSocket(); + + private Socket returnAllocatedSocket() { + Socket socket = genSocket(); + InferBuiltins.assume_allocated(socket); + sLast = socket; + return socket; + } + + public Socket createSocket() { + Socket socket = returnAllocatedSocket(); + InferBuiltins.__set_taint_attribute(socket); + return socket; + } + +} diff --git a/infer/models/java/src/javax/net/ssl/HostnameVerifier.java b/infer/models/java/src/javax/net/ssl/HostnameVerifier.java new file mode 100644 index 000000000..fb23228f6 --- /dev/null +++ b/infer/models/java/src/javax/net/ssl/HostnameVerifier.java @@ -0,0 +1,38 @@ +/* +* Copyright (c) 2015 - present Facebook, Inc. +* All rights reserved. +* +* This source code is licensed under the BSD style license found in the +* LICENSE file in the root directory of this source tree. An additional grant +* of patent rights can be found in the PATENTS file in the same directory. +*/ + +package javax.net.ssl; + +import java.net.Socket; +import javax.net.SocketFactory; +import javax.net.ssl.SSLSession; + +import com.facebook.infer.models.InferBuiltins; +import com.facebook.infer.models.InferUndefined; + +public class HostnameVerifier { + + public boolean verify( + String hostname, + SSLSession session) { + + Socket socket = SocketFactory.getLastSocket(); + + if (InferUndefined.boolean_undefined()) { + // verification succeeded; we can untaint the socket + InferBuiltins.__set_untaint_attribute(socket); + return true; + } else { + // verification failed; we can't untaint the socket + return false; + } + } + + +} diff --git a/infer/models/java/src/javax/net/ssl/SSLSocketFactory.java b/infer/models/java/src/javax/net/ssl/SSLSocketFactory.java new file mode 100644 index 000000000..eb6235642 --- /dev/null +++ b/infer/models/java/src/javax/net/ssl/SSLSocketFactory.java @@ -0,0 +1,38 @@ +/* +* Copyright (c) 2015 - present Facebook, Inc. +* All rights reserved. +* +* This source code is licensed under the BSD style license found in the +* LICENSE file in the root directory of this source tree. An additional grant +* of patent rights can be found in the PATENTS file in the same directory. +*/ + +package javax.net.ssl; + +import java.io.IOException; +import java.net.InetAddress; +import java.net.Socket; + +import javax.net.SocketFactory; + +import com.facebook.infer.models.InferBuiltins; + +public class SSLSocketFactory extends SocketFactory { + + public Socket createSocket(InetAddress addr, int i) throws IOException { + return super.createSocket(); + } + + public Socket createSocket(InetAddress addr1, int i, InetAddress addr2, int j) throws IOException { + return super.createSocket(); + } + + public Socket createSocket(String s, int i) throws IOException { + return super.createSocket(); + } + + public Socket createSocket(String s, int i, InetAddress addr, int j) throws IOException { + return super.createSocket(); + } + +} diff --git a/infer/tests/ant_report.json b/infer/tests/ant_report.json index 0fdb87867..843692c60 100644 --- a/infer/tests/ant_report.json +++ b/infer/tests/ant_report.json @@ -29,6 +29,21 @@ "file": "codetoanalyze/java/infer/ContextLeaks.java", "bug_type": "CONTEXT_LEAK" }, + { + "procedure": "InputStream TaintExample.socketIgnoreExceptionNoVerify(SSLSocketFactory)", + "file": "codetoanalyze/java/infer/TaintExample.java", + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION" + }, + { + "procedure": "InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory)", + "file": "codetoanalyze/java/infer/TaintExample.java", + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION" + }, + { + "procedure": "InputStream TaintExample.socketVerifiedForgotToCheckRetval(SSLSocketFactory,HostnameVerifier,SSLSession)", + "file": "codetoanalyze/java/infer/TaintExample.java", + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION" + }, { "procedure": "String TaintExample.taintGetAuthorityCompareTo(String)", "file": "codetoanalyze/java/infer/TaintExample.java", diff --git a/infer/tests/buck_report.json b/infer/tests/buck_report.json index 0d874db80..14c5d18d6 100644 --- a/infer/tests/buck_report.json +++ b/infer/tests/buck_report.json @@ -29,6 +29,21 @@ "file": "infer/tests/codetoanalyze/java/infer/ContextLeaks.java", "bug_type": "CONTEXT_LEAK" }, + { + "procedure": "InputStream TaintExample.socketIgnoreExceptionNoVerify(SSLSocketFactory)", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION" + }, + { + "procedure": "InputStream TaintExample.socketNotVerifiedSimple(SSLSocketFactory)", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION" + }, + { + "procedure": "InputStream TaintExample.socketVerifiedForgotToCheckRetval(SSLSocketFactory,HostnameVerifier,SSLSession)", + "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", + "bug_type": "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION" + }, { "procedure": "String TaintExample.taintGetAuthorityCompareTo(String)", "file": "infer/tests/codetoanalyze/java/infer/TaintExample.java", diff --git a/infer/tests/codetoanalyze/java/infer/TaintExample.java b/infer/tests/codetoanalyze/java/infer/TaintExample.java index c6d71a900..4bc333cd7 100644 --- a/infer/tests/codetoanalyze/java/infer/TaintExample.java +++ b/infer/tests/codetoanalyze/java/infer/TaintExample.java @@ -9,10 +9,18 @@ package codetoanalyze.java.infer; - +import java.io.InputStream; +import java.io.IOException; import java.net.MalformedURLException; +import java.net.Socket; import java.net.URL; +import javax.net.ssl.HostnameVerifier; +import javax.net.ssl.SSLException; +import javax.net.ssl.SSLSession; +import javax.net.ssl.SSLSocket; +import javax.net.ssl.SSLSocketFactory; + public class TaintExample { String test_equals(String s) { @@ -253,4 +261,63 @@ public class TaintExample { return res; } + public InputStream socketNotVerifiedSimple(SSLSocketFactory f) + throws IOException { + Socket socket = f.createSocket(); + return socket.getInputStream(); + } + + public InputStream socketVerifiedForgotToCheckRetval(SSLSocketFactory f, + HostnameVerifier v, + SSLSession session) + throws IOException { + + Socket socket = f.createSocket(); + v.verify("hostname", session); + return socket.getInputStream(); + } + + public InputStream socketVerifiedOk1(SSLSocketFactory f, + HostnameVerifier v, + SSLSession session) + throws IOException { + + Socket socket = f.createSocket(); + if (v.verify("hostname", session)) { + return socket.getInputStream(); + } else { + return null; + } + } + + + HostnameVerifier mHostnameVerifier; + + public void throwExceptionIfNoVerify(SSLSocket sslSocket, String host) + throws IOException { + + if (!mHostnameVerifier.verify(host, sslSocket.getSession())) { + throw new SSLException("Couldn't verify!"); + } + } + + public InputStream socketVerifiedOk2(SSLSocketFactory f) throws IOException { + SSLSocket s = (SSLSocket) f.createSocket(); + throwExceptionIfNoVerify(s, "hostname"); + return s.getInputStream(); + } + + public InputStream socketIgnoreExceptionNoVerify(SSLSocketFactory f) + throws IOException { + + SSLSocket s = (SSLSocket) f.createSocket(); + try { + throwExceptionIfNoVerify(s, "hostname"); + } catch (SSLException e) { + // ignore the fact that verifying the socket failed + } + return s.getInputStream(); + } + + } diff --git a/infer/tests/endtoend/java/infer/TaintTest.java b/infer/tests/endtoend/java/infer/TaintTest.java index 34743a4bd..2bdeb2198 100644 --- a/infer/tests/endtoend/java/infer/TaintTest.java +++ b/infer/tests/endtoend/java/infer/TaintTest.java @@ -57,7 +57,10 @@ public class TaintTest { "taintToStringEquals", "taintToStringCompareTo", "taintToStringEndsWith", - "taintToStringStartsWith" + "taintToStringStartsWith", + "socketNotVerifiedSimple", + "socketVerifiedForgotToCheckRetval", + "socketIgnoreExceptionNoVerify" }; assertThat(