A Mechanized Rich Model of the 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.