Verifying information flow and metaprogramming in dynamically typed languages

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 via eval.
In order to deal 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 demonstrate the applicability of the analysis,
we also present a general method for transforming a program using eval
into one using staged metaprogramming.

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.