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 toolchain turning the Coq model and the Web invariants into SMT-lib formulas to enable model checking with the Z3 theorem prover. If a violation is found, the toolchain automatically generates executable tests corresponding to the discovered attack trace, which is validated across major browsers. 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和安全机制等。其规格由专家手工审查,以确定潜在的安全问题。然而,由于现代浏览器规格的广泛性以及新的和现有的网络平台组件之间的相互作用,这一过程证明容易出错。为了解决这个问题,我们开发了WebSpec,这是用于分析浏览器安全机制的第一个正式安全框架,它使得自动发现逻辑缺陷和开发机器检查的安全证明。特别是,WebSpec包含一个全面的Coq验证助理浏览器的语义模型,使10个网络安全变量模式正规化,以及将Coq模型和网络变量转换成SMT校正公式的工具链,以便能够与 Z3 orem 验证器进行模式检查。如果发现违规,则工具链将自动产生与所发现的攻击跟踪相匹配的可执行的测试。我们通过在主要浏览器上验证的、通过发现当前网络服务器的3个新版本的逻辑性缺陷,我们展示了网络S的实效,最终通过不同版本的网络核查机制显示了当前三个新的逻辑缺陷,从而显示了当前网络服务器的更新了我们所发现的5个新版本。