一种动态类型函数式语言的分段元编程信息流分析
Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming
摘要：
用JavaScript编写的Web应用程序通常用于处理敏感或个人数据。因此，推理其安全属性已成为一个重要的问题，这是非常困难的高度动态的语言，特别是它的支持运行时代码生成的性质。作为处理这一问题的第一步，我们建议调查的安全性分析的语言与更有原则的形式的动态代码生成。为此，我们提出了一个静态信息流分析的动态类型的函数式语言与基于原型的继承和分期元编程。我们证明了它的合理性，实现它，并测试它的各种例子，旨在证明其相关性的安全属性，如不干扰，在JavaScript。据我们所知，这是第一个完全静态的信息流分析的语言与分级元编程，和第一个正式的可靠性证明的CFA为基础的信息流分析的功能性程序设计语言。
英文摘要：
Web applications written in JavaScript are regularly used for dealing with sensitive or personal data. Consequently, reasoning about their security properties has become an important problem, which is made very difficult by the highly dynamic nature of the language, particularly its support for runtime code generation. As a first step towards dealing with this, we propose to investigate security analyses for languages with more principled forms of dynamic code generation. To this end, we present a static information flow analysis for a dynamically typed functional language with prototype-based inheritance and staged metaprogramming. We prove its soundness, implement it and test it on various examples designed to show its relevance to proving security properties, such as noninterference, in JavaScript. To our knowledge, this is the first fully static information flow analysis for a language with staged metaprogramming, and the first formal soundness proof of a CFA-based information flow analysis for a functional programming language.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
