Skip to content

Commit

Permalink
[Souffle] Fix Souffle backend to allow refs to strings
Browse files Browse the repository at this point in the history
  • Loading branch information
richardmzhang committed Oct 4, 2017
1 parent 212dda3 commit 6e76675
Show file tree
Hide file tree
Showing 4 changed files with 38 additions and 8 deletions.
33 changes: 29 additions & 4 deletions src/petablox/analyses/taint/taint.dl
Original file line number Diff line number Diff line change
@@ -1,12 +1,34 @@
// name=taint-dlog

.symbol_type Name

.number_type M
.decl MMap(m:M, n:Name) //M,Name
.input MMap()

.number_type MethodID
.decl MethodIDMap(m:MethodID, n:Name) //methodID,Name
.input MethodIDMap()

.number_type EXPR
.decl EXPRMap(e:EXPR, n:Name) //EXPR,Name
.input EXPRMap()

.number_type Invoke
.decl InvokeMap(i:Invoke, n:Name) //Invoke,Name
.input InvokeMap()

.number_type P
.decl PMap(p:P, n:Name) //P,Name
.input PMap()

.number_type Z
.decl ZMap(z:Z, n:Name) //Z,Name
.input ZMap()

.number_type Var
.decl VarMap(v:Var, n:Name) //Var,Name
.input VarMap()

.decl reachableM(m:M) // M
.input reachableM()
Expand Down Expand Up @@ -46,13 +68,16 @@
.decl sql_injection(p0:P,p1:P,e:EXPR) // P0,P1,EXPR0
.output sql_injection()

source(3).
sink(3).
//source("<test.C: int source()>").
//sink("<test.C: void sink(int)>").
.decl sql_injectionMap(p0:Name, p1:Name, e:Name) // P0,P1,EXPR0
.output sql_injectionMap()

source(x) :- MethodIDMap(x, "<test.C: int source()>").
sink(x) :- MethodIDMap(x, "<test.C: void sink(int)>").
taint_var(v,p) :- AssignInst(p,e,e0), VarExpr(e,v), InvokeExpr(e0,i), VirtualInvoke(i,_,f), source(f).
taint_var(v,p) :- AssignInst(_,e,e0), VarExpr(e,v), taint_exp(e0,p).
taint_exp(e,p) :- taint_var(v,p), VarExpr(e,v).
taint_exp(e,p) :- AddExpr(e,e0,_), taint_exp(e0,p).

sql_injection(p0,p1,e) :- taint_exp(e,p0), InvokeInst(p1,i), VirtualInvoke(i,_,f), sink(f), MethodArg(i,0,e).

sql_injectionMap(p0s,p1s,es) :- sql_injection(p0,p1,e), PMap(p0, p0s), PMap(p1, p1s), EXPRMap(e, es).
2 changes: 1 addition & 1 deletion src/petablox/souffle/SouffleExporter.java
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ public class SouffleExporter extends SouffleIOBase {
*/
public void saveDomain(Dom<?> dom) {
String domName = dom.getName();
File factsFile = new File(workDir, domName + ".facts");
File factsFile = new File(workDir, domName + "Map.facts");
saveDomainData(dom, factsFile);

File domainFile = new File(workDir, domName + ".dl");
Expand Down
9 changes: 7 additions & 2 deletions src/petablox/souffle/SouffleParser.java
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,8 @@ public DatalogMetadata parseMetadata(File file) throws IOException {
String line;
while (null != (line = in.readLine())) {
line = line.trim();
if (line.startsWith(".symbol_type") || line.startsWith(".number_type")) {
if (line.startsWith(".number_type")) {
// We don't consider symbol types because BDDBDDB's intermediate output is numbers.
domNames.add(line.substring(13));
} else if (line.startsWith(".type")) {
domNames.add(line.substring(6));
Expand All @@ -59,7 +60,11 @@ public DatalogMetadata parseMetadata(File file) throws IOException {
inputRels.add(line.substring(7, line.indexOf('(')));
} else if (line.startsWith(".decl")) {
String name = line.substring(6, line.indexOf('('));
rels.put(name, line.substring(line.indexOf('(') + 1));
if (!name.endsWith("Map")) {
// Special case here: Map should only be used for
// mapping from bddbddb indexes to strings
rels.put(name, line.substring(line.indexOf('(') + 1));
}
} else if (line.startsWith("// name=")) {
metadata.setDlogName(line.substring(8));
}
Expand Down

0 comments on commit 6e76675

Please sign in to comment.