adding model for verifying sockets before reading from them

Reviewed By: jeremydubreil

Differential Revision: D2665885

fb-gh-sync-id: 4f821ef

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);

infer/models/java/src/java/lang/Object.java

@@ -19,4 +19,7 @@ public class Object {
         return c;
     }
 
+    public int hashCode() {
+      return InferUndefined.int_undefined();
+    }
 }

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();
     }
+
 }

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;
+  }
+
+}

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;
+    }
+  }
+
+
+}

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();
+  }
+
+}

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",

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",

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();
+  }
+
+
 }

infer/tests/endtoend/java/infer/TaintTest.java

@@ -57,7 +57,10 @@ public class TaintTest {
         "taintToStringEquals",
         "taintToStringCompareTo",
         "taintToStringEndsWith",
-        "taintToStringStartsWith"
+        "taintToStringStartsWith",
+        "socketNotVerifiedSimple",
+        "socketVerifiedForgotToCheckRetval",
+        "socketIgnoreExceptionNoVerify"
     };
 
     assertThat(