Checker Injection   as of Julia version 2.4 (built on 23 Oct 2017)

belongs to group Advanced

Identify potential security injections


The most dangerous software errors are due to the injection of user data into sensitive routines, such as database queries, html output to the client or file system access. These attacks are generally known as injection attacks and there is large literature about the risk that they pose to software exposed to uncontrolled user input. The list available at cwe.mitre.org reports explicit examples of such security issues, for instance SQL-injection, OS-command injection, cross-site scripting and open redirect. The unifying aspect of these errors is that user input can flow, unconstrained, into sensitive routines. Hence Julia provides this checker in order to track explicit information flow in the program, from automatically or manually selected source locations into automatically or manually selected sink locations. In this way, Julia allows one to identify potential security errors of the above categories, with a soundness guarantee derived from the use of abstract interpretation, and with the freedom to bend the analysis to specific needs, through the use of code annotations.

Action: Verify that a security error actually corresponds to unconstrained information flow from source locations into sink locations. If this is the case, add a sanitizing algorithm to clean data before it flows into sinks, or use prepared statements for SQL queries rather than free queries built from string concatenation.

Specification of source locations

Normally, you needn't specify any source location, since Julia will recognize the most frequent locations automatically (see the list of sources natively recognized by Julia). For special experiments or for frameworks not recognized by Julia, please use the following code annotations.

Julia has a built-in mechanism that identifies standard source locations from where user input can be provided to a program. These belong to the following five classes:

  • Request objects to servlets and input read from console are considered as source locations of untrusted data. The programmer can specify further method parameters as source locations of this class, through the @UntrustedUserInput annotation. This class is turned off if the trustUserInput option is flagged
  • Input streams from sockets or URL are considered as source locations of untrusted data. The programmer can specify further method parameters as source locations of this class, through the @UntrustedExternalStream annotation. This class is turned off if the trustExternalStreams option is flagged
  • Files from the file system, system properties and arguments to main methods are considered as source locations of untrusted data. The programmer can specify further method parameters as source locations of this class, through the @UntrustedEnvironment annotation. This class is turned off if the trustEnvironment option is flagged
  • The results of database queries are considered as source locations of untrusted data. The programmer can specify further method parameters as source locations of this class, through the @UntrustedDatabase annotation. This class is turned off if the trustDatabase option is flagged
  • Data about the specific device where the program is running, such as its phone number, its geographical location and its IMEI code, is considered as untrusted. The programmer can specify further method parameters as source locations of this class, through the @UntrustedDevice annotation. This class is turned off if the trustDevice option is flagged


Specification of sink locations

Normally, you needn't specify any sink location, since Julia will recognize the most frequent locations automatically. (see the list of sinks natively recognized by Julia). For special experiments or for frameworks not recognized by Julia, please use the following code annotations.

Julia has a built-in specification of sink locations where untrusted data should not flow into. These include:

  • Parameters passed to SQL database query methods. If untrusted data flows here, an SQL-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @SqlTrusted annotation
  • Parameters passed to IP address factory methods such as Inet6Address.getByAddress(). If untrusted data flows here, an address-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @AddressTrusted annotation
  • Parameters passed to value/attribute manipulation methods of servlet session objects. If untrusted data flows here, a session-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @SessionTrusted annotation
  • Parameters passed to constructors, bind and connect methods of sockets. If untrusted data flows here, a resource-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @ResourceTrusted annotation
  • Parameters passed to reflection methods. If untrusted data flows here, a reflection-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @ReflectionTrusted annotation
  • Parameters passed as names to file or file stream constructors. If untrusted data flows here, a path-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @PathTrusted annotation
  • Parameters passed to logging functions. If untrusted data flows here, a log-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @LogTrusted annotation
  • Parameters passed to the output stream of servlets. If untrusted data flows here, a cross-site-scripting-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @CrossSiteTrusted annotation
  • Parameters passed to the http response object of servlets. If untrusted data flows here, an http-response-injection warning is reported. This encompasses open redirection attacks. The programmer can specify extra locations of this class where untrusted data should not flow, through the @HttpResponseTrusted annotation
  • Parameters passed to the xpath compilation and evaluation methods. If untrusted data flows here, an xpath-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @XPathTrusted annotation
  • Parameters passed as addresses to URL constructors or to Class.getResource(). If untrusted data flows here, a resource-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @UrlTrusted annotation
  • Parameters passed to methods that might induce an indefinite wait and consequently a denial-of service, such as Thread.sleep(). If untrusted data flows here, a denial-of-service-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @DenialTrusted annotation
  • Parameters passed as filters to javax.naming.directory.DirContext methods, that might induce unconstrained listing of files. If untrusted data flows here, a filter-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @FilterTrusted annotation
  • Parameters passed as values of javax.naming.directory.BasicAttribute's. If untrusted data flows here, an attribute-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @AttributeTrusted annotation
  • Parameters passed to selected methods of javax.script.ScriptEngine objects. If untrusted data flows here, a code-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @CodeTrusted annotation
  • Parameters passed to command or process execution methods. If untrusted data flows here, an OS-command-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @CommandTrusted annotation
  • Parameters passed as names of native libraries loaded at runtime. If untrusted data flows here, a control-injection warning is reported. The programmer can specify extra locations of this class where untrusted data should not flow, through the @ControlTrusted annotation
The programmer can also specify a generic location where untrusted data should not flow, through the @Trusted annotation.


Examples


Consider the following program:

import java.io.IOException;
import java.io.PrintWriter;
import java.sql.Connection;
import java.sql.DriverManager;
import java.sql.ResultSet;
import java.sql.SQLException;
import java.sql.Statement;
import javax.servlet.http.HttpServlet;
import javax.servlet.http.HttpServletRequest;
import javax.servlet.http.HttpServletResponse;

