The complexity of browsers has steadily increased over the years, driven by the continuous introduction and update of Web platform components, such as novel Web APIs and security mechanisms. Their specifications are manually reviewed by experts to identify potential security issues. However, this process has proved to be error-prone due to the extensiveness of modern browser specifications and the interplay between new and existing Web platform components. To tackle this problem, we developed WebSpec, the first formal security framework for the analysis of browser security mechanisms, which enables both the automatic discovery of logical flaws and the development of machine-checked security proofs. WebSpec, in particular, includes a comprehensive semantic model of the browser in the Coq proof assistant, a formalization in this model of ten Web security invariants, and a compiler turning the Coq model and the Web invariants into SMT-lib formulas. We showcase the effectiveness of WebSpec by discovering two new logical flaws caused by the interaction of different browser mechanisms and by identifying three previously discovered logical flaws in the current Web platform, as well as five in old versions. Finally, we show how WebSpec can aid the verification of our proposed changes to amend the reported inconsistencies affecting the current Web platform.

翻译：多年来,浏览器的复杂程度稳步增加,这得益于不断引入和更新网络平台组件,如新版网页API和安全机制等,浏览器的复杂程度多年来不断提高,其复杂性在不断引入和更新的网络平台组件,如新版网页API和安全机制的驱动下稳步提高,其规格由专家手工审查,以确定潜在的安全问题。然而,由于现代浏览器规格的广泛性以及新的和现有的网络平台组件之间的相互作用,这一过程证明容易出错。为了解决这个问题,我们开发了WebSpec,这是用于分析浏览器安全机制分析的第一个正式安全框架,它使得能够自动发现逻辑缺陷并开发机器检查的安全证明。 WebSpec尤其包括了Coq验证助理中浏览器的全面语义模型,将10个网络安全变量的模型正式化,以及一个将 Coq 模型和 Web 变量转换成SMT-lib 公式的汇编者。我们展示了WebSpec