A Mechanized Rich Model of the Web Infrastructure

万维网是现代社会必不可少的信息和通信技术。因此，网络的安全和隐私已经成为越来越重要的方面。web是一个复杂的基础设施，DNS服务器、web服务器和web浏览器等实体使用各种技术进行交互和通信。鉴于已经报道的针对网络基础设施和网络应用程序的大量攻击，以及网络日益增长的复杂性，对网络基础设施和网络应用程序进行严格和系统的安全和隐私分析是必不可少的。为了进行这样的分析，需要一个详细的web基础设施的正式模型，它可以用来精确地说明和证明web标准和web应用程序的安全和隐私属性。在申请人之前的工作和之前的项目中，我们已经开发并成功地应用了这样一个模型，其中包括分析广泛使用的web标准和应用程序。我们发现了几个严重的攻击，提出了修复建议，并首次证明了固定标准和应用程序的安全性和隐私属性。然而，到目前为止，该模型需要纸笔证明——安全性和隐私分析还没有工具支持。这有几个缺点，比如证明有缺陷的风险，以及缺乏可重用性和非专家的可访问性。因此，这个项目的主要目标是提供这样的工具支持，完全消除了对纸笔证明的需要。更具体地说，我们希望在函数式编程语言F*中形式化我们的web模型，该语言自带程序验证机制，并使用该模型来分析重要的web应用程序和标准。我们还计划使用这个机械化的模型来自动地派生经过验证的web应用程序代码，为web应用程序和标准生成测试用例，并从失败的安全证明尝试中生成漏洞。

The World Wide Web is an essential and by now indispensable information and communication technology for modern societies. As such, security and privacy in the web have become more and more crucial aspects. The web is a complex infrastructure, with entities such as DNS servers, web servers, and web browsers interacting and communicating using diverse technologies. In the light of numerous attacks on the web infrastructure and web applications that have been reported and the growing complexity of the web, rigorous and systematic security and privacy analyses of both the web infrastructure and web applications is essential. In order to carry out such analyses, a detailed formal model of the web infrastructure is required which can be used to precisely state and then prove security and privacy properties of web standards and web applications. In previous work by the applicant and in the predecessor project we have developed and successfully applied such a model, among others, to analyze widely used web standards and applications. We have uncovered several severe attacks, suggested fixes, and for the first time proved security and privacy properties for the fixed standards and applications. So far, however, the model requires pencil-and-paper proofs–security and privacy analyses are not supported by tools. This has several disadvantages, such as the risk of proofs being flawed as well as a lack of reusability and accessibility for non-experts. The main goal of this project is therefore to provide such tool-support, completely eliminating the need for pencil-and-paper proofs. More specifically, we want to formalize our web model in the functional programming language F*, which comes with built-in mechanisms for program verification, and use this model to analyze important web applications and standards. We also plan to use this mechanized model to automatically derive verified web application code, to generate test cases for web applications and standards, and to generate exploits from failed security proof attempts.