import com.juliasoft.julia.checkers.flows.UntrustedUserInput;
import com.juliasoft.julia.checkers.injection.SqlTrusted;
import com.juliasoft.julia.checkers.injection.Trusted;
import com.juliasoft.julia.extraction.EntryPoint;

public class SqlInjection extends HttpServlet {
  private @SqlTrusted Object sqlTrusted;
  private @Trusted Object trusted;

  @Override
  protected final void doGet(HttpServletRequest request, HttpServletResponse response) throws IOException {
    processRequest(request, response);
  }

  @Override
  protected final void doPost(HttpServletRequest request, HttpServletResponse response) throws IOException {
    processRequest(request, response);
  }

  public @EntryPoint void test1(@UntrustedUserInput String user) {
    Connection conn = null;
    String url = "jdbc:mysql://192.168.2.128:3306/";
    String dbName = "anvayaV2";
    String driver = "com.mysql.jdbc.Driver";
    String userName = "root";
    String password = "";
    // with the following assignment, there is no injection anymore at line 48
    // user = "erasmus";

    try {
      Class.forName(driver).newInstance();
      conn = DriverManager.getConnection(url + dbName, userName, password);

      Statement st = conn.createStatement();
      String query = "SELECT * FROM  User where userId='" + user + "'";
      System.out.printf(query);
      st.executeQuery(query);

      // Julia does not like these
      test2(query + " extra characters");
      test3(query + " hello");

      // while Julia likes this!
      test2("driver".substring(3, 5));

      conn.close();
    } catch (Exception e) {
      e.printStackTrace();
    }
  }

  private void test2(@SqlTrusted String s) {
  }

  private void test3(@Trusted String s) {
  }

  private void processRequest(HttpServletRequest request, HttpServletResponse response) throws IOException {
    response.setContentType("text/html;charset=UTF-8");

    String user = request.getParameter("user");
    String url = "jdbc:mysql://192.168.2.128:3306/";
    String dbName = "anvayaV2";
    String driver = "com.mysql.jdbc.Driver";
    String userName = "root";
    String password = "";

    try {
      Class.forName(driver).newInstance();
    }
    catch (InstantiationException | IllegalAccessException | ClassNotFoundException e) {
      return;
    }

    try (Connection conn = DriverManager.getConnection(url + dbName, userName, password);
         PrintWriter out = response.getWriter()) {

      Statement st = conn.createStatement();
      String query = "SELECT * FROM  User where userId='" + user + "'";
      out.println("Query : " + query);
      System.out.printf(query);
      ResultSet res = st.executeQuery(query);
      trusted = query.substring(5, 7);
      sqlTrusted = query;

      out.println("Results");
      while (res.next()) {
        String s = res.getString("address");
        out.println("\t\t" + s);
      }
    }
    catch (SQLException e) {}
  }
}

This checker issues the following warnings:

SqlInjection.java:48: [Injection: SqlInjectionWarning] possible SQL-injection through the 0th actual parameter of executeQuery
SqlInjection.java:51: [Injection: SqlInjectionWarning] possible SQL-injection through the 0th actual parameter of test2
SqlInjection.java:52: [Injection: GenericInjectionWarning] possible injection of tainted data through the 0th actual parameter of test3
SqlInjection.java:91: [Injection: XSSInjectionWarning] possible XSS-injection through the 0th actual parameter of println
SqlInjection.java:93: [Injection: SqlInjectionWarning] possible SQL-injection through the 0th actual parameter of executeQuery
SqlInjection.java:94: [Injection: GenericInjectionIntoFieldWarning] possible injection of tainted data into field trusted
SqlInjection.java:95: [Injection: SqlInjectionIntoFieldWarning] possible SQL-injection into field sqlTrusted
SqlInjection.java:100: [Injection: XSSInjectionWarning] possible XSS-injection through the 0th actual parameter of println

Let us discuss the motivation of such warnings. At lines 48 and 93, the query to the database is partially built from user input passed as a parameter to the servlet. Hence there might be an SQL-injection there. At line 51, user input is passed to test2(), which requires its parameter to be @SqlTrusted instead. Hence Julia issues a warning there. The situation at line 53 is similar, but for the kind of annotation, which is @Trusted for the parameter of test3(). At line 91, user input is sent to the servlet output stream and might hence allow a cross-site scripting attack. At lines 94 and 95, data built from user input is written into fields annotated as @Trusted and @SqlTrusted, respectively. Hence, Julia issues a warning there. At line 100, data derived from the result of a database query is sent to the output stream of the servlet. Julia issues a cross-site scripting warning there since the query depends from user input and hence its result as well.

In this example, the programmer should avoid a direct flow of user input into database queries or into the output stream of the servlet. The solution is to use a sanitizing method that guarantees the correct handling of user input, so that it becomes harmless (see the list of sanitizing methods natively recognized by Julia), or to use prepared statements for database queries, or to implement proprietary sanitizing methods. For an example of the last case, the query might be passed through a sanitizing method such as query = clean(query) just after line 50, where:

private @Trusted String clean(String query) {
  return ...sanitized query
}

The @Trusted annotation is needed here to suggest to Julia the fact that this is a sanitizing method, whose result is always trusted. Julia is not able to infer such complex property by itself.

As for all checkers, you can turn off warnings of this checker with the SuppressJuliaWarnings annotation. Moreover, you can turn off specific warnings by asserting that specific variables are clean at a given program point. For instance, if you want to state that a given variable var is clean, add the following to your code:

var = com.juliasoft.julia.checkers.injection.assertions.InjectionAssertions.clean(var);

After that call, variable var will be assumed to contain no secret data, until another assignment of side effect that might affect it.