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

1 protectedvoidTextChanged(objectsender,EventArgse){
2 stringstr=Request.QueryString["name"];
3 stringstr2=HttpUtility.HtmlEncode(str);
4 Response.Write(str2);
5 }
7 protectedvoidButtonClicked(objectsender,EventArgse){
8 stringstr=Request.UrlReferrer.AbsolutePath;
9 stringstr2=HttpUtility.UrlEncode(str);
10 Response.Redirect(str2);
11 }

FIGURE 11.17: Program for Example 6.

Sources (1):
stringSystem.Web.HttpUtility+UrlDecoder.Getstring()
Sanitizers (8):
stringSystem.Web.HttpUtility.HtmlEncode(string)
stringSystem.Web.HttpUtility.UrlEncodeSpaces(string)
stringSystem.Web.HttpServerUtility.UrlDecode(string)
stringSystem.Web.HttpUtility.UrlEncode(string,Encoding)
stringSystem.Web.HttpUtility.UrlEncode(string)
stringSystem.Web.HttpServerUtility.UrlEncode(string)
stringSystem.Web.HttpUtility.UrlDecodestringFrom...
stringSystem.Web.HttpUtility.UrlDecode(string,Encoding)
Sinks (4):
voidSystem.Web.HttpResponse.WriteFile(string)
voidSystem.Web.HttpRequest.set_QuerystringText(string)
voidSystem.IO.TextWriter.Write(string)
voidSystem.Web.HttpResponse.Redirect(string)

FIGURE 11.18: Specification inferred for Example 6.

increasingly larger specifications that fill many gaps in the originalCat.Net
specification.

2

11.6.3 Running Times
Finally, Figure 11.19 provides information about running time of the
variousMerlincomponents, measured in seconds. Columns 2{4 show the
Cat.Netrunning time, the time to build the propagation graph, and the in-
ference time. The experiments were conducted on a 3 GHz Pentium Dual Core
Windows XP SP2 machine equipped with 4 GB of memory. Overall, in part
due to the approximation described in Section 11.5, our analysis scales quite
well, with none of the benchmarks taking over four minutes to analyze. Given
thatCat.Netis generally run once a day or less frequently, these running
times are more than acceptable.