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

M. Bugliesi et al. / Journal of Logical and Algebraic Methods in Programming 87 (2017) 110–126
Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7–10, 2006, Revised Lectures, 2006, pp. 266–296.
pean Symposium on Research in Computer Security, Milan, Italy, September 12–14, 2005, Proceedings, 2005, pp. 489–508.
[53]
Z. Luo, T. Rezk, M. Serrano, Automated code injection prevention for web applications, in: Theory of Security and Applications - Joint Workshop, TOSCA 2011,
Saarbrücken, Germany, March 31 – April 1, 2011, Revised Selected Papers, 2011, pp. 186–204.
an ACM SIGPLAN Workshop Colocated with POPL 2008, San Francisco, California, USA, January 9, 2008, 2008.
Security and Privacy, S&P 2006, 21–24 May 2006, Berkeley, California, USA, 2006, pp. 258–263.
[23]
S. Calzavara, M. Bugliesi, S. Crafa, E. Steffinlongo, Fine-grained detection of privilege escalation attacks on browser extensions, in: Programming Lan guages 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, pp. 510–534.
Machine Translated by Google

---

[74]
D. Ray, J. Ligatti, Defining code-injection attacks, in: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Lan
[58]
S. Maffeis, JC Mitchell, A. Taly, Object capabilities and isolation of untrusted web applications, in: 31st IEEE Symposium on Security and Privacy, S&P
[71]
JG Politz, A. Guha, S. Krishnamurthi, Typed-based verification of web sandboxes, J. Comput. Secur. 22 (4) (2014) 511–565.
(2013) 402–451.
USENIX Security 15, Washington, DC, USA, August 12–14, 2015, 2015, pp. 707–721.
[62]
J. Meseguer, R. Sasse, HJ Wang, Y. Wang, A systematic approach to uncover security flaws in GUI logic, in: 2007 IEEE Symposium on Security and
[76]
G. Ro ¸su, TF Serb
anu
[77]
A. Russo, A. Sabelfeld, A. Chudnov, Tracking information flow in dynamic tree structures, in: Computer Security - ESORICS 2009, 14th European
[84]
A. Taly, Ú. Erlingsson, JC Mitchell, MS Miller, J. Nagra, Automated analysis of security-critical JavaScript APIs, in: 32nd IEEE Symposium on Security
[60]
AGA Matos, JF Santos, T. Rezk, An information flow monitor for a core of DOM - introducing references and live primitives, in: Trustworthy Global
guages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22–28, 2012, 2012, pp. 179–190.
[79]
D. Schoepe, D. Hedin, A. Sabelfeld, SeLINQ: tracking information across application-database boundaries, in: Proceedings of the 19th ACM SIGPLAN
Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, 2007, pp. 108–123.
Symposium on Research in Computer Security, Saint-Malo, France, September 21-23, 2009, Proceedings, 2009, pp. 86–103.
[87]
ML Tobarra, D. Cazorla, F. Cuartero, G. Díaz, Analysis of web services secure conversation with formal methods, in: International Conference on
Privacy, S&P 2007, 20–23 May 2007, Oakland, California, USA, 2007, pp. 71–85.
ÿ
and Privacy, S&P 2011, 22–25 May 2011, Berkeley, California, USA, 2011, pp. 363–378.
2010, 16–19 May 2010, Berleley / Oakland, California, USA, 2010, pp. 125–140.
M. Bugliesi et al. / Journal of Logical and Algebraic Methods in Programming 87 (2017) 110–126
[68]
D. Park, A. Stefanescu, G. Rosu, KJS: a complete formal semantics of JavaScript, in: Proceedings of the 36th ACM SIGPLAN Conference on Programming
Language Design and Implementation, Portland, OR, USA, June 15–17 , 2015, 2015, pp. 346–356.
[81]
Z. Su, G. Wassermann, The essence of command injection attacks in web applications, in: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium
[90]
S. Yoshihama, T. Tateishi, N. Tabuchi, T. Matsumoto, Information-flow-based access control for web browsers, IEICE Trans. 92-D (5) (2009) 836–850.
Internet and Web Applications and Services, ICIW 2007, May 13–19, 2007, Le Morne, Mauritius, 2007, p. 27.
Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5–6, 2014, 2014, pp. 1–16.
[75]
G. Richards, C. Hammer, B. Burg, J. Vitek, The eval that men do - a large-scale study of the use of eval in JavaScript applications, in: ECOOP 2011 -
[80]
K. Singh, A. Moshchuk, HJ Wang, W. Lee, On the incoherencies in web browser access control policies, in: 31st IEEE Symposium on Security and
[72]
JG Politz, A. Martinez, M. Milano, S. Warren, D. Patterson, J. Li, A. Chitipothu, S. Krishnamurthi, Python: the full monty, in: 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, pp. 217–232.
¸
[92]
X. Zheng, J. Jiang, J. Liang, H. Duan, S. Chen, T. Wan, N. Weaver, Cookies lack integrity: real-world implications, in: 24th USENIX Security Symposium,
[65]
N. Nikiforakis, L. Invernizzi, A. Kapravelos, SV Acker, W. Joosen, C. Kruegel, F. Piessens, G. Vigna, You are what you include: large-scale evaluation of remote
JavaScript inclusions, in : The ACM Conference on Computer and Communications Security, CCS'12, Raleigh, NC, USA, October 16–18, 2012, 2012, pp. 736–747.
Symposium, FACS 2012, Mountain View, CA, USA, September 12–14, 2012, Revised Selected Papers, 2012, pp. 224–241.
[63] Microsoft. LINQ (language-integrated query), Available at
https://msdn.microsoft.com/it-it/library/bb397926.aspx,
2015.
ÿ
[85] The World Wide Web Consortium, HTML5 specification, Available at
http://www.w3.org/TR/html5/,
2015.
[57]
S. Maffeis, JC Mitchell, A. Taly, Isolating JavaScript with filters, rewriting, and wrappers, in: Computer Security - ESORICS 2009, 14th European
[69]
PH Phung, D. Sands, A. Chudnov, Lightweight self-protecting JavaScript, in: Proceedings of the 2009 ACM Symposium on Information, Computer and
Communications Security, ASIACCS 2009, Sydney, Australia, March 10–12, 2009, 2009, pp. 47–60.
on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11–13, 2006, 2006, pp. 372–382.
[91]
D. Yu, A. Chander, N. Islam, I. Serikov, JavaScript instrumentation for browser security, in: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium
[66] OASIS, SAML specification, Available at
http://saml.xml.org/saml-specifications,
2005.
International Conference on Functional Programming, Gothenburg, Sweden, September 1–3, 2014, 2014, pp. 25–38.
[88]
L. Viganò, Automated security protocol analysis with the AVISPA tool, Electron. Notes Theor. Comput. Sci. 155 (2006) 61–86.
[59]
S. Maffeis, A. Taly, Language-based isolation of untrusted JavaScript, in: Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF
[73]
V. Rajani, A. Bichhawat, D. Garg, C. Hammer, Information flow control for event handling and the DOM in web browsers, in: IEEE 28th Computer Security
Foundations Symposium, CSF 2015, Verona, Italy, 13– July 17, 2015, 2015, pp. 366–379.
¸
Symposium on Research in Computer Security, Saint-Malo, France, September 21–23, 2009, Proceedings, 2009, pp. 505–522.
[70]
JG Politz, MJ Carroll, BS Lerner, J. Pombrio, S. Krishnamurthi, A tested semantics for getters, setters, and eval in JavaScript, in: Proceedings of the 8th Symposium
on Dynamic Languages, LS '12, Tucson, AZ, USA, October 22, 2012, 2012, pp. 1–16.
[82]
N. Swamy, J. Chen, C. Fournet, P. Strub, K. Bhargavan, J. Yang, Secure distributed programming with value-dependent types, J. Funct. Program. 23 (4)
on Principles of Programming Languages, POPL 2007, Nice, France, January 17–19, 2007, 2007, pp. 237–249.
[64]
T. Murphy VII, K. Crary, R. Harper, Type-safe distributed programming with ML5, in: Trustworthy Global Computing, Third Symposium, TGC 2007,
[61]
J. Meseguer, Conditioned rewriting logic as a united model of concurrency, Theor. Comput. Sci. 96 (1) (1992) 73–155.
Object-Oriented Programming - 25th European Conference, Lancaster, UK, July 25–29, 2011, Proceedings, 2011, pp. 52–78.
[83]
N. Swamy, C. Fournet, A. Rastogi, K. Bhargavan, J. Chen, P. Strub, GM Bierman, Gradual typing embedded securely in JavaScript, in: The 41st Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20–21, 2014, 2014, pp. 425–438.
[78]
R. Sasse, ST King, J. Meseguer, S. Tang, IBOS: a correct-by-construction modular browser, in: Formal Aspects of Component Software, 9th International
126
[67] OpenID Working Groups, OpenID specification, Available at
http://openid.net/developers/specs/,
2014.
Privacy, S&P 2010, 16–19 May 2010, Berleley / Oakland, California, USA, 2010, pp. 463–478.
[89] WSS Technical Committee, WS-security specification, Available at
https://www.oasis-open.org/committees/tc_home.php?wg_abbrev=wss,
2006.
ta, An overview of the K semantic framework, J. Log. Algebraic Program. 79 (6) (2010) 397–434.
[86]
ML Tobarra, D. Cazorla, F. Cuartero, G. Díaz, Application of formal methods to the analysis of web services security, in: 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, pp. 215–229.
2009, Port Jefferson, New York, USA, July 8–10, 2009, 2009, pp. 77–91.
Machine Translated by Google