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: first, 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.