Merlin: Specification Inference for Explicit Information Flow Problems - Mining Software Specifications: Methodologies and Applications - page 380

1.voidProcessRequest(HttpRequestrequest,
2. HttpResponseresponse)
3.{
4. strings1=request.GetParameter("name");
5. strings2=request.GetHeader("encoding");
6.
7. response.WriteLine("Parameter"+s1);
8. response.WriteLine("Header"+s2);
9.}
FIGURE 11.1: Simple cross-site scripting example.
FIGURE 11.2:Merlinsystem architecture.
a sanitizer. In fact, this is precisely what many commercial analysis tools in
everyday use do [4, 24].
User-provided specifications, however, lead to both false positives and false
negatives in practice. False positives arise because a flow from source to sink
classified as offending by the tool could have a sanitizer that the tool was
unaware of. False negatives arise because of incomplete information about
sources and sinks.
This paper presentsMerlin, a tool that automatically infers information
flow specifications for programs. Our inference algorithm uses the intuition
that most paths in a propagation graph are secure. That is, most paths in the
propagation graph that start from a source and end in a sink pass through
some sanitizer.
Example 1 Consider a Web application code snippet written in C# shown
in Figure 11.1. While method GetParameter , the method returning argu-
ments of an HTTP request, is highly likely to be part of the default specifi-
cation that comes with a static analysis tool and classified as a source, the
method retrieving an HTTP header GetHeader may easily be missed. Be-
cause response : WriteLine sends information to the browser, there are two
possibilities of cross-site scripting vulnerabilities on line 7 and line 8. The vul-
nerability in line 7 (namely, passing a tainted value returned by GetParameter
into WriteLine without saniziting it first) will be reported, but the similar
vulnerability on line 8 may be missed due to an incomplete specification. In
fact, in both .NET and J2EE there exist a number of source methods that