forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Adding in a test that passes taint information via two arguments of s…
…ink.
- Loading branch information
1 parent
7a6359c
commit 8cf5a0d
Showing
5 changed files
with
161 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
<project name="Main" basedir="." default="compile"> | ||
|
||
<property name="root.dir" value="./"/> | ||
<property name="src.dir" value="${root.dir}/src"/> | ||
<property name="classes.dir" value="${root.dir}/build"/> | ||
|
||
<target name="compile"> | ||
<antcall target="clean" /> | ||
<mkdir dir="${classes.dir}"/> | ||
<javac srcdir="${src.dir}" destdir="${classes.dir}" includeantruntime="false" debug="on" /> | ||
</target> | ||
|
||
<target name="clean"> | ||
<delete dir="${classes.dir}"/> | ||
</target> | ||
|
||
</project> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,75 @@ | ||
{ | ||
"namespace": "com.diffblue.security", | ||
"rules": | ||
[ | ||
{ | ||
"comment": "Streams returned by getInputStream on ServletRequest are tainted", | ||
"class": "two.tokens.HttpServletRequest", | ||
"method": "getInputStream:()Ltwo/tokens/ServletInputStream;", | ||
"result": { | ||
"location": "returns", | ||
"taint": "Tainted stream" | ||
} | ||
}, | ||
{ | ||
"comment": "Read from tainted stream gives tainted string and tainted bytes.", | ||
"class": "two.tokens.ServletInputStream", | ||
"method": "read:([B)Ltwo/tokens/String;", | ||
"input": { | ||
"location": "this", | ||
"taint": "Tainted stream" | ||
}, | ||
"result": { | ||
"location": "arg1", | ||
"namespace": "com.diffblue.security.specialized", | ||
"taint": "Tainted byte array" | ||
} | ||
}, | ||
{ | ||
"comment": "Read from tainted stream gives tainted string and tainted bytes.", | ||
"class": "two.tokens.ServletInputStream", | ||
"method": "read:([B)Ltwo/tokens/String;", | ||
"input": { | ||
"location": "this", | ||
"taint": "Tainted stream" | ||
}, | ||
"result": { | ||
"location": "returns", | ||
"namespace": "com.diffblue.security.specialized", | ||
"taint": "Tainted string" | ||
} | ||
}, | ||
{ | ||
"comment": "Writing potentially tainted bytes (the whole array) to a vulnerable stream is a sink.", | ||
"class": "two.tokens.HttpServletResponse", | ||
"method": "write:([BLtwo/tokens/String;)V", | ||
"input": { | ||
"location": "arg1", | ||
"namespace": "com.diffblue.security.specialized", | ||
"taint": "Tainted byte array" | ||
}, | ||
"sinkTarget": { | ||
"location": "this", | ||
"vulnerability": "Vulnerable stream" | ||
}, | ||
"message": "Unescaped HTML potentially written back to browser" | ||
}, | ||
{ | ||
"comment": "Writing potentially tainted string to a vulnerable stream is a sink.", | ||
"class": "two.tokens.HttpServletResponse", | ||
"method": "write:([BLtwo/tokens/String;)V", | ||
"input": { | ||
"location": "arg2", | ||
"namespace": "com.diffblue.security.specialized", | ||
"taint": "Tainted string" | ||
}, | ||
"sinkTarget": { | ||
"location": "this", | ||
"vulnerability": "Vulnerable stream" | ||
}, | ||
"message": "Unescaped HTML potentially written back to browser" | ||
} | ||
] | ||
} | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,32 @@ | ||
package two.tokens; | ||
|
||
class String { | ||
} | ||
|
||
class ServletInputStream { | ||
String read(byte[] data) { | ||
return new String(); | ||
} | ||
} | ||
|
||
class HttpServletRequest { | ||
public ServletInputStream getInputStream() { | ||
return new ServletInputStream(); | ||
} | ||
} | ||
|
||
class HttpServletResponse { | ||
public void write(byte[] data, String s) { | ||
} | ||
} | ||
|
||
public class Main { | ||
|
||
public void doGet(HttpServletRequest req, HttpServletResponse res) { | ||
byte[] b = new byte[10]; | ||
String s = req.getInputStream().read(b); | ||
res.write(b,s); | ||
} | ||
|
||
} | ||
|
29 changes: 29 additions & 0 deletions
29
regression/end_to_end/taint_two_tokens/test_taint_two_tokens.py
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,29 @@ | ||
import os | ||
import subprocess | ||
|
||
from regression.end_to_end.driver import run_security_analyser_pipeline | ||
import regression.utils as utils | ||
|
||
|
||
def test_taint_two_tokens(): | ||
|
||
with utils.working_dir(os.path.abspath(os.path.dirname(__file__))): | ||
subprocess.call("ant") | ||
with run_security_analyser_pipeline( | ||
"build", | ||
"rules.json", | ||
os.path.realpath(os.path.dirname(__file__))) as traces: | ||
|
||
# There are two traces here but they are both linked to the same line number even if the goto assert operation | ||
# is different. Right now we can't tell the difference between the two, except of their length. | ||
assert traces.count_traces() == 2 | ||
assert traces.trace_of_length_exists( | ||
"java::two.tokens.Main.doGet:(Ltwo/tokens/HttpServletRequest;Ltwo/tokens/HttpServletResponse;)V", | ||
28, | ||
"jbmc", | ||
60) | ||
assert traces.trace_of_length_exists( | ||
"java::two.tokens.Main.doGet:(Ltwo/tokens/HttpServletRequest;Ltwo/tokens/HttpServletResponse;)V", | ||
28, | ||
"jbmc", | ||
61) |