Web security

The security of the Web is a problem of paramount importance in the digital society, given its social and economic relevance. Over the last decades, the Web evolved from a mesh of interconnected documents to the largest application distribution platform. Unfortunately, the growing complexity caused by this transformation underlies a gigantic attack surface, ranging from network infrastructures to browsers running modern client-side applications, which hinders a systematic and rigorous enforcement of security and privacy properties. Our research tackles foundational aspects of Web security and more pressing challenges, combining various disciplines and delivering practical impact.

Formal Verification

Web protocols and standards serve as the foundation of modern Web applications. A security flaw in a specification translates into a vulnerability in compliant implementations, disrupting security and privacy guarantees in the Web ecosystem. Despite this, Web specifications typically undergo only manual expert review to identify potential issues. Due to the evolving nature of the Web, this process must often be revised, e.g., whenever new components and API land on the Web platform. As a result, such continuous and complex activity tends to overlook logical flaws.

Our research aims to develop rigorous frameworks and formal models for the automated detection of logical flaws, as well as machine-checked security proofs. As opposed to manual review, formal security analysis enables us to (i) precisely define the relevant security properties of a system, (ii) consider the entangled nature of the Web platform by taking into account the interaction between different components, and (iii) capture corner cases that could be easily overlooked.

Empirical Evaluation

Understanding the impact of security flaws found at the specification level requires a thorough investigation of real applications. Security vulnerabilities can also be introduced due to discrepancies between specifications and implementations or caused by other flaws in server or client-side applications.

Our research group employs white-box and black-box analysis techniques to test security properties of Web frameworks and applications. We also investigate cross-browser inconsistencies to detect browser behaviors that could lead to violating the security and privacy of end users. To support our findings, we routinely perform large-scale evaluations on prevalent websites to accurately understand how modern Web services are deployed and measure the impact of the discovered threats.

Mobile/Web Security

While standard desktop platforms rely on the browser as the first-hand means to access websites, the mobile ecosystem is more diverse and supports multiple mechanisms to mesh Web resources and mobile apps. However, bridging mobile native apps and Web content can have unforeseen consequences.

For this reason, security analysis of mobile apps and Web security cannot be performed in isolation but need to be considered in unison. We investigate new ways that Web and mobile apps can interact and how attackers could abuse these mechanisms to either exploit security vulnerabilities to escalate their privileges on a device or obtain novel capabilities previously unavailable to standard Web attackers.

Main directions of our research include: