Skip to content

Commit 3097fa8

Browse files
author
owen-jones-diffblue
authored
Merge pull request diffblue#459 from diffblue/owen-jones-diffblue/ginco-rules
SEC-467: Ginco rules
2 parents 51b6c8c + bd088e8 commit 3097fa8

File tree

3 files changed

+147
-8
lines changed

3 files changed

+147
-8
lines changed

‎benchmarks/GENUINE/GincoRules.json

+138-3
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,150 @@
33
"rules":
44
[
55
{
6-
"comment": "Get on a tainted map returns a tainted object",
6+
"comment": "Incoming MultipartBody is potentially dangerous.",
7+
"class": "Main",
8+
"method": "makeTainted:(Lorg/apache/cxf/jaxrs/ext/multipart/MultipartBody;)V",
9+
"result": {
10+
"location": "arg0",
11+
"taint": "Tainted MultipartBody"
12+
}
13+
},
14+
{
15+
"comment": "Obtained MultipartBody's tainted Attachment.",
16+
"class": "org.apache.cxf.jaxrs.ext.multipart.MultipartBody",
17+
"method": "getAttachment:(Ljava/lang/String;)Lorg/apache/cxf/jaxrs/ext/multipart/Attachment;",
18+
"input": {
19+
"location": "this",
20+
"taint": "Tainted MultipartBody"
21+
},
22+
"result": {
23+
"location": "returns",
24+
"taint": "Tainted Attachment"
25+
}
26+
},
27+
{
28+
"comment": "Obtained Attachment's tainted String",
29+
"class": "org.apache.cxf.jaxrs.ext.multipart.Attachment",
30+
"method": "getObject:(Ljava/lang/Class;)Ljava/lang/Object;",
31+
"input": {
32+
"location": "this",
33+
"taint": "Tainted Attachment"
34+
},
35+
"result": {
36+
"location": "returns",
37+
"taint": "Tainted String"
38+
}
39+
},
40+
{
41+
"comment": "Obtained tainted Map from tainted content String",
42+
"class": "fr.mcc.ginco.imports.ISKOSImportService",
43+
"method": "importSKOSFile:(Ljava/lang/String;Ljava/lang/String;Ljava/io/File;)Ljava/util/Map;",
44+
"input": {
45+
"location": "arg1",
46+
"taint": "Tainted String"
47+
},
48+
"result": {
49+
"location": "returns",
50+
"taint": "Tainted Map"
51+
}
52+
},
53+
{
54+
"comment": "Obtained tainted Set from tainted Map",
755
"class": "java.util.Map",
8-
"method": "get:(Ljava/lang/Object;)Ljava/lang/Object;",
56+
"method": "keySet:()Ljava/util/Set;",
57+
"input": {
58+
"location": "this",
59+
"taint": "Tainted Map"
60+
},
61+
"result": {
62+
"location": "returns",
63+
"taint": "Tainted Set"
64+
}
65+
},
66+
{
67+
"comment": "Obtained tainted Iterator from tainted Set",
68+
"class": "java.util.Set",
69+
"method": "iterator:()Ljava/util/Iterator;",
970
"input": {
1071
"location": "this",
11-
"taint": "Tainted Parameter Map"
72+
"taint": "Tainted Set"
1273
},
1374
"result": {
1475
"location": "returns",
76+
"taint": "Tainted Iterator"
77+
}
78+
},
79+
{
80+
"comment": "Obtained tainted Object from tainted Iterator",
81+
"class": "java.util.Iterator",
82+
"method": "next:()Ljava/util/Object;",
83+
"input": {
84+
"location": "this",
85+
"taint": "Tainted Iterator"
86+
},
87+
"result": {
88+
"location": "returns",
89+
"taint": "Tainted Thesaurus"
90+
}
91+
},
92+
{
93+
"comment": "Obtained tainted String from tainted Thesaurus",
94+
"class": "fr.mcc.ginco.beans.Thesaurus",
95+
"method": "getTitle:()Ljava/lang/String;()",
96+
"input": {
97+
"location": "this",
98+
"taint": "Tainted Thesaurus"
99+
},
100+
"result": {
101+
"location": "returns",
102+
"taint": "Tainted String"
103+
}
104+
},
105+
{
106+
"comment": "Setting title to tainted String gives tainted ImportedThesaurusResponse",
107+
"class": "fr.mcc.ginco.extjs.view.ImportedThesaurusResponse",
108+
"method": "setThesaurusTitle:(Ljava/lang/String;)V",
109+
"input": {
110+
"location": "arg1",
111+
"taint": "Tainted String"
112+
},
113+
"result": {
114+
"location": "this",
115+
"taint": "Tainted ImportedThesaurusResponse"
116+
}
117+
},
118+
{
119+
"comment": "Initialize tainted ExtJsonFormLoadData from tainted ImportedThesaurusResponse",
120+
"class": "fr.mcc.ginco.extjs.view.ExtJsonFormLoadData",
121+
"method": "<init>:(Ljava/lang/Object;)V",
122+
"input": {
123+
"location": "arg1",
124+
"taint": "Tainted ImportedThesaurusResponse"
125+
},
126+
"result": {
127+
"location": "this",
128+
"taint": "Tainted ExtJsonFormLoadData"
129+
}
130+
},
131+
{
132+
"comment": "Turn tainted ExtJsonFormLoadData into tainted String",
133+
"class": "org.codehaus.jackson.map.ObjectMapper",
134+
"method": "writeValueAsString:(Ljava/lang/Object;)Ljava/lang/String;",
135+
"input": {
136+
"location": "arg1",
137+
"taint": "Tainted ExtJsonFormLoadData"
138+
},
139+
"result": {
140+
"location": "returns",
141+
"taint": "Tainted String"
142+
}
143+
},
144+
{
145+
"comment": "ARTIFICIAL sink to capture servlet returning tainted String.",
146+
"class": "Main",
147+
"method": "sink:(Ljava/lang/String;)V",
148+
"sinkTarget": {
149+
"location": "arg0",
15150
"taint": "Tainted String"
16151
}
17152
}

‎benchmarks/GENUINE/Ginco_files/__MAIN__/src/main/java/Main.java

+7-3
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,17 @@
55

66
public class Main {
77

8+
static void makeTainted(MultipartBody x) {
9+
}
10+
811
static void sink(String s) {
912
}
1013

1114
public static void main(String[] args) {
12-
MultipartBody arg0 = CProver.nondetWithNull();
13-
HttpServletRequest arg1 = CProver.nondetWithNull();
14-
ImportRestService obj = CProver.nondetWithNull();
15+
MultipartBody arg0 = CProver.nondetWithNull((MultipartBody)null);
16+
makeTainted(arg0);
17+
HttpServletRequest arg1 = CProver.nondetWithNull((HttpServletRequest)null);
18+
ImportRestService obj = CProver.nondetWithNull((ImportRestService)null);
1519
try {
1620
sink(obj.uploadFile(arg0, arg1));
1721
}

‎src/driver/sec_driver_parse_options.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -215,12 +215,12 @@ int sec_driver_parse_optionst::doit()
215215
return CPROVER_EXIT_SUCCESS;
216216
}
217217

218-
if (cmdline.isset("do-not-use-precise-access-paths"))
218+
if(cmdline.isset("do-not-use-precise-access-paths"))
219219
{
220220
local_value_sett::do_not_use_precise_access_paths = true;
221221
}
222222

223-
if (cmdline.isset("security-scanner"))
223+
if(cmdline.isset("security-scanner"))
224224
{
225225
try
226226
{

0 commit comments

Comments
 (0)