Fully Abstract compilation from F* to JavaScript

If you aren't familiar with the F* project, it's a rather fascinating
approach to language security based on a rich type system. It's worth
studying if you're into PL at all:
http://research.microsoft.com/en-us/projects/fstar/

But perhaps more interesting to this venue: the developers claim to have
achieved a fully abstract compiler to JavaScript:

http://research.microsoft.com/apps/pubs/default.aspx?id=176601

If you are unfamiliar with the concept, compilation with 'full abstraction'
means that the JavaScript target has the same observational properties -
critically, the same security properties! - as the original program.

http://en.wikipedia.org/wiki/Denotational_semantics#Abstraction

This means the F* program, in JavaScript form, is secure even against other
JavaScript code involving in-browser mashups or similar. The article
studies the range of obscure attacks possible in JS contexts, across a
variety of implementations.

If you're interested in targeting JavaScript as an 'assembly language' of a
web, while maintaining security properties, this seems a valuable article
to read.

_______________________________________________
cap-talk mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/cap-talk