Merge pull request diffblue#459 from diffblue/owen-jones-diffblue/gin…

…co-rules SEC-467: Ginco rules
NathanJPhillips · Jun 22, 2018 · 3097fa8 · 3097fa8
2 parents 51b6c8c + bd088e8
commit 3097fa8
Show file tree

Hide file tree

Showing 3 changed files with 147 additions and 8 deletions.
diff --git a/benchmarks/GENUINE/GincoRules.json b/benchmarks/GENUINE/GincoRules.json
@@ -3,15 +3,150 @@
   "rules":
   [
     {
-      "comment": "Get on a tainted map returns a tainted object",
+      "comment": "Incoming MultipartBody is potentially dangerous.",
+      "class": "Main",
+      "method": "makeTainted:(Lorg/apache/cxf/jaxrs/ext/multipart/MultipartBody;)V",
+      "result": {
+        "location": "arg0",
+        "taint": "Tainted MultipartBody"
+      }
+    },
+    {
+      "comment": "Obtained MultipartBody's tainted Attachment.",
+      "class": "org.apache.cxf.jaxrs.ext.multipart.MultipartBody",
+      "method": "getAttachment:(Ljava/lang/String;)Lorg/apache/cxf/jaxrs/ext/multipart/Attachment;",
+      "input": {
+        "location": "this",
+        "taint": "Tainted MultipartBody"
+      },
+      "result": {
+        "location": "returns",
+        "taint": "Tainted Attachment"
+      }
+    },
+    {
+      "comment": "Obtained Attachment's tainted String",
+      "class": "org.apache.cxf.jaxrs.ext.multipart.Attachment",
+      "method": "getObject:(Ljava/lang/Class;)Ljava/lang/Object;",
+      "input": {
+          "location": "this",
+          "taint": "Tainted Attachment"
+        },
+      "result": {
+        "location": "returns",
+        "taint": "Tainted String"
+      }
+    },
+    {
+      "comment": "Obtained tainted Map from tainted content String",
+      "class": "fr.mcc.ginco.imports.ISKOSImportService",
+      "method": "importSKOSFile:(Ljava/lang/String;Ljava/lang/String;Ljava/io/File;)Ljava/util/Map;",
+      "input": {
+          "location": "arg1",
+          "taint": "Tainted String"
+        },
+      "result": {
+        "location": "returns",
+        "taint": "Tainted Map"
+      }
+    },
+    {
+      "comment": "Obtained tainted Set from tainted Map",
       "class": "java.util.Map",
-      "method": "get:(Ljava/lang/Object;)Ljava/lang/Object;",
+      "method": "keySet:()Ljava/util/Set;",
+      "input": {
+        "location": "this",
+        "taint": "Tainted Map"
+      },
+      "result": {
+        "location": "returns",
+        "taint": "Tainted Set"
+      }
+    },
+    {
+      "comment": "Obtained tainted Iterator from tainted Set",
+      "class": "java.util.Set",
+      "method": "iterator:()Ljava/util/Iterator;",
       "input": {
         "location": "this",
-        "taint": "Tainted Parameter Map"
+        "taint": "Tainted Set"
       },
       "result": {
         "location": "returns",
+        "taint": "Tainted Iterator"
+      }
+    },
+    {
+      "comment": "Obtained tainted Object from tainted Iterator",
+      "class": "java.util.Iterator",
+      "method": "next:()Ljava/util/Object;",
+      "input": {
+        "location": "this",
+        "taint": "Tainted Iterator"
+      },
+      "result": {
+        "location": "returns",
+        "taint": "Tainted Thesaurus"
+      }
+    },
+    {
+      "comment": "Obtained tainted String from tainted Thesaurus",
+      "class": "fr.mcc.ginco.beans.Thesaurus",
+      "method": "getTitle:()Ljava/lang/String;()",
+      "input": {
+        "location": "this",
+        "taint": "Tainted Thesaurus"
+      },
+      "result": {
+        "location": "returns",
+        "taint": "Tainted String"
+      }
+    },
+    {
+      "comment": "Setting title to tainted String gives tainted ImportedThesaurusResponse",
+      "class": "fr.mcc.ginco.extjs.view.ImportedThesaurusResponse",
+      "method": "setThesaurusTitle:(Ljava/lang/String;)V",
+      "input": {
+        "location": "arg1",
+        "taint": "Tainted String"
+      },
+      "result": {
+        "location": "this",
+        "taint": "Tainted ImportedThesaurusResponse"
+      }
+    },
+    {
+      "comment": "Initialize tainted ExtJsonFormLoadData from tainted ImportedThesaurusResponse",
+      "class": "fr.mcc.ginco.extjs.view.ExtJsonFormLoadData",
+      "method": "<init>:(Ljava/lang/Object;)V",
+      "input": {
+        "location": "arg1",
+        "taint": "Tainted ImportedThesaurusResponse"
+      },
+      "result": {
+        "location": "this",
+        "taint": "Tainted ExtJsonFormLoadData"
+      }
+    },
+    {
+      "comment": "Turn tainted ExtJsonFormLoadData into tainted String",
+      "class": "org.codehaus.jackson.map.ObjectMapper",
+      "method": "writeValueAsString:(Ljava/lang/Object;)Ljava/lang/String;",
+      "input": {
+        "location": "arg1",
+        "taint": "Tainted ExtJsonFormLoadData"
+      },
+      "result": {
+        "location": "returns",
+        "taint": "Tainted String"
+      }
+    },
+    {
+      "comment": "ARTIFICIAL sink to capture servlet returning tainted String.",
+      "class": "Main",
+      "method": "sink:(Ljava/lang/String;)V",
+      "sinkTarget": {
+        "location": "arg0",
         "taint": "Tainted String"
       }
     }

diff --git a/benchmarks/GENUINE/Ginco_files/__MAIN__/src/main/java/Main.java b/benchmarks/GENUINE/Ginco_files/__MAIN__/src/main/java/Main.java
@@ -5,13 +5,17 @@
 
 public class Main {
 
+    static void makeTainted(MultipartBody x) {
+    }
+
     static void sink(String s) {
     }
 
     public static void main(String[] args) {
-        MultipartBody arg0 = CProver.nondetWithNull();
-        HttpServletRequest arg1 = CProver.nondetWithNull();
-        ImportRestService obj = CProver.nondetWithNull();
+        MultipartBody arg0 = CProver.nondetWithNull((MultipartBody)null);
+        makeTainted(arg0);
+        HttpServletRequest arg1 = CProver.nondetWithNull((HttpServletRequest)null);
+        ImportRestService obj = CProver.nondetWithNull((ImportRestService)null);
         try {
             sink(obj.uploadFile(arg0, arg1));
         }

diff --git a/src/driver/sec_driver_parse_options.cpp b/src/driver/sec_driver_parse_options.cpp
@@ -215,12 +215,12 @@ int sec_driver_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
-  if (cmdline.isset("do-not-use-precise-access-paths"))
+  if(cmdline.isset("do-not-use-precise-access-paths"))
   {
     local_value_sett::do_not_use_precise_access_paths = true;
   }
 
-  if (cmdline.isset("security-scanner"))
+  if(cmdline.isset("security-scanner"))
   {
     try
     {