Reseña: A certified JavaScript interpreter

Se ha publicado un nuevo trabajo de formalización en Coq titulado A certified JavaScript interpreter.

El autor del trabajo es Martin Bodin (del INRIA de Rennes) en colaboración con Alan Schmitt y Thomas Jensen.

El trabajo es parte del proyecto JSCert cuyo objetivo es la construcción de modelos de JavaScript en Coq y el desarrollo de herramientas de análisis automático basadas en dichos modelos.

El resumen del trabajo es

Although it was initially designed for running small scripts in web pages, JavaScript has become the programming language of the web. It is designed to be very dynamic, for instance by allowing the evaluation of strings as code or by letting programmers to explicitly specify the scope in which a program runs. These aspects allow for great flexibility, but significantly hinder the understanding of the semantics of programs, such as the development of certified analyses.

In practice, it is frequent to insert external code in a web page (such as an advertisement or an interactive map) and make it interact with some scripts carrying some potentially secret information. It would be useful to be able to prove the safety of a web page despite the presence of unknown (thus untrusted) code.

In this internship, we present a formalisation in Coq of JavaScript’s semantics. Our main result is a JavaScript interpreter proven correct with respect to the Coq’s semantics. This work is the first step in the building of certified analysers.