Language-Based Web Session Integrity
We propose a static analysis technique to enforce session integrity on web applications.
We recently presented our latest work on web session security (PDF) at the 33rd IEEE Computer Security Foundations Symposium which, due to the ongoing Covid-19 pandemic, this year took place exclusively online.
Web session management is a fundamental component of any modern web application. A web session is established upon login, when a user provides her credentials (username/password) to prove her identity. After this authentication step, the web application sets into the user’s browser a cookie, which identifies the user, that is automatically attached to all the subsequent requests towards the website. In this way, a user can perform multiple operations on a website without providing her credentials at every step.
Since the Web infrastructure does not provide built-in support for session management, web applications have to implement their own management logic which, in the past, often proved to be vulnerable to a variety of attacks.
In the most severe cases, the attacker manages to obtain full control over a web session, e.g., if she manages to steal either the login credentials or the cookie that identifies the session. Another well-known attack is known as cross-site request forgery (CSRF), where the attacker can force the browser of a victim to produce requests (indistinguishable from legitimate ones) triggering dangerous side-effects to websites where the victim has an active session – for instance, the attacker may produce an online bank transfer without that the victim even notices it. Another class of attacks consists in logging a victim into an account that belongs to an attacker in order to steal some sensitive information that the user could provide while interacting with the website – for example, the search history in a search engine, or a newly registered credit card in an online shop.
To prevent these different attacks against web sessions, we propose a novel framework for the analysis of web applications. Our approach is built upon a type system for a formal encoding of web application code, which at its core makes use of techniques from the area of information flow control. The main theoretical result of our paper says that an application that satisfies the typing rules is not affected by session integrity vulnerabilities.
Through our research, we uncovered novel vulnerabilities in real world applications, including the conference management system HotCRP which, ironically, is the system used to submit this work to the conference! These vulnerabilities could be exploited to take full control over the account of a victim. We then proposed a fixed version of the application, and proved – using our framework – that the fixed version is no more vulnerable to the identified threats.