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

3. Challenges for formal methods
The semantics of JavaScript includes many quirks and surprises. For instance, the + operator performs several type co ercions
and is heavily overloaded, resulting in a specification based on a 15-step algorithm using meta-functions spanning three pages: we
refer to
[44]
for an interesting discussion about this and other peculiarities of the language. Moreover, there are often inconsistencies
between different browser implementations of the JavaScript engine, which lead to the same JavaScript program behaving slightly
differently on different web browsers. For these reasons, several research papers advo cate the usage of more disciplined programming
languages to develop the client-side part of a web application. To ensure backward compatibility with existing web browsers, these
languages are either securely compiled to JavaScript
[37,83,43]
or amount to well-behaved JavaScript subsets enjoying some form
of type safety
[12].
4.1.1. A fully abstract compilation to JavaScript
[37]
2. cross-site request forgery (CSRF): since the SOP does not constrain cross-site requests, a page from
http: // attacker. com
can
force the browser into sending HTTP (S) requests to
http://trusted.com.
Since all these auto requests automatically include
cookies previously set by the latter website, they will be considered part of the session between the user browser and
http://
trusted.com.
These requests may thus be abused to trigger dangerous side-effects on the website on the user's behalf.
tioning only two notable examples:
1. code injection: a missing or flawed sanitization of user inputs in a web application may lead to the inclusion of attacker controlled
contents into benign web pages. Since these injected contents are indistinguishable from legitimate ones and inherit their origin,
they may be entitled to access sensitive data provided by the benign pages, eg, cookies, without violating the SOP. The injection
of malicious JavaScript code is one of the most pervasive attacks on the Web, known as cross-site scripting (XSS);
4.1. RL1: security by construction
Unfortunately, the SOP is not enough to prevent many common attacks. For our present endeavors, it is worth men