Databases Reference
In-Depth Information
Also, in this caseWP(Triple; Post
E
)(!) is the product of two quantities
X(!) and Y (!), where X(!) is equal to the product of probabilities c
t
for
each triple t = hs;w;ni such that m(hs;w;ni) 6= 101, and Y (!) is equal
to the product of probabilities (1 c
t
0
) for each triple t
0
= hs
0
;w
0
;n
0
i such
that m(hs
0
;w
0
;n
0
i) = 101. Since c
t
's have been carefully chosen according to
Equation 11.13 and Y (!) 2 [0; 1], it follows that X(!) is less than or equal
to the product of the probabilities c
p
for each path p. Therefore, it is indeed
the case that for each state !,WP(Triple; Post
E
)(!) WP(Path; Post
E
)(!).
Any solver for a probabilistic constraint system C with post expecta-
tion Post
E
chooses states such thatWP(C; Post
E
)() is greater than some
threshold t. Since we have proved thatPathrenesTriple, we know that every
solution state for theTriplesystem is also a solution state for thePathsystem.
Thus, the set of states that are chosen by solver for theTriplesystem is con-
tained in the set of states that are chosen by the solver for thePathsystem.
This has the desirable property that theTriplesystem will not introduce more
false positives than thePathsystem.
Note that thePathsystem itself can result in false positives, since it re-
quires at least one sanitizer on each source-sink path, and does not require
minimization of sanitizers. In order to remove false positives due to redundant
sanitizers, we add the constraints B2 and B3 to theTriplesystem. Further,
the path system does not distinguish wrappers of sources or sinks, so we
add additional constraints B4 and B5 to avoid classifying these wrappers as
sources or sinks. Using all these extra constraints, we find that theTriplesys-
tem performs very well on several large benchmarks and infers specifications
with very few false positives. We describe these results in the next section.
11.6 Experimental Evaluation
Cat.Net, a publicly available state-of-the-art static analysis tool for Web
application, is the platform for our experiments [21].Merlinis implemented
as an add-on on top ofCat.Net, usingInfer.NET, a library [22] that pro-
vides an interface to probabilistic inference algorithms. This section presents
the results of evaluatingMerlinon 10 large .NET Web applications. All
these benchmarks are security-critical enterprise line-of-business applications
currently in production written in C# on top of ASP.NET. They are also
subject to periodic security audits.
Search WWH ::
Custom Search