Skip to content

Commit 6ef5fac

Browse files
aschackmullaschackmull
authored
Merge pull request github#10814 from aschackmull/dataflow/synth-global
Dataflow: Add support for synthetic global fields in MaD.
2 parents dbee26e + 72fc9d1 commit 6ef5fac

File tree

18 files changed

+340
-11
lines changed

18 files changed

+340
-11
lines changed

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowPrivate.qll

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1672,6 +1672,8 @@ predicate jumpStep(Node pred, Node succ) {
16721672
jrk.getTarget() = call.getATarget(_) and
16731673
succ = getAnOutNode(call, jrk.getTargetReturnKind())
16741674
)
1675+
or
1676+
FlowSummaryImpl::Private::Steps::summaryJumpStep(pred, succ)
16751677
}
16761678

16771679
private class StoreStepConfiguration extends ControlFlowReachabilityConfiguration {

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImpl.qll

Lines changed: 53 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,20 @@ module Public {
6161

6262
/** Gets a summary component for a return of kind `rk`. */
6363
SummaryComponent return(ReturnKind rk) { result = TReturnSummaryComponent(rk) }
64+
65+
/** Gets a summary component for synthetic global `sg`. */
66+
SummaryComponent syntheticGlobal(SyntheticGlobal sg) {
67+
result = TSyntheticGlobalSummaryComponent(sg)
68+
}
69+
70+
/**
71+
* A synthetic global. This represents some form of global state, which
72+
* summaries can read and write individually.
73+
*/
74+
abstract class SyntheticGlobal extends string {
75+
bindingset[this]
76+
SyntheticGlobal() { any() }
77+
}
6478
}
6579

6680
/**
@@ -256,6 +270,7 @@ module Private {
256270
TParameterSummaryComponent(ArgumentPosition pos) or
257271
TArgumentSummaryComponent(ParameterPosition pos) or
258272
TReturnSummaryComponent(ReturnKind rk) or
273+
TSyntheticGlobalSummaryComponent(SummaryComponent::SyntheticGlobal sg) or
259274
TWithoutContentSummaryComponent(ContentSet c) or
260275
TWithContentSummaryComponent(ContentSet c)
261276

@@ -563,6 +578,11 @@ module Private {
563578
getCallbackReturnType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
564579
s.tail())), rk)
565580
)
581+
or
582+
exists(SummaryComponent::SyntheticGlobal sg |
583+
head = TSyntheticGlobalSummaryComponent(sg) and
584+
result = getSyntheticGlobalType(sg)
585+
)
566586
)
567587
or
568588
n = summaryNodeOutputState(c, s) and
@@ -582,6 +602,11 @@ module Private {
582602
getCallbackParameterType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
583603
s.tail())), pos)
584604
)
605+
or
606+
exists(SummaryComponent::SyntheticGlobal sg |
607+
head = TSyntheticGlobalSummaryComponent(sg) and
608+
result = getSyntheticGlobalType(sg)
609+
)
585610
)
586611
)
587612
}
@@ -692,6 +717,18 @@ module Private {
692717
)
693718
}
694719

720+
/**
721+
* Holds if there is a jump step from `pred` to `succ`, which is synthesized
722+
* from a flow summary.
723+
*/
724+
predicate summaryJumpStep(Node pred, Node succ) {
725+
exists(SummaryComponentStack s |
726+
s = SummaryComponentStack::singleton(SummaryComponent::syntheticGlobal(_)) and
727+
pred = summaryNodeOutputState(_, s) and
728+
succ = summaryNodeInputState(_, s)
729+
)
730+
}
731+
695732
/**
696733
* Holds if values stored inside content `c` are cleared at `n`. `n` is a
697734
* synthesized summary node, so in order for values to be cleared at calls
@@ -871,18 +908,28 @@ module Private {
871908
AccessPathRange() { relevantSpec(this) }
872909
}
873910

874-
/** Holds if specification component `c` parses as parameter `n`. */
911+
/** Holds if specification component `token` parses as parameter `pos`. */
875912
predicate parseParam(AccessPathToken token, ArgumentPosition pos) {
876913
token.getName() = "Parameter" and
877914
pos = parseParamBody(token.getAnArgument())
878915
}
879916

880-
/** Holds if specification component `c` parses as argument `n`. */
917+
/** Holds if specification component `token` parses as argument `pos`. */
881918
predicate parseArg(AccessPathToken token, ParameterPosition pos) {
882919
token.getName() = "Argument" and
883920
pos = parseArgBody(token.getAnArgument())
884921
}
885922

923+
/** Holds if specification component `token` parses as synthetic global `sg`. */
924+
predicate parseSynthGlobal(AccessPathToken token, string sg) {
925+
token.getName() = "SyntheticGlobal" and
926+
sg = token.getAnArgument()
927+
}
928+
929+
private class SyntheticGlobalFromAccessPath extends SummaryComponent::SyntheticGlobal {
930+
SyntheticGlobalFromAccessPath() { parseSynthGlobal(_, this) }
931+
}
932+
886933
private SummaryComponent interpretComponent(AccessPathToken token) {
887934
exists(ParameterPosition pos |
888935
parseArg(token, pos) and result = SummaryComponent::argument(pos)
@@ -894,6 +941,10 @@ module Private {
894941
or
895942
token = "ReturnValue" and result = SummaryComponent::return(getReturnValueKind())
896943
or
944+
exists(string sg |
945+
parseSynthGlobal(token, sg) and result = SummaryComponent::syntheticGlobal(sg)
946+
)
947+
or
897948
result = interpretComponentSpecific(token)
898949
}
899950

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/FlowSummaryImplSpecific.qll

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,12 @@ DataFlowType getCallbackReturnType(DataFlowType t, ReturnKind rk) {
9191
)
9292
}
9393

94+
/** Gets the type of synthetic global `sg`. */
95+
DataFlowType getSyntheticGlobalType(SummaryComponent::SyntheticGlobal sg) {
96+
exists(sg) and
97+
result = Gvn::getGlobalValueNumber(any(ObjectType t))
98+
}
99+
94100
bindingset[provenance]
95101
private boolean isGenerated(string provenance) {
96102
provenance = "generated" and result = true

‎java/ql/lib/semmle/code/java/dataflow/internal/DataFlowPrivate.qll

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,8 @@ predicate jumpStep(Node node1, Node node2) {
8383
or
8484
any(AdditionalValueStep a).step(node1, node2) and
8585
node1.getEnclosingCallable() != node2.getEnclosingCallable()
86+
or
87+
FlowSummaryImpl::Private::Steps::summaryJumpStep(node1, node2)
8688
}
8789

8890
/**

‎java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImpl.qll

Lines changed: 53 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,20 @@ module Public {
6161

6262
/** Gets a summary component for a return of kind `rk`. */
6363
SummaryComponent return(ReturnKind rk) { result = TReturnSummaryComponent(rk) }
64+
65+
/** Gets a summary component for synthetic global `sg`. */
66+
SummaryComponent syntheticGlobal(SyntheticGlobal sg) {
67+
result = TSyntheticGlobalSummaryComponent(sg)
68+
}
69+
70+
/**
71+
* A synthetic global. This represents some form of global state, which
72+
* summaries can read and write individually.
73+
*/
74+
abstract class SyntheticGlobal extends string {
75+
bindingset[this]
76+
SyntheticGlobal() { any() }
77+
}
6478
}
6579

6680
/**
@@ -256,6 +270,7 @@ module Private {
256270
TParameterSummaryComponent(ArgumentPosition pos) or
257271
TArgumentSummaryComponent(ParameterPosition pos) or
258272
TReturnSummaryComponent(ReturnKind rk) or
273+
TSyntheticGlobalSummaryComponent(SummaryComponent::SyntheticGlobal sg) or
259274
TWithoutContentSummaryComponent(ContentSet c) or
260275
TWithContentSummaryComponent(ContentSet c)
261276

@@ -563,6 +578,11 @@ module Private {
563578
getCallbackReturnType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
564579
s.tail())), rk)
565580
)
581+
or
582+
exists(SummaryComponent::SyntheticGlobal sg |
583+
head = TSyntheticGlobalSummaryComponent(sg) and
584+
result = getSyntheticGlobalType(sg)
585+
)
566586
)
567587
or
568588
n = summaryNodeOutputState(c, s) and
@@ -582,6 +602,11 @@ module Private {
582602
getCallbackParameterType(getNodeType(summaryNodeInputState(pragma[only_bind_out](c),
583603
s.tail())), pos)
584604
)
605+
or
606+
exists(SummaryComponent::SyntheticGlobal sg |
607+
head = TSyntheticGlobalSummaryComponent(sg) and
608+
result = getSyntheticGlobalType(sg)
609+
)
585610
)
586611
)
587612
}
@@ -692,6 +717,18 @@ module Private {
692717
)
693718
}
694719

720+
/**
721+
* Holds if there is a jump step from `pred` to `succ`, which is synthesized
722+
* from a flow summary.
723+
*/
724+
predicate summaryJumpStep(Node pred, Node succ) {
725+
exists(SummaryComponentStack s |
726+
s = SummaryComponentStack::singleton(SummaryComponent::syntheticGlobal(_)) and
727+
pred = summaryNodeOutputState(_, s) and
728+
succ = summaryNodeInputState(_, s)
729+
)
730+
}
731+
695732
/**
696733
* Holds if values stored inside content `c` are cleared at `n`. `n` is a
697734
* synthesized summary node, so in order for values to be cleared at calls
@@ -871,18 +908,28 @@ module Private {
871908
AccessPathRange() { relevantSpec(this) }
872909
}
873910

874-
/** Holds if specification component `c` parses as parameter `n`. */
911+
/** Holds if specification component `token` parses as parameter `pos`. */
875912
predicate parseParam(AccessPathToken token, ArgumentPosition pos) {
876913
token.getName() = "Parameter" and
877914
pos = parseParamBody(token.getAnArgument())
878915
}
879916

880-
/** Holds if specification component `c` parses as argument `n`. */
917+
/** Holds if specification component `token` parses as argument `pos`. */
881918
predicate parseArg(AccessPathToken token, ParameterPosition pos) {
882919
token.getName() = "Argument" and
883920
pos = parseArgBody(token.getAnArgument())
884921
}
885922

923+
/** Holds if specification component `token` parses as synthetic global `sg`. */
924+
predicate parseSynthGlobal(AccessPathToken token, string sg) {
925+
token.getName() = "SyntheticGlobal" and
926+
sg = token.getAnArgument()
927+
}
928+
929+
private class SyntheticGlobalFromAccessPath extends SummaryComponent::SyntheticGlobal {
930+
SyntheticGlobalFromAccessPath() { parseSynthGlobal(_, this) }
931+
}
932+
886933
private SummaryComponent interpretComponent(AccessPathToken token) {
887934
exists(ParameterPosition pos |
888935
parseArg(token, pos) and result = SummaryComponent::argument(pos)
@@ -894,6 +941,10 @@ module Private {
894941
or
895942
token = "ReturnValue" and result = SummaryComponent::return(getReturnValueKind())
896943
or
944+
exists(string sg |
945+
parseSynthGlobal(token, sg) and result = SummaryComponent::syntheticGlobal(sg)
946+
)
947+
or
897948
result = interpretComponentSpecific(token)
898949
}
899950

‎java/ql/lib/semmle/code/java/dataflow/internal/FlowSummaryImplSpecific.qll

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,12 @@ DataFlowType getCallbackReturnType(DataFlowType t, ReturnKind rk) {
5252
exists(rk)
5353
}
5454

55+
/** Gets the type of synthetic global `sg`. */
56+
DataFlowType getSyntheticGlobalType(SummaryComponent::SyntheticGlobal sg) {
57+
exists(sg) and
58+
result instanceof TypeObject
59+
}
60+
5561
bindingset[provenance]
5662
private boolean isGenerated(string provenance) {
5763
provenance = "generated" and result = true

‎java/ql/test/library-tests/dataflow/synth-global/A.java

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
package my.qltest.synth;
2+
3+
public class A {
4+
void storeInArray(String x) { }
5+
void storeTaintInArray(String x) { }
6+
void storeValue(String x) { }
7+
8+
String readValue() { return null; }
9+
String readArray() { return null; }
10+
11+
String source(String tag) { return "tainted"; }
12+
13+
void sink(Object o) { }
14+
15+
void stores() {
16+
storeInArray(source("A"));
17+
storeTaintInArray(source("B"));
18+
storeValue(source("C"));
19+
}
20+
21+
void reads() {
22+
sink(readValue()); // $ hasValueFlow=C
23+
sink(readArray()); // $ hasValueFlow=A hasTaintFlow=B hasTaintFlow=C
24+
}
25+
}

‎java/ql/test/library-tests/dataflow/synth-global/test.expected

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
failures
2+
invalidModelRow

‎java/ql/test/library-tests/dataflow/synth-global/test.ql

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
import java
2+
import TestUtilities.InlineFlowTest
3+
import CsvValidation
4+
5+
class SummaryModelTest extends SummaryModelCsv {
6+
override predicate row(string row) {
7+
row =
8+
[
9+
"my.qltest.synth;A;false;storeInArray;(String);;Argument[0];SyntheticGlobal[db1].ArrayElement;value;manual",
10+
"my.qltest.synth;A;false;storeTaintInArray;(String);;Argument[0];SyntheticGlobal[db1].ArrayElement;taint;manual",
11+
"my.qltest.synth;A;false;storeValue;(String);;Argument[0];SyntheticGlobal[db1];value;manual",
12+
"my.qltest.synth;A;false;readValue;();;SyntheticGlobal[db1];ReturnValue;value;manual",
13+
"my.qltest.synth;A;false;readArray;();;SyntheticGlobal[db1].ArrayElement;ReturnValue;value;manual",
14+
]
15+
}
16+
}

‎python/ql/lib/semmle/python/dataflow/new/internal/DataFlowPrivate.qll

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -453,6 +453,8 @@ predicate jumpStep(Node nodeFrom, Node nodeTo) {
453453
jumpStepSharedWithTypeTracker(nodeFrom, nodeTo)
454454
or
455455
jumpStepNotSharedWithTypeTracker(nodeFrom, nodeTo)
456+
or
457+
FlowSummaryImpl::Private::Steps::summaryJumpStep(nodeFrom, nodeTo)
456458
}
457459

458460
/**

0 commit comments

Comments
 (0)