The internet is a major distribution platform for web applications, but there are no effective transparency and audit mechanisms in place for the web. Due to the ephemeral nature of web applications, a client visiting a website has no guarantee that the code it receives today is the same as yesterday, or the same as other visitors receive. Despite advances in web security, it is thus challenging to audit web applications before they are rendered in the browser. We propose Accountable JS, a browser extension and opt in protocol for accountable delivery of active content on a web page. We prototype our protocol, formally model its security properties with the Tamarin Prover, and evaluate its compatibility and performance impact with case studies including WhatsApp Web, AdSense and Nimiq. Accountability is beginning to be deployed at scale, with Meta's recent announcement of Code Verify available to all 2 billion WhatsApp users, but there has been little formal analysis of such protocols. We formally model Code Verify using the Tamarin Prover and compare its properties to our Accountable JS protocol. We also compare Code Verify's and Accountable JS extension's performance impacts on WhatsApp Web.
翻译:互联网是网络应用程序的主要分发平台,但网络没有有效的透明度和审计机制。由于网络应用程序的短暂性质,访问网站的客户不能保证今天收到的代码与昨天相同,或与其他访问者收到的代码相同。尽管在网络安全方面取得了进步,因此在浏览器提供网络应用程序之前对网络应用程序进行审计具有挑战性。我们提议采用负责的联署材料,浏览器扩展,并选择在网站上以负责的方式提供主动内容。我们制作了我们的协议,正式将其安全属性与Tamarin Prover建模,并评估其与案例研究的兼容性和绩效影响,包括“WestsApp Web”、“Adsense”和“Nimiq”的兼容性和绩效影响。问责制开始大规模部署,Meta最近宣布的代码核查向所有20亿个“WhatsApp”用户提供,但对此类协议几乎没有正式分析。我们正式用Tamarin Prover验证示范代码,并将其属性与我们的可问责的联署材料协议进行比较。我们还比较了代码核查和可问责的联署材料对“What App”网络的业绩影响。