As it normally happens in computer science, when some kind of process is too error-prone

9. Conclusion
[6]
IG Baltopoulos, AD Gordon, Secure compilation of a multi-tier web language, in: Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop
evaluate this important aspect. The point is that, like any form of testing, practical evaluations on the Web are inherently limited and they are better complemented
by formal analysis.
and Application Security and Privacy, CODASPY 2016, New Orleans, LA, USA, March 9–11, 2016, 2016, pp. 307–318.
References
thank Sergio Maffeis, Frank Piessens and Andrei Sabelfeld for their valuable feedback on an early draft of this work.
We would like to thank the anonymous reviewers for their careful reading and precise comments. We would also like to
Acknowledgements
and remediations, Comput. Secur. 33 (2013) 41–58.
[3]
A. Armando, R. Carbone, L. Compagna, J. Cuéllar, G. Pellegrino, A. Sorniotti, An authentication flaw in browser-based single sign-on protocols: impact
Machine Translated by Google

---

[33]
D. Devriese, F. Piessens, Noninterference through secure multi-execution, in: 1st IEEE Symposium on Security and Privacy, S&P 2010, 16–19 May 2010,
[20]
G. Boudol, Z. Luo, T. Rezk, M. Serrano, Reasoning about web applications: an operational semantics for HOP, ACM Trans. Program. Lang. Syst. 34 (2)
on Security and Privacy, EuroS & P 2016, Saarbrücken, Germany, March 21–24, 2016, 2016, pp. 147–162.
22–25 May 2011, Berkeley, California, USA, 2011, pp. 115–130.
[55]
NA Lynch, MR Tuttle, Hierarchical correctness proofs for distributed algorithms, in: Proceedings of the Sixth Annual ACM Symposium on Principles
[25] S. Cantor, M. Erdos, Shibboleth specification, Available at
https://shibboleth.net/,
2015.
[37]
C. Fournet, N. Swamy, J. Chen, P. Dagand, P. Strub, B. Livshits, Fully abstract compilation to JavaScript, in: The 40th Annual ACM SIGPLAN-SIGACT
[47]
D. Jackson, Alloy: a lightweight object modeling notation, ACM Trans. Softw. Eng. Methodol. 11 (2) (2002) 256–290.
(2012) 10.
[34]
D. Fett, R. Küsters, G. Schmitz, An expressive model for the web infrastructure: definition and application to the BrowserID SSO system, in: 2014 IEEE
bridge, MA, USA, June 25–27, 2012, 2012, pp. 25–27.
[28]
A. Chlipala, Ur / web: a simple model for programming the web, in: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of
[39]
C. Grier, S. Tang, ST King, Designing and implementing the OP and OP2 web browsers, ACM Trans. Web 5 (2) (2011) 11.
[50]
BS Lerner, L. Elberty, N. Poole, S. Krishnamurthi, Verifying web browser extensions' compliance with private-browsing mode, in: Computer Security - ESORICS
2013 - 18th European Symposium on Research in Computer Security, Egham, UK , September 9–13, 2013. Proceedings, 2013, pp. 57–74.
[26]
EY Chen, J. Bau, C. Reis, A. Barth, C. Jackson, App isolation: get the security of multiple browsers with just one, in: Proceedings of the 18th ACM Conference on
Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17–21, 2011, 2011, pp. 227–238.
Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23–25, 2013, 2013, pp. 371–384.
[48]
D. Jang, Z. Tatlock, S. Lerner, Establishing browser security guarantees through formal shim verification, in: Proceedings of the 21st USENIX Security Symposium,
Bellevue, WA, USA, August 8–10, 2012, 2012, pp . 113–128.
[21]
M. Bugliesi, S. Calzavara, R. Focardi, W. Khan, CookiExt: patching the browser against session hijacking attacks, J. Comput. Secur. 23 (4) (2015) 509–537.
125
[30]
BJ Corcoran, N. Swamy, MW Hicks, Cross-tier, label-based security enforcement for web applications, in: Proceedings of the ACM SIGMOD International
Conference on Data Management, SIGMOD 2009, Providence, Rhode Island, USA , June 29 – July 2, 2009, 2009, pp. 269–282.
[42]
T. Groß, B. Pfitzmann, A. Sadeghi, Proving a WS-federation passive requestor profile with a browser model, in: Proceedings of the 2nd ACM Workshop
[54]
Z. Luo, JF Santos, AA Matos, T. Rezk, Mashic compiler: mashup sandboxing based on inter-frame communication, J. Comput. Secur. 24 (1) (2016)
[51]
BS Lerner, JG Politz, A. Guha, S. Krishnamurthi, TeJaS: retrofitting type systems for JavaScript, in: DLS'13, Proceedings of the 9th Symposium on
[24]
S. Calzavara, G. Tolomei, A. Casini, M. Bugliesi, S. Orlando, A supervised learning approach to protect client authentication on the web, ACM Trans. Web
[35]
D. Fett, R. Küsters, G. Schmitz, Analyzing the BrowserID SSO system with primary identity providers using an expressive model of the web, in: Com puter Security
- ESORICS 2015 - 20th European Symposium on Research in Computer Security, Vienna, Austria, September 21–25, 2015, Proceedings, Part I, 2015, pp. 43–65.
[46]
Y. Huang, F. Yu, C. Hang, C. Tsai, D. Lee, S. Kuo, Securing web application code by static analysis and runtime protection, in: Proceedings of the 13th
Berleley / Oakland, California, USA, 2010, pp. 109–124.
[44]
A. Guha, C. Saftoiu, S. Krishnamurthi, The essence of JavaScript, in: ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor,
of Distributed Computing, Vancouver, British Columbia, Canada, August 10–12, 1987, 1987, pp. 137–151.
Programming Languages, POPL 2015, Mumbai, India, January 15–17, 2015, 2015, pp. 153–165.
[40]
WD Groef, D. Devriese, N. Nikiforakis, F. Piessens, FlowFox: a web browser with flexible and precise information flow control, in: The ACM Conference on Computer
and Communications Security, CCS'12, Raleigh, NC, USA, October 16–18, 2012, 2012, pp. 748–759.
[27]
A. Chlipala, Static checking of dynamically-varying security policies in database-backed applications, in: 9th USENIX Symposium on Operating Systems
[38]
P. Gardner, G. Smith, MJ Wheelhouse, U. Zarfaty, DOM: towards a formal specification, in: PLAN-X 2008, Programming Language Technologies for XML,
[49]
N. Jovanovic, C. Krügel, E. Kirda Pixy, A static analysis tool for detecting web application vulnerabilities (short paper), in: 2006 IEEE Symposium on
[18]
A. Bohannon, Foundations of webscript security, PhD thesis, University of Pennsylvania, 2012.
[31]
P. De Ryck, L. Desmet, W. Joosen, F. Piessens, Automatic and precise client-side protection against CSRF attacks, in: Computer Security - ESORICS 2011 - 16th
European Symposium on Research in Computer Security, Leuven, Belgium, September 12–14, 2011, Proceedings, 2011, pp. 100–116.
on Secure Web Services, SWS 2005, Fairfax, VA, USA, November 11, 2005, 2005, pp. 54–64.
Dynamic Languages, Part of SPLASH 2013, Indianapolis, IN, USA, October 26–31, 2013, 2013, pp. 1–16.
[29]
E. Cooper, S. Lindley, P. Wadler, J. Yallop, Links: web programming without tiers, in: Formal Methods for Components and Objects, 5th International
[41]
T. Groß, B. Pfitzmann, A. Sadeghi, Browser model for security analysis of browser-based protocols, in: Computer Security - ESORICS 2005, 10th Euro
[52]
G. Lowe, Breaking and fixing the Needham – Schroeder public-key protocol using FDR, Softw., Concepts Tools 17 (3) (1996) 93–102.
[22]
M. Bugliesi, S. Calzavara, R. Focardi, W. Khan, M. Tempesta, Provably sound browser-based implementation of web session integrity, in: IEEE 27th Computer
Security Foundations Symposium, CSF 2014, Vienna, Austria, 19–22 July, 2014, 2014, pp. 366–380.
Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, May 18–21, 2014, 2014, pp. 673–688.
Slovenia, June 21–25, 2010. Proceedings, 2010, pp. 126–150.
[56]
S. Maffeis, JC Mitchell, A. Taly, An operational semantics for JavaScript, in: Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore,
India, December 9–11, 2008, Proceedings, 2008, pp . 307–325.
[19]
A. Bohannon, BC Pierce, Featherweight Firefox: formalizing the core of a web browser, in: USENIX Conference on Web Application Development, WebApps'10,
Boston, Massachusetts, USA, June 23–24, 2010, 2010.
[32]
D. Devriese, L. Birkedal, F. Piessens, Reasoning about object capabilities with logical relations and effect parametricity, in: IEEE European Symposium
[43]
A. Guha, M. Fredrikson, B. Livshits, N. Swamy, Verified security for browser extensions, in: 32nd IEEE Symposium on Security and Privacy, S&P 2011,
91–136.
Design and Implementation, OSDI 2010, October 4–6, 2010, Vancouver, BC, Canada, Proceedings, 2010, pp. 105–118.
9 (3) (2015) 15.
[36]
D. Filaretti, S. Maffeis, An executable formal semantics of PHP, in: ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden,
July 28– August 1, 2014. Proceedings, 2014, pp. 567–592.
International Conference on World Wide Web, WWW 2004, New York, NY, USA, May 17–20, 2004, 2004, pp. 40–52.
[45]
D. Hedin, A. Sabelfeld, Information-flow security for a core of JavaScript, in: 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cam