Towards efficient and verified virtual machines for dynamic languages

Abstract

The prevalence of dynamic languages is not commensurate with the security guarantees provided by their execution mechanisms. Consider, for example, the ubiquitous case of JavaScript: It runs everywhere and its complex just-in-time compilers produce code that is fast and, unfortunately, sometimes incorrect. We present an Isabelle/HOL formalization of an alternative execution model-optimizing interpreters-and mechanically verify its correctness. Specifically, we formalize advanced speculative optimizations similar to those used in just-in-time compilers and prove semantics preservation. As a result, our formalization provides a path towards unifying vital performance requirements with desirable security guarantees.