Skip to content

Commit 6c303bb

Browse files
marek-trtiksmowton
marek-trtik
authored and
smowton
committed
Merge pull request diffblue#101 from trtikm/security_scanner__extended_expressivity_PR
Security scanner: Initial implementation of the extended expressivity.
1 parent 14ef1b5 commit 6c303bb

22 files changed

+1283
-478
lines changed

‎regression/december_demo_sprint/TRAINING/taint_traces_06/APP/README.txt

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
taint_traces_05
2+
~~~~~~~~~~~~~~~
3+
4+
This is a training benchmarks. It won't be part of the evaluation. Also, this is not Maven
5+
application (actually it uses Ant). But this fact does not affect it use as a training bemchmark.
6+
7+
Installation on Ubuntu
8+
9+
1. Open terminal in the root directory of the souce code (there should be a file "build.xml")
10+
and run there this command: ant
11+
12+
Resulting JAR file is automatically copied into directory ../BENCHMARK, which is a destination
13+
already consistent with this evaluation. So, no other steps are necessary.

‎regression/december_demo_sprint/TRAINING/taint_traces_06/APP/roots.json

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
[
2+
"taint_test.test.doGet"
3+
]
4+

‎regression/december_demo_sprint/TRAINING/taint_traces_06/APP/taint.json

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
[
2+
{
3+
"id": "my_source",
4+
"kind": "source",
5+
"where": "return_value",
6+
"immediate": true,
7+
"taint": "X1",
8+
"function": "TaintSource.get_tainted_int"
9+
},
10+
{
11+
"id": "my_sink",
12+
"kind": "sink",
13+
"where": "parameter1",
14+
"immediate": true,
15+
"taint": "X1",
16+
"function": "TaintSink.receive_taint",
17+
"message": "Unescaped HTML written to DAO"
18+
}
19+
]
20+

‎regression/december_demo_sprint/TRAINING/taint_traces_06/APP/taint_traces_06/build.xml

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
<project name="taint_traces_06" basedir="." default="jar">
2+
3+
<property name="root.dir" value="./"/>
4+
<property name="src.dir" value="${root.dir}"/>
5+
<property name="classes.dir" value="${root.dir}/classes"/>
6+
<property name="serverlib.dir" value="/home/marek/Software/apache-tomcat-9.0.0.M11/lib"/>
7+
<property name="install.dir" value="${root.dir}/../../BENCHMARK"/>
8+
9+
<path id="server.lib">
10+
<fileset dir="${serverlib.dir}">
11+
<include name="servlet*.jar"/>
12+
</fileset>
13+
</path>
14+
15+
<target name="jar">
16+
<antcall target="compile" />
17+
<mkdir dir="${install.dir}"/>
18+
<jar destfile="${install.dir}/taint_traces_06.war" basedir="${classes.dir}" />
19+
</target>
20+
21+
<target name="compile">
22+
<antcall target="clean" />
23+
<mkdir dir="${classes.dir}"/>
24+
<javac srcdir="${src.dir}" destdir="${classes.dir}" includeantruntime="false" debug="on">
25+
<classpath refid="server.lib"/>
26+
</javac>
27+
</target>
28+
29+
<target name="clean">
30+
<delete dir="${classes.dir}"/>
31+
</target>
32+
33+
34+
</project>
35+

‎regression/december_demo_sprint/TRAINING/taint_traces_06/APP/taint_traces_06/test.java

