Dataset icon

Dataset

Verifying information flow and metaprogramming in dynamically typed languages

Subtitle:
Mechanised Coq proofs and analysis source code supporting thesis
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 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...

Expand abstract

Actions


Access Document


Files:

Authors


More by this author
Department:
Department of Computer Science, University of Oxford
Role:
Creator, Researcher

Contributors

Department:
Department of Computer Science, University of Oxford
Role:
Researcher
Publisher:
University of Oxford
Publication date:
2015
DOI:
Keywords:
Subjects:
Format:
Digital
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.<br/><br/> 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 progra... Expand documentation

Terms of use


Metrics



If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP