[PRL] Information Flow Analysis for a Dynamically Typed Functional Language with S...

[Mitch]

  Sent to you by Mitch via Google Reader: Information Flow Analysis for
a Dynamically Typed Functional Language with Staged Metaprogramming.
(arXiv:1302.3178v1 [cs.PL]) via cs.PL updates on arXiv.org by <a
href="http://arxiv.org/find/cs/1/au:+Lester_M/0/1/0/all/0/1">Martin
Lester</a>, <a
href="http://arxiv.org/find/cs/1/au:+Ong_L/0/1/0/all/0/1">Luke Ong</a>,
<a href="http://arxiv.org/find/cs/1/au:+Schaefer_M/0/1/0/all/0/1">Max
Schaefer</a> on 2/13/13

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.

Things you can do from here:
- Subscribe to cs.PL updates on arXiv.org using Google Reader
- Get started using Google Reader to easily keep up with all your
favorite sites
-------------- next part --------------
HTML attachment scrubbed and removed