×

Formal methods for web security. (English) Zbl 1359.68021

Summary: In the last few years, many security researchers proposed to endow the web platform with more rigorous foundations, thus allowing for a precise reasoning on web security issues. Given the complexity of the Web, however, research efforts in the area are scattered around many different topics and problems, and it is not easy to understand the import of formal methods on web security so far. In this survey we collect, classify and review existing proposals in the area of formal methods for web security, spanning many different topics: JavaScript security, browser security, web application security, and web protocol analysis. Based on the existing literature, we discuss recommendations for researchers working in the area to ensure their proposals have the right ingredients to be amenable for a large scale adoption.

MSC:

68M11 Internet topics
68-02 Research exposition (monographs, survey articles) pertaining to computer science
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Abadi, M.; Fournet, C., Mobile values, new names, and secure communication, (Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17-19, 2001, (2001)), 104-115 · Zbl 1323.68398
[2] Akhawe, D.; Barth, A.; Lam, P. E.; Mitchell, J. C.; Song, D., Towards a formal foundation of web security, (Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, (2010)), 290-304
[3] Armando, A.; Carbone, R.; Compagna, L.; Cuéllar, J.; Pellegrino, G.; Sorniotti, A., An authentication flaw in browser-based single sign-on protocols: impact and remediations, Comput. Secur., 33, 41-58, (2013)
[4] Armando, A.; Carbone, R.; Compagna, L.; Cuéllar, J.; Tobarra, M. L., Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for google apps, (Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering, FMSE 2008, Alexandria, VA, USA, October 27, 2008, (2008)), 1-10
[5] Balliu, M.; Liebe, B.; Schoepe, D.; Sabelfeld, A., JSLINQ: building secure applications across tiers, (Proceedings of the Sixth ACM on Conference on Data and Application Security and Privacy, CODASPY 2016, New Orleans, LA, USA, March 9-11, 2016, (2016)), 307-318
[6] Baltopoulos, I. G.; Gordon, A. D., Secure compilation of a multi-tier web language, (Proceedings of TLDI’09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, (2009)), 27-38
[7] Bansal, C.; Bhargavan, K.; Delignat-Lavaud, A.; Maffeis, S., Keys to the cloud: formal analysis and concrete attacks on encrypted web storage, (Principles of Security and Trust - Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings, (2013)), 126-146 · Zbl 06195651
[8] Bansal, C.; Bhargavan, K.; Maffeis, S., Discovering concrete attacks on website authorization by formal analysis, (25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012, (2012)), 247-262
[9] Barth, A., The web origin concept, (2011)
[10] Bauer, L.; Cai, S.; Jia, L.; Passaro, T.; Stroucken, M.; Tian, Y., Run-time monitoring and formal analysis of information flows in chromium, (22nd Annual Network and Distributed System Security Symposium, NDSS 2015, San Diego, California, USA, February 8-11, 2015, (2015))
[11] Bengtson, J.; Bhargavan, K.; Fournet, C.; Gordon, A. D.; Maffeis, S., Refinement types for secure implementations, ACM Trans. Program. Lang. Syst., 33, 2, 8, (2011)
[12] Bhargavan, K.; Delignat-Lavaud, A.; Maffeis, S., Language-based defenses against untrusted browser origins, (Proceedings of the 22th USENIX Security Symposium, Washington, DC, USA, August 14-16, 2013, (2013)), 653-670
[13] Bielova, N., Survey on javascript security policies and their enforcement mechanisms in a web browser, J. Log. Algebraic Program., 82, 8, 243-262, (2013) · Zbl 1283.68063
[14] Bielova, N.; Devriese, D.; Massacci, F.; Piessens, F., Reactive non-interference for a browser model, (5th International Conference on Network and System Security, NSS 2011, Milan, Italy, September 6-8, 2011, (2011)), 97-104
[15] Bisht, P.; Madhusudan, P.; Venkatakrishnan, V. N., CANDID: dynamic candidate evaluations for automatic prevention of SQL injection attacks, ACM Trans. Inf. Syst. Secur., 13, 2, (2010)
[16] Blanchet, B., Automatic verification of security protocols in the symbolic model: the verifier proverif, (Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures, (2013)), 54-87 · Zbl 1448.68185
[17] Bodin, M.; Charguéraud, A.; Filaretti, D.; Gardner, P.; Maffeis, S.; Naudziuniene, D.; Schmitt, A.; Smith, G., A trusted mechanised javascript specification, (The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, (2014)), 87-100 · Zbl 1284.68381
[18] Bohannon, A., Foundations of webscript security, (2012), University of Pennsylvania, PhD thesis
[19] Bohannon, A.; Pierce, B. C., Featherweight firefox: formalizing the core of a web browser, (USENIX Conference on Web Application Development, WebApps’10, Boston, Massachusetts, USA, June 23-24, 2010, (2010))
[20] Boudol, G.; Luo, Z.; Rezk, T.; Serrano, M., Reasoning about web applications: an operational semantics for HOP, ACM Trans. Program. Lang. Syst., 34, 2, 10, (2012)
[21] Bugliesi, M.; Calzavara, S.; Focardi, R.; Khan, W., Cookiext: patching the browser against session hijacking attacks, J. Comput. Secur., 23, 4, 509-537, (2015)
[22] Bugliesi, M.; Calzavara, S.; Focardi, R.; Khan, W.; Tempesta, M., Provably sound browser-based enforcement of web session integrity, (IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014, (2014)), 366-380
[23] Calzavara, S.; Bugliesi, M.; Crafa, S.; Steffinlongo, E., Fine-grained detection of privilege escalation attacks on browser extensions, (Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings, (2015)), 510-534 · Zbl 1335.68047
[24] Calzavara, S.; Tolomei, G.; Casini, A.; Bugliesi, M.; Orlando, S., A supervised learning approach to protect client authentication on the web, ACM Trans. Web, 9, 3, 15, (2015)
[25] Cantor, S.; Erdos, M., (2015), Available at
[26] Chen, E. Y.; Bau, J.; Reis, C.; Barth, A.; Jackson, C., App isolation: get the security of multiple browsers with just one, (Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17-21, 2011, (2011)), 227-238
[27] Chlipala, A., Static checking of dynamically-varying security policies in database-backed applications, (9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, October 4-6, 2010, Vancouver, BC, Canada, Proceedings, (2010)), 105-118
[28] Chlipala, A., Ur/web: a simple model for programming the web, (Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, (2015)), 153-165
[29] Cooper, E.; Lindley, S.; Wadler, P.; Yallop, J., Links: web programming without tiers, (Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures, (2006)), 266-296
[30] Corcoran, B. J.; Swamy, N.; Hicks, M. W., Cross-tier, label-based security enforcement for web applications, (Proceedings of the ACM SIGMOD International Conference on Management of Data, SIGMOD 2009, Providence, Rhode Island, USA, June 29-July 2, 2009, (2009)), 269-282
[31] De Ryck, P.; Desmet, L.; Joosen, W.; Piessens, F., Automatic and precise client-side protection against CSRF attacks, (Computer Security - ESORICS 2011 - 16th European Symposium on Research in Computer Security, Leuven, Belgium, September 12-14, 2011, Proceedings, (2011)), 100-116
[32] Devriese, D.; Birkedal, L.; Piessens, F., Reasoning about object capabilities with logical relations and effect parametricity, (IEEE European Symposium on Security and Privacy, EuroS&P 2016, Saarbrücken, Germany, March 21-24, 2016, (2016)), 147-162
[33] Devriese, D.; Piessens, F., Noninterference through secure multi-execution, (1st IEEE Symposium on Security and Privacy, S&P 2010, 16-19 May 2010, Berleley/Oakland, California, USA, (2010)), 109-124
[34] Fett, D.; Küsters, R.; Schmitz, G., An expressive model for the web infrastructure: definition and application to the browserid SSO system, (2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, May 18-21, 2014, (2014)), 673-688
[35] Fett, D.; Küsters, R.; Schmitz, G., Analyzing the browserid SSO system with primary identity providers using an expressive model of the web, (Computer Security - ESORICS 2015 - 20th European Symposium on Research in Computer Security, Vienna, Austria, September 21-25, 2015, Proceedings, Part I, (2015)), 43-65
[36] Filaretti, D.; Maffeis, S., An executable formal semantics of PHP, (ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28- August 1, 2014. Proceedings, (2014)), 567-592
[37] Fournet, C.; Swamy, N.; Chen, J.; Dagand, P.; Strub, P.; Livshits, B., Fully abstract compilation to javascript, (The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, Rome, Italy - January 23-25, 2013, (2013)), 371-384 · Zbl 1301.68100
[38] Gardner, P.; Smith, G.; Wheelhouse, M. J.; Zarfaty, U., DOM: towards a formal specification, (PLAN-X 2008, Programming Language Technologies for XML, an ACM SIGPLAN Workshop Colocated with POPL 2008, San Francisco, California, USA, January 9, 2008, (2008))
[39] Grier, C.; Tang, S.; King, S. T., Designing and implementing the OP and OP2 web browsers, ACM Trans. Web, 5, 2, 11, (2011)
[40] Groef, W. D.; Devriese, D.; Nikiforakis, N.; Piessens, F., Flowfox: a web browser with flexible and precise information flow control, (The ACM Conference on Computer and Communications Security, CCS’12, Raleigh, NC, USA, October 16-18, 2012, (2012)), 748-759
[41] Groß, T.; Pfitzmann, B.; Sadeghi, A., Browser model for security analysis of browser-based protocols, (Computer Security - ESORICS 2005, 10th European Symposium on Research in Computer Security, Milan, Italy, September 12-14, 2005, Proceedings, (2005)), 489-508
[42] Groß, T.; Pfitzmann, B.; Sadeghi, A., Proving a WS-federation passive requestor profile with a browser model, (Proceedings of the 2nd ACM Workshop on Secure Web Services, SWS 2005, Fairfax, VA, USA, November 11, 2005, (2005)), 54-64
[43] Guha, A.; Fredrikson, M.; Livshits, B.; Swamy, N., Verified security for browser extensions, (32nd IEEE Symposium on Security and Privacy, S&P 2011, 22-25 May 2011, Berkeley, California, USA, (2011)), 115-130
[44] Guha, A.; Saftoiu, C.; Krishnamurthi, S., The essence of javascript, (ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings, (2010)), 126-150
[45] Hedin, D.; Sabelfeld, A., Information-flow security for a core of javascript, (25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012, (2012)), 25-27
[46] Huang, Y.; Yu, F.; Hang, C.; Tsai, C.; Lee, D.; Kuo, S., Securing web application code by static analysis and runtime protection, (Proceedings of the 13th International Conference on World Wide Web, WWW 2004, New York, NY, USA, May 17-20, 2004, (2004)), 40-52
[47] Jackson, D., Alloy: a lightweight object modelling notation, ACM Trans. Softw. Eng. Methodol., 11, 2, 256-290, (2002)
[48] Jang, D.; Tatlock, Z.; Lerner, S., Establishing browser security guarantees through formal shim verification, (Proceedings of the 21th USENIX Security Symposium, Bellevue, WA, USA, August 8-10, 2012, (2012)), 113-128
[49] Jovanovic, N.; Krügel, C.; Pixy, E. Kirda, A static analysis tool for detecting web application vulnerabilities (short paper), (2006 IEEE Symposium on Security and Privacy, S&P 2006, 21-24 May 2006, Berkeley, California, USA, (2006)), 258-263
[50] Lerner, B. S.; Elberty, L.; Poole, N.; Krishnamurthi, S., Verifying web browser extensions’ compliance with private-browsing mode, (Computer Security - ESORICS 2013 - 18th European Symposium on Research in Computer Security, Egham, UK, September 9-13, 2013. Proceedings, (2013)), 57-74
[51] Lerner, B. S.; Politz, J. G.; Guha, A.; Krishnamurthi, S., Tejas: retrofitting type systems for javascript, (DLS’13, Proceedings of the 9th Symposium on Dynamic Languages, Part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, (2013)), 1-16
[52] Lowe, G., Breaking and fixing the needham-schroeder public-key protocol using FDR, Softw., Concepts Tools, 17, 3, 93-102, (1996)
[53] Luo, Z.; Rezk, T.; Serrano, M., Automated code injection prevention for web applications, (Theory of Security and Applications - Joint Workshop, TOSCA 2011, Saarbrücken, Germany, March 31-April 1, 2011, Revised Selected Papers, (2011)), 186-204
[54] Luo, Z.; Santos, J. F.; Matos, A. A.; Rezk, T., Mashic compiler: mashup sandboxing based on inter-frame communication, J. Comput. Secur., 24, 1, 91-136, (2016)
[55] Lynch, N. A.; Tuttle, M. R., Hierarchical correctness proofs for distributed algorithms, (Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, Vancouver, British Columbia, Canada, August 10-12, 1987, (1987)), 137-151
[56] Maffeis, S.; Mitchell, J. C.; Taly, A., An operational semantics for javascript, (Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008, Proceedings, (2008)), 307-325
[57] Maffeis, S.; Mitchell, J. C.; Taly, A., Isolating javascript with filters, rewriting, and wrappers, (Computer Security - ESORICS 2009, 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009, Proceedings, (2009)), 505-522
[58] Maffeis, S.; Mitchell, J. C.; Taly, A., Object capabilities and isolation of untrusted web applications, (31st IEEE Symposium on Security and Privacy, S&P 2010, 16-19 May 2010, Berleley/Oakland, California, USA, (2010)), 125-140
[59] Maffeis, S.; Taly, A., Language-based isolation of untrusted javascript, (Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8-10, 2009, (2009)), 77-91
[60] Matos, A. G.A.; Santos, J. F.; Rezk, T., An information flow monitor for a core of DOM - introducing references and live primitives, (Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014, (2014)), 1-16
[61] Meseguer, J., Conditioned rewriting logic as a united model of concurrency, Theor. Comput. Sci., 96, 1, 73-155, (1992) · Zbl 0758.68043
[62] Meseguer, J.; Sasse, R.; Wang, H. J.; Wang, Y., A systematic approach to uncover security flaws in GUI logic, (2007 IEEE Symposium on Security and Privacy, S&P 2007, 20-23 May 2007, Oakland, California, USA, (2007)), 71-85
[63] Microsoft. LINQ (language-integrated query), (2015), Available at
[64] Murphy VII, T.; Crary, K.; Harper, R., Type-safe distributed programming with ML5, (Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, (2007)), 108-123
[65] Nikiforakis, N.; Invernizzi, L.; Kapravelos, A.; Acker, S. V.; Joosen, W.; Kruegel, C.; Piessens, F.; Vigna, G., You are what you include: large-scale evaluation of remote javascript inclusions, (The ACM Conference on Computer and Communications Security, CCS’12, Raleigh, NC, USA, October 16-18, 2012, (2012)), 736-747
[66] OASIS, SAML specification, (2005), Available at
[67] Openid specification, (2014), Available at
[68] Park, D.; Stefanescu, A.; Rosu, G., KJS: a complete formal semantics of javascript, (Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, (2015)), 346-356
[69] Phung, P. H.; Sands, D.; Chudnov, A., Lightweight self-protecting javascript, (Proceedings of the 2009 ACM Symposium on Information, Computer and Communications Security, ASIACCS 2009, Sydney, Australia, March 10-12, 2009, (2009)), 47-60
[70] Politz, J. G.; Carroll, M. J.; Lerner, B. S.; Pombrio, J.; Krishnamurthi, S., A tested semantics for getters, setters, and eval in javascript, (Proceedings of the 8th Symposium on Dynamic Languages, LS ’12, Tucson, AZ, USA, October 22, 2012, (2012)), 1-16
[71] Politz, J. G.; Guha, A.; Krishnamurthi, S., Typed-based verification of web sandboxes, J. Comput. Secur., 22, 4, 511-565, (2014)
[72] Politz, J. G.; Martinez, A.; Milano, M.; Warren, S.; Patterson, D.; Li, J.; Chitipothu, A.; Krishnamurthi, S., Python: the full monty, (Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, Part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, (2013)), 217-232
[73] Rajani, V.; Bichhawat, A.; Garg, D.; Hammer, C., Information flow control for event handling and the DOM in web browsers, (IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July, 2015, (2015)), 366-379
[74] Ray, D.; Ligatti, J., Defining code-injection attacks, (Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, (2012)), 179-190 · Zbl 1321.68035
[75] Richards, G.; Hammer, C.; Burg, B.; Vitek, J., The eval that men do - a large-scale study of the use of eval in javascript applications, (ECOOP 2011 - Object-Oriented Programming - 25th European Conference, Lancaster, UK, July 25-29, 2011, Proceedings, (2011)), 52-78
[76] Roşu, G.; Şerbănuţă, T. F., An overview of the K semantic framework, J. Log. Algebraic Program., 79, 6, 397-434, (2010) · Zbl 1214.68188
[77] Russo, A.; Sabelfeld, A.; Chudnov, A., Tracking information flow in dynamic tree structures, (Computer Security - ESORICS 2009, 14th European Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009, Proceedings, (2009)), 86-103
[78] Sasse, R.; King, S. T.; Meseguer, J.; Tang, S., IBOS: a correct-by-construction modular browser, (Formal Aspects of Component Software, 9th International Symposium, FACS 2012, Mountain View, CA, USA, September 12-14, 2012, Revised Selected Papers, (2012)), 224-241
[79] Schoepe, D.; Hedin, D.; Sabelfeld, A., Selinq: tracking information across application-database boundaries, (Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 1-3, 2014, (2014)), 25-38 · Zbl 1346.68065
[80] Singh, K.; Moshchuk, A.; Wang, H. J.; Lee, W., On the incoherencies in web browser access control policies, (31st IEEE Symposium on Security and Privacy, S&P 2010, 16-19 May 2010, Berleley/Oakland, California, USA, (2010)), 463-478
[81] Su, Z.; Wassermann, G., The essence of command injection attacks in web applications, (Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, (2006)), 372-382 · Zbl 1369.68158
[82] Swamy, N.; Chen, J.; Fournet, C.; Strub, P.; Bhargavan, K.; Yang, J., Secure distributed programming with value-dependent types, J. Funct. Program., 23, 4, 402-451, (2013) · Zbl 1290.68033
[83] Swamy, N.; Fournet, C.; Rastogi, A.; Bhargavan, K.; Chen, J.; Strub, P.; Bierman, G. M., Gradual typing embedded securely in javascript, (The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, (2014)), 425-438 · Zbl 1284.68108
[84] Taly, A.; Erlingsson, Ú.; Mitchell, J. C.; Miller, M. S.; Nagra, J., Automated analysis of security-critical javascript apis, (32nd IEEE Symposium on Security and Privacy, S&P 2011, 22-25 May 2011, Berkeley, California, USA, (2011)), 363-378
[85] The World Wide Web Consortium, HTML5 specification, (2015), Available at
[86] Tobarra, M. L.; Cazorla, D.; Cuartero, F.; Díaz, G., Application of formal methods to the analysis of web services security, (Formal Techniques for Computer Systems and Business Processes, European Performance Engineering Workshop, EPEW 2005 and International Workshop on Web Services and Formal Methods, WS-FM 2005, Versailles, France, September 1-3, 2005, Proceedings, (2005)), 215-229
[87] Tobarra, M. L.; Cazorla, D.; Cuartero, F.; Díaz, G., Analysis of web services secure conversation with formal methods, (International Conference on Internet and Web Applications and Services, ICIW 2007, May 13-19, 2007, Le Morne, Mauritius, (2007)), 27
[88] Viganò, L., Automated security protocol analysis with the AVISPA tool, Electron. Notes Theor. Comput. Sci., 155, 61-86, (2006)
[89] WSS Technical Committee, WS-security specification, (2006), Available at
[90] Yoshihama, S.; Tateishi, T.; Tabuchi, N.; Matsumoto, T., Information-flow-based access control for web browsers, IEICE Trans., 92-D, 5, 836-850, (2009)
[91] Yu, D.; Chander, A.; Islam, N.; Serikov, I., Javascript instrumentation for browser security, (Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, (2007)), 237-249 · Zbl 1295.68056
[92] Zheng, X.; Jiang, J.; Liang, J.; Duan, H.; Chen, S.; Wan, T.; Weaver, N., Cookies lack integrity: real-world implications, (24th USENIX Security Symposium, USENIX Security 15, Washington, DC, USA, August 12-14, 2015, (2015)), 707-721
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.