Information Flow Analysis for a Dynamically Typed Functional Language with Staged Metaprogramming

TL;DR

This paper introduces a novel static information flow analysis for a dynamically typed functional language with staged metaprogramming, aiming to improve security reasoning in languages like JavaScript.

Contribution

It presents the first fully static information flow analysis for a language with staged metaprogramming and provides a formal proof of its soundness.

Findings

Proved the soundness of the analysis

Implemented the analysis and tested it on relevant examples

Demonstrated its applicability to security properties like noninterference

Abstract

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.