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

Chapter 11
Merlin: Specification Inference for
Explicit Information Flow Problems
Benjamin Livshits
Microsoft Research{Redmond
Aditya V. Nori
Microsoft Research{Redmond
Sriram K. Rajamani
Microsoft Research{Bangalore
Anindya Banerjee
IMDEA Software
11.1 Introduction ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 379
11.2 Overview :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 382
11.2.1 Assumptions and Probabilistic Inference ::::::::::::::::::::::::: 383
11.2.2 Potential Sources, Sinks, and Sanitizers :::::::::::::::::::::::::: 384
11.2.3 Core Constraints :::::::::::::::::::::::::::::::::::::::::::::::::: 384
11.2.4 Auxiliary Constraints ::::::::::::::::::::::::::::::::::::::::::::: 386
11.3 Factor Graph Primer :::::::::::::::::::::::::::::::::::::::::::::::::::::: 388
11.4 Constructing the Factor Graph ::::::::::::::::::::::::::::::::::::::::::: 390
11.4.1 Computing s() and W() :::::::::::::::::::::::::::::::::::::::::: 392
11.5 Relationship between Triples and Paths :::::::::::::::::::::::::::::::::: 395
11.6 Experimental Evaluation :::::::::::::::::::::::::::::::::::::::::::::::::: 398
11.6.1 Experimental Setup ::::::::::::::::::::::::::::::::::::::::::::::: 399
11.6.2 Merlin Findings ::::::::::::::::::::::::::::::::::::::::::::::::::: 400
11.6.3 Running Times :::::::::::::::::::::::::::::::::::::::::::::::::::: 404
11.7 Related Work ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 405
11.7.1 Securing Web Applications :::::::::::::::::::::::::::::::::::::::: 405
11.7.2 Mining Specications :::::::::::::::::::::::::::::::::::::::::::::: 406
11.8 Conclusions :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 406
Acknowledgments ::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 407
Bibliography ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 407
377