2013/02/13 by Martin Mariusz Lester, Lester, Martin, C.-H. Luke Ong +2
Computer Science · #Advanced Malware Detection Techniques #FOS: Computer and information sciences #Network Security and Intrusion Detection #Programming Languages (cs.PL) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1302.3178
openalex publication_date 2013/02/13 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.