Merge pull request diffblue#279 from diffblue/marek/may_alias_to_vsa

SEC-144: Introducing function 'get_may_alias_values'.

Author: marek-trtik

cbmc/src/pointer-analysis/value_set.cpp

@@ -10,6 +10,7 @@
 
 #include <cassert>
 #include <ostream>
+#include <algorithm>
 
 #include <util/symbol_table.h>
 #include <util/simplify_expr.h>

regression/end_to_end/interprocedural01/build.xml

@@ -0,0 +1,29 @@
+<project name="interprocedural01" basedir="." default="jar">
+
+  <property name="root.dir"      value="./"/>
+  <property name="src.dir"       value="${root.dir}/src"/>
+  <property name="classes.dir"   value="${root.dir}/build"/>
+  <property name="install.dir"   value="${root.dir}/dist"/>
+
+  <target name="jar">
+    <antcall target="compile" />
+    <mkdir dir="${install.dir}"/>
+    <jar destfile="${install.dir}/interprocedural01.jar" basedir="${classes.dir}" />
+  </target>  
+  
+  <target name="compile">
+    <antcall target="clean" />
+    <mkdir dir="${classes.dir}"/>
+    <javac srcdir="${src.dir}" destdir="${classes.dir}" includeantruntime="false" debug="on">
+    </javac>
+  </target>
+
+  <target name="clean">
+    <delete dir="${classes.dir}"/>
+    <delete dir="${install.dir}"/>
+  </target>
+
+
+</project>
+
+

regression/end_to_end/interprocedural01/rules.json

@@ -0,0 +1,62 @@
+{
+  "namespace": "com.diffblue.security",
+  "rules":
+    [
+      {
+        "comment": "Obtaining a stream with potentially tainted data.",
+        "class": "Main",
+        "method": "getInStream:()LIStream;",
+        "result": {
+          "location": "returns",
+          "taint": "Tainted stream"
+        }
+      },
+      {
+        "comment": "Obtaining a vulnerable stream",
+        "class": "Main",
+        "method": "getOutStream:()LOStream;",
+        "result": {
+          "location": "returns",
+          "vulnerability": "Vulnerable stream"
+        }
+      },
+      {
+        "comment": "Read from tainted stream gives tainted string",
+        "class": "IStream",
+        "method": "read:(LData;)V",
+        "input": {
+          "location": "this",
+          "taint": "Tainted stream"
+        },
+        "result": {
+          "location": "arg1",
+          "taint": "Tainted data"
+        }
+      },
+      {
+        "comment": "Writing potentially tainted data to a vulnerable stream.",
+        "class": "OStream",
+        "method": "write:(LData;)V",
+        "input": {
+          "location": "arg1",
+          "taint": "Tainted data"
+        },
+        "sinkTarget": {
+          "location": "this",
+          "vulnerability": "Vulnerable stream"
+        },
+        "message": "Writing potentially tainted data to a vulnerable stream."
+      },
+      {
+        "comment": "Sanitise tainted data.",
+        "class": "Main",
+        "method": "sanitise:(LData;)V",
+        "sanitizes": {
+          "location": "arg0",
+          "taint": "Tainted data"
+        }
+      }
+    ]
+}
+
+

regression/end_to_end/interprocedural01/src/Main.java

@@ -0,0 +1,59 @@
+class Data {
+}
+
+class IStream {
+    public void read(Data d) {
+    }
+}
+
+class OStream {
+    public void write(Data d) {
+    }
+}
+
+public class Main {
+
+    public static IStream getInStream() {
+        return new IStream();
+    }
+
+    public static OStream getOutStream() {
+        return new OStream();
+    }
+    
+    public static Data getData1() {
+        return new Data();
+    }
+    
+    public static Data getData2() {
+        return new Data();
+    }
+    
+    private static void getBytes(Data data, IStream in) {
+        Data alias = data;
+        in.read(alias);
+    }
+
+    private static void postBytes(Data data, OStream out) {
+        out.write(data);
+    }
+
+    public static void sanitise(Data d) {
+    }
+
+    public static void main() {
+        IStream in = getInStream();
+        OStream out = getOutStream();
+        Data d = getData1();
+        Data e = getData2();
+        Data q = d;
+        getBytes(d, in);
+        getBytes(e, in);
+        sanitise(q);
+        postBytes(d, out);
+        postBytes(q, out);
+        postBytes(e, out);
+    }
+
+}
+

