ADsafety: Type-Based Verification of JavaScript Sandboxing
ADsafety: Type-Based Verification of JavaScript Sandboxing
复制标题
DOI：
--
复制
发表时间：
2011-08
期刊：
影响因子：
--
通讯作者：
J. Politz;Spiridon Aristides Eliopoulos;Arjun Guha;S. Krishnamurthi
中科院分区：
文献类型：
--
作者：
J. Politz;Spiridon Aristides Eliopoulos;Arjun Guha;S. Krishnamurthi
网站通常会将多个来源的 JavaScript 程序合并到一个页面中。这些来源必须相互保护，这需要强大的沙箱。沙箱的众多入口点和 JavaScript 的微妙之处需要对实际沙箱源进行可靠的验证。我们使用一种新颖的 JavaScript 类型系统来编码和验证沙箱属性。由此产生的验证器是轻量级且高效的，并且在实际源上运行。我们通过将其应用于 ADsafe 来展示我们的技术的有效性，这揭示了一些错误和其他弱点。
Web sites routinely incorporate JavaScript programs from several sources into a single page. These sources must be protected from one another, which requires robust sandboxing. The many entry-points of sandboxes and the subtleties of JavaScript demand robust verification of the actual sandbox source. We use a novel type system for JavaScript to encode and verify sandboxing properties. The resulting verifier is lightweight and efficient, and operates on actual source. We demonstrate the effectiveness of our technique by applying it to ADsafe, which revealed several bugs and other weaknesses.