Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures
Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures
复制标题
安全分析与设计基础 VII - FOSAD 2012/2013 教程讲座
DOI：
10.1007/978-3-319-10082-1_4
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Bhargavan K
中科院分区：
文献类型：
--
作者：
Bhargavan K
防御性JavaScript （DJS）是JavaScript的一个类型化子集，它保证程序的功能行为不会被篡改，即使它是在攻击者控制的恶意环境中加载和执行的。因此，DJS非常适合编写JavaScript安全组件，例如bookmarklet、单点登录小部件和加密库，这些组件可能与来自任意第三方的未知脚本一起加载在不受信任的web页面中。我们提供了一个关于DJS语言的教程以及它的设计动机。我们将展示如何在DJS中编写安全组件，如何使用DJS类型检查器验证它们的防御性，以及如何使用ProVerif自动分析它们的安全属性。
Defensive JavaScript (DJS) is a typed subset of JavaScript that guarantees that the functional behavior of a program cannot be tampered with even if it is loaded by and executed within a malicious environment under the control of the attacker. As such, DJS is ideal for writing JavaScript security components, such as bookmarklets, single sign-on widgets, and cryptographic libraries, that may be loaded within untrusted web pages alongside unknown scripts from arbitrary third parties. We present a tutorial of the DJS language along with motivations for its design. We show how to program security components in DJS, how to verify their defensiveness using the DJS typechecker, and how to analyze their security properties automatically using ProVerif.