关键词：HTML5；应用程序；移动设备；网络协议
摘 要：Rich client-side applications written in HTML5 proliferate diverse platforms such as mobile devices, commodity PCs, and the web platform. These client-side HTML5 applications are increasingly accessing sensitive data, including users' personal and social data, sensor data, and capability-bearing tokens. Instead of the classic client/server model of web applications, modern HTML5 applications are complex client-side applications that may call some web services, and run with ambient privileges to access sensitive data or sensors. The goal of this work is to enable the creation of higher-assurance HTML5 applications. We propose two major directions: rst, we present the use of formal methods to analyze web protocols for errors. Second, we use existing primitives to enable practical privilege separation for HTML5 applications. We also propose a new primitive for complete mediation of HTML5 applications. Our proposed designs considerably ease analysis and improve auditability.