Dataset
Verifying information flow and metaprogramming in dynamically typed languages
- Alternative title:
- Mechanised Coq proofs and analysis source code supporting thesis
- Documentation:
-
This gzip-compressed tar archive contains files supporting a paper on information flow analysis for a JavaScript-like language, focusing on how to handle eval.
The focus of the paper is an automated program analysis for this language. The directory demo1 contains an implementation of this analysis in OCaml. Mechanised Coq proofs of the correctness of the analysis are in the directories coq-cfa and coq-if. Finally, demo2 contains an OCaml implementation of a transformation on programs in this language that is developed in the paper. A README file in the archive discusses this in more detail.
Proofs were tested in Coq 8.3pl4. Source code was tested in OCaml 3.12.1. Binaries were built under Debian 7 ("wheezy") on i386. 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.
Actions
Authors/Creators
Contributors
+ Schäfer, M
- Institution:
- University of Oxford
- Division:
- MPLS
- Department:
- Computer Science
- Role:
- Researcher
- Publisher:
- University of Oxford
- Publication date:
- 2015
- DOI:
- Keywords:
- Subjects:
- UUID:
-
uuid:f52857fa-5059-4341-a486-165e98ea8753
- Deposit date:
-
2016-07-21
Terms of use
- Copyright date:
- 2015
If you are the owner of this record, you can report an update to it here: Report update to this record