Lines changed: 299 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,299 @@
1+
package taint_test;
2+
3+
import javax.servlet.http.HttpServlet;
4+
import javax.servlet.http.HttpServletRequest;
5+
import javax.servlet.http.HttpServletResponse;
6+
import java.io.InputStream;
7+
import java.io.OutputStream;
8+
import java.io.IOException;
9+
10+
11+
/*
12+
13+
** State transformation rules **
14+
15+
Rule no. Sink? Base class Method/operator Assumptions on args Effect
16+
17+
0 false ServletRequest getInputStream (*) RET -> {1}
18+
19+
1 false InputStream read ({0},*,*,*) ARG1 -> {2}
20+
21+
2 false String String ({2},*,*) RET -> {3}
22+
23+
3 false String charAt ({3},*) RET -> {4}
24+
25+
4 false String replace (*,"<",#) ARG0 -> BOTTOM
26+
27+
5 false ServletResponse getOutputStream (*) RET -> {6}
28+
29+
6 true OutputStream write ({6},{2},*,*)
30+
31+
7 true OutputStream write ({6},{3})
32+
33+
8 true OutputStream write ({6},{4})
34+
35+
9 false java.util.List add (*,{3}) ARG0 -> {ARG0}+{3}
36+
37+
10 false java.util.List add (*,{4}) ARG0 -> {ARG0}+{4}
38+
39+
*/
40+
public class test extends javax.servlet.http.HttpServlet {
41+
42+
/*
43+
Input map:
44+
request -> T1
45+
response -> T2
46+
Summary:
47+
*/
48+
@Override
49+
public void doGet(HttpServletRequest request, HttpServletResponse response) {
50+
// request -> T1
51+
// response -> T2
52+
53+
java.io.InputStream in0 = getInStream(request); // rule: IMPLICIT - applying summary and assignment
54+
55+
// request -> T1
56+
// response -> T2
57+
// in0 -> {1}
58+
59+
java.io.InputStream in = in0; // rule: IMPLICIT - copy ref
60+
61+
// request -> T1
62+
// response -> T2
63+
// in0 -> {1}
64+
// in -> {1}
65+
66+
byte[] data = new byte[2048]; // rule: IMPLICIT - new
67+
68+
// request -> T1
69+
// response -> T2
70+
// in0 -> {1}
71+
// in -> {1}
72+
73+
int size = getBytes(data,in); // rule: IMPLICIT - applying summary and assignment
74+
75+
// request -> T1
76+
// response -> T2
77+
// in0 -> {1}
78+
// in -> {1}
79+
// data -> {2}
80+
81+
String str0 = new String(data, 0, size); // rule: 2
82+
83+
// request -> T1
84+
// response -> T2
85+
// in0 -> {1}
86+
// in -> {1}
87+
// data -> {2}
88+
// str0 -> {3}
89+
90+
String str = str0; // rule: IMPLICIT - copy ref
91+
92+
// request -> T1
93+
// response -> T2
94+
// in0 -> {1}
95+
// in -> {1}
96+
// data -> {2}
97+
// str0 -> {3}
98+
// str -> {3}
99+
100+
char c = str.charAt(size / 2); // rule: 3
101+
102+
// request -> T1
103+
// response -> T2
104+
// in0 -> {1}
105+
// in -> {1}
106+
// data -> {2}
107+
// str0 -> {3}
108+
// str -> {3}
109+
// c -> {4}
110+
111+
sanitise(str); // rule: IMPLICIT - applying summary
112+
113+
// request -> T1
114+
// response -> T2
115+
// in0 -> {1}
116+
// in -> {1}
117+
// data -> {2}
118+
// c -> {4}
119+
120+
java.io.OutputStream out0 = getOutStream(response); // rule: IMPLICIT - applying summary and assignment
121+
122+
// request -> T1
123+
// response -> T2
124+
// in0 -> {1}
125+
// in -> {1}
126+
// data -> {2}
127+
// c -> {4}
128+
// out0 -> {6}
129+
130+
java.io.OutputStream out = out0; // rule: IMPLICIT - copy ref
131+
132+
// request -> T1
133+
// response -> T2
134+
// in0 -> {1}
135+
// in -> {1}
136+
// data -> {2}
137+
// c -> {4}
138+
// out0 -> {6}
139+
// out -> {6}
140+
141+
try {
142+
143+
out.write(data,0,size); // rule: 6 !SINK!
144+
145+
// request -> T1
146+
// response -> T2
147+
// in0 -> {1}
148+
// in -> {1}
149+
// data -> {2}
150+
// c -> {4}
151+
// out0 -> {6}
152+
// out -> {6}
153+
154+
out.write(str.getBytes()); // rule: 7 !SINK!
155+
156+
// request -> T1
157+
// response -> T2
158+
// in0 -> {1}
159+
// in -> {1}
160+
// data -> {2}
161+
// c -> {4}
162+
// out0 -> {6}
163+
// out -> {6}
164+
165+
out.write(c); // rule: 8 !SINK!
166+
167+
// request -> T1
168+
// response -> T2
169+
// in0 -> {1}
170+
// in -> {1}
171+
// data -> {2}
172+
// c -> {4}
173+
// out0 -> {6}
174+
// out -> {6}
175+
176+
} catch(java.io.IOException e) {}
177+
}
178+
179+
/*
180+
Input map:
181+
request -> T3
182+
Summary:
183+
return_value -> {1}
184+
*/
185+
private java.io.InputStream getInStream(HttpServletRequest request) {
186+
try {
187+
188+
// request -> T3
189+
190+
return request.getInputStream(); // rule: 0
191+
192+
// request -> T3
193+
// return_value -> {1}
194+
195+
} catch(java.io.IOException e) {
196+
return null;
197+
}
198+
}
199+
200+
/*
201+
Input map:
202+
data -> T4
203+
in -> T5
204+
Summary:
205+
data -> ITE({1} in T5,{2},BOTTOM)
206+
*/
207+
private int getBytes(byte[] data, java.io.InputStream in) {
208+
try {
209+
210+
// data -> T4
211+
// in -> T5
212+
213+
return in.read(data, 0, data.length); // rule: 1
214+
215+
// data -> ITE({1} in T5,{2},BOTTOM)
216+
// in -> T5
217+
218+
} catch(java.io.IOException e) {
219+
return 0;
220+
}
221+
}
222+
223+
/*
224+
Input map:
225+
str -> T6
226+
Summary:
227+
str -> BOTTOM
228+
*/
229+
private void sanitise(String str) {
230+
231+
// str -> T6
232+
233+
str.replace("<","&lt;"); // rule: 4
234+
235+
// str -> BOTTOM
236+
237+
str.replace(">","&gt;"); // rule: IMPLICIT - identity
238+
239+
// str -> BOTTOM
240+
}
241+
242+
/*
243+
Input map:
244+
response -> T7
245+
Summary:
246+
return_value -> {6}
247+
*/
248+
private java.io.OutputStream getOutStream(HttpServletResponse response) {
249+
try {
250+
// response -> T7
251+
252+
return response.getOutputStream(); // rule: 5
253+
254+
// response -> T7
255+
// return_value -> {6}
256+
257+
} catch(java.io.IOException e) {
258+
return null;
259+
}
260+
}
261+
262+
263+
/*
264+
Input map:
265+
ss -> {3}
266+
cc -> {4}
267+
Summary:
268+
return_value -> {3,4}
269+
*/
270+
private java.util.List foo(String ss, Character cc) {
271+
272+
// ss -> {3}
273+
// cc -> {4}
274+
275+
java.util.List<java.lang.Object> L = new java.util.ArrayList<java.lang.Object>(); // rule: IMPLICIT - new
276+
277+
// ss -> {3}
278+
// cc -> {4}
279+
280+
L.add(ss); // rule: 9
281+
282+
// ss -> {3}
283+
// cc -> {4}
284+
// L -> {3}
285+
286+
L.add(cc); // rule:
287+
288+
// ss -> {3}
289+
// cc -> {4}
290+
// L -> {3,4}
291+
292+
return L;
293+
294+
// ss -> {3}
295+
// cc -> {4}
296+
// L -> {3,4}
297+
}
298+
}
299+