regression/end_to_end/interprocedural01/test_interprocedural01.py

@@ -0,0 +1,23 @@
+import regression.end_to_end.driver as pipeline_executor
+import os
+import subprocess
+
+
+def test_interprocedural01():
+    with pipeline_executor.working_dir(os.path.abspath(os.path.dirname(__file__))):
+        subprocess.call("ant")
+    traces = pipeline_executor.run_security_analyser_pipeline(
+        os.path.join("dist", "interprocedural01.jar"),
+        "rules.json",
+        os.path.realpath(os.path.dirname(__file__)))
+    assert traces.count_traces() == 1
+    assert traces.trace_exists("java::Main.postBytes:(LData;LOStream;)V", 38)
+    assert traces.trace_goes_through(
+        "jbmc",
+        -2,
+        "java::Main.main:()V",
+        55,
+        "java::Main.postBytes:(LData;LOStream;)V",
+        38
+        )
+

src/pointer-analysis/external_value_set_expr.h

@@ -287,4 +287,10 @@ inline const external_value_set_exprt &to_external_value_set(const exprt &e)
   return static_cast<const external_value_set_exprt &>(e);
 }
 
+template<>
+inline bool can_cast_expr<external_value_set_exprt >(const exprt &base)
+{
+  return base.id()==ID_external_value_set;
+}
+
 #endif

src/pointer-analysis/local_value_set.cpp

@@ -8,6 +8,7 @@
 #include <util/simplify_expr_class.h>
 #include <util/infix.h>
 #include <util/suffix.h>
+#include <util/c_types.h>
 
 #include <pointer-analysis/dynamic_object_name.h>
 
@@ -76,6 +77,67 @@ void local_value_sett::get_value_set(
   baset::get_value_set(tmp, dest, ns, true);
 }
 
+/// Builds a version of expr suitable for alias-comparison
+/// \param expr: The expression to be converted to the alias-uniform structure
+/// \return expr without information which is irrelevant to alias-comparison
+static exprt get_uniform_expr(const exprt &expr)
+{
+  if(const auto desc_ptr=expr_try_dynamic_cast<object_descriptor_exprt>(expr))
+  {
+    object_descriptor_exprt ob;
+    ob.object() = get_uniform_expr(desc_ptr->object());
+    ob.offset() = desc_ptr->offset();
+    return ob;
+  }
+  if(can_cast_expr<external_value_set_exprt>(expr))
+  {
+    exprt copy = expr;
+    copy.set(ID_is_initializer, ID_0);
+    return copy;
+  }
+  return expr;
+}
+
+/// Reconstructs a type of a pointer to the object expr
+/// \param expr: An object in a points-to set we make an alias type for
+/// \return A type of a pointer to the object expr
+static typet get_alias_type(const exprt &expr)
+{
+  if(expr.id()==ID_object_descriptor)
+  {
+    object_descriptor_exprt ob_expr=to_object_descriptor_expr(expr);
+    if(ob_expr.offset().id()==ID_invalid || ob_expr.offset().id()==ID_unknown)
+      return pointer_type(ob_expr.object().type());
+  }
+  return pointer_type(expr.type());
+}
+
+void local_value_sett::get_may_alias_set(
+  const exprt &expr,
+  value_setst::valuest &dest,
+  const namespacet &ns) const
+{
+  object_mapt pointed_objects;
+  get_value_set(expr, pointed_objects, ns, false);
+  std::vector<exprt> uniform_pointed_objects;
+  for(const auto &num_obj : pointed_objects.read())
+    uniform_pointed_objects.push_back(get_uniform_expr(to_expr(num_obj)));
+
+  for(const auto &name_entry : values)
+    for(const auto &enum_eobj : name_entry.second.object_map.read())
+    {
+      if(std::find(uniform_pointed_objects.cbegin(),
+                   uniform_pointed_objects.cend(),
+                   get_uniform_expr(to_expr(enum_eobj)))!=
+         uniform_pointed_objects.cend())
+      {
+        dest.push_back(symbol_exprt(
+          name_entry.second.identifier,
+          get_alias_type(to_expr(enum_eobj))));
+      }
+    }
+}
+
 /// Value-set analysis accrues a `suffix` as it walks down an expression tree--
 /// for example, it transforms a `get_value_set_rec(x.y.z)` into
 /// `get_value_set_rec(x, suffix = "y.z")`. This function recovers the type

src/pointer-analysis/local_value_set.h

@@ -58,6 +58,15 @@ class local_value_sett:public value_sett
     const namespacet &ns,
     bool is_simplified) const override;
 
+  /// Computes all pointers which MAY point to objects pointed to by expr
+  /// \param expr: Identifies a points-to set for which to compute aliases
+  /// \param dest: Output container for pointers to objects pointed to by expr
+  /// \param ns: A reference to a symbol table
+  void get_may_alias_set(
+    const exprt &expr,
+    value_setst::valuest &dest,
+    const namespacet &ns) const;
+
   /// Overrides `value_sett::assign` to (a) tag all external-value-set
   /// expressions from `rhs` indicating they have been assigned, and (b)
   /// apply side-effects of this assignment to the whole domain, which currently

src/pointer-analysis/local_value_set_analysis.h

@@ -186,7 +186,22 @@ class local_value_set_analysist
   /// Counts summary assignment steps performed in `transform_function_stub`
   size_t nstub_assignments;
 
- protected:
+  /// Fills in dest with all pointers to any object pointed to be expr
+  /// \param l: A program location w.r.t which the operation will be performed
+  /// \param expr: Identifies a points-to set whose aliases we will compute
+  /// \param dest: Output container for aliases
+  void get_may_alias_values(
+    locationt l,
+    const exprt &expr,
+    value_setst::valuest &dest)
+  {
+    ((const local_value_sett&)(*this)[l].value_set).get_may_alias_set(
+      expr,
+      dest,
+      baset::ns);
+  }
+
+protected:
   /// Type of function under analysis
   const code_typet& function_type;
   /// Name of function under analysis

src/taint-analysis/taint_summary.cpp

@@ -237,6 +237,27 @@ static void collect_lvsa_access_paths(
     result.insert(taint_object_numbering.number(object));
 }
 
+/// Invokes LVSA for the aliases and converts them to numbers
+/// \param query_in: Identifies a points to set (e.g. a pointer to some object)
+/// \param ns: A symbol table (for internal use in LVSA)
+/// \param lvsa: The LVSA analysis
+/// \param inst_it: A program location w.r.t which the operation will be performed
+/// \param taint_object_numbering: For conversion of aliases to numbers
+/// \param result: The output container for numbers of computed aliases
+static void collect_lvsa_alias_access_paths(
+  exprt const& query_in,
+  namespacet const& ns,
+  local_value_set_analysist& lvsa,
+  instruction_iteratort const& inst_it,
+  object_numberingt& taint_object_numbering,
+  lvalue_numbers_sett& result)
+{
+  value_setst::valuest dest;
+  lvsa.get_may_alias_values(inst_it, query_in, dest);
+  for(const exprt &object : dest)
+    result.insert(taint_object_numbering.number(object));
+}
+
 static void collect_lvsa_access_paths(
   exprt const& querye_in,
   namespacet const& ns,
@@ -555,9 +576,25 @@ void taint_algorithm_computing_summary_of_functiont::
         lvsa,
         Iit,
         *numbering);
+      collect_lvsa_alias_access_paths(
+        fn_call.arguments().at(param_idx),
+        program->get_namespace(),
+        lvsa,
+        Iit,
+        *numbering,
+        argument_lvalues);
     }
     else
+    {
       argument_lvalues.insert(lvalue_taint.first);
+      collect_lvsa_alias_access_paths(
+        lvalue,
+        program->get_namespace(),
+        lvsa,
+        Iit,
+        *numbering,
+        argument_lvalues);
+    }
 
     const object_numbers_by_field_per_functiont &object_numbers_by_field =
       numbering_map->get_object_numbers_by_field();
@@ -920,12 +957,20 @@ void taint_algorithm_computing_summary_of_functiont::
     *numbering,
     numbers_of_aliases,
     singular);
+  collect_lvsa_alias_access_paths(
+    lvalue,
+    program->get_namespace(),
+    lvsa,
+    Iit,
+    *numbering,
+    numbers_of_aliases);
 
   if(singular && is_allowed_pure_assignment)
   {
     // Singular implies that lhs has exactly one element,
     // so we can access it directly
-    assign(result, *numbers_of_aliases.begin(), taint_from_rule);
+    for(const auto num : numbers_of_aliases)
+      assign(result, num, taint_from_rule);
   }
   else
   {