A Mechanized Rich Model of the Web Infrastructure

Web 基础设施的机械化丰富模型

• 批准号: 276807658
• 负责人: Professor Dr. Ralf Küsters
• 金额: --
• 依托单位: Institut für Informationssicherheit
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2015
• 资助国家: 德国
• 起止时间: 2014-12-31 至 2019-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/276807658?language=en
• 关键词: Mechanized; Rich; Model; Web; Infrastructure

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.

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