‎regression/december_demo_sprint/goto-analyzer/run.py

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -271,6 +271,7 @@ def __main():
271271
os.path.abspath(os.path.join(__get_my_dir(), "..", "TRAINING/taint_traces_03")),
272272
os.path.abspath(os.path.join(__get_my_dir(), "..", "TRAINING/taint_traces_04")),
273273
os.path.abspath(os.path.join(__get_my_dir(), "..", "TRAINING/taint_traces_05")),
274+
os.path.abspath(os.path.join(__get_my_dir(), "..", "TRAINING/taint_traces_06")),
274275
]
275276
toy_benchs = [
276277
os.path.abspath(os.path.join(__get_my_dir(), "..", "TOY_APPS/Fotoalbum")),

‎src/cbmc.files

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -699,11 +699,15 @@ goto-analyzer/taint_summary_json.cpp
699699
goto-analyzer/taint_summary_json.h
700700
goto-analyzer/taint_summary_libmodels.cpp
701701
goto-analyzer/taint_summary_libmodels.h
702+
goto-analyzer/taint_svalue.cpp
703+
goto-analyzer/taint_svalue.h
702704
goto-analyzer/taint_trace_recogniser.cpp
703705
goto-analyzer/taint_trace_recogniser.h
704706
goto-analyzer/taint_trace_dump_html.cpp
705707
goto-analyzer/taint_trace_dump_json.cpp
706708
goto-analyzer/taint_trace_dump.h
709+
goto-analyzer/taint_transition_rules.cpp
710+
goto-analyzer/taint_transition_rules.h
707711
goto-analyzer/unreachable_instructions.cpp
708712
goto-analyzer/unreachable_instructions.h
709713
goto-analyzer/taint_fast_analyser.cpp

0 commit comments

Comments
 (0)