{"id":2123,"date":"2012-08-11T08:51:08","date_gmt":"2012-08-11T08:51:08","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2123"},"modified":"2013-03-08T05:48:13","modified_gmt":"2013-03-08T05:48:13","slug":"resena-a-certified-javascript-interpreter","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-certified-javascript-interpreter\/","title":{"rendered":"Rese\u00f1a: A certified JavaScript interpreter"},"content":{"rendered":"<p>Se ha publicado un nuevo trabajo de formalizaci\u00f3n en <a href=\"http:\/\/coq.inria.fr\"><\/a>Coq titulado  <a href=\"http:\/\/perso.ens-lyon.fr\/martin.bodin\/M2\/stage\/rapport.pdf\">A certified JavaScript interpreter<\/a>. <\/p>\n<p>El autor del trabajo es <a href=\"http:\/\/perso.ens-lyon.fr\/martin.bodin\/research.html.fr\">Martin Bodin<\/a> (del INRIA de Rennes) en colaboraci\u00f3n con <a href=\"http:\/\/www.irisa.fr\/celtique\/aschmitt\">Alan Schmitt<\/a> y <a href=\"http:\/\/www.irisa.fr\/celtique\/jensen\">Thomas Jensen<\/a>.<\/p>\n<p>El trabajo es parte del proyecto <a href=\"http:\/\/jscert.org\">JSCert<\/a> cuyo objetivo es la construcci\u00f3n de modelos de JavaScript en Coq y el desarrollo de herramientas de an\u00e1lisis autom\u00e1tico basadas en dichos modelos. <\/p>\n<p>El resumen del trabajo es<\/p>\n<blockquote><p>\nAlthough 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. <\/p>\n<p>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. <\/p>\n<p>In this internship, we present a formalisation in Coq of JavaScript\u2019s semantics. Our main result is a JavaScript interpreter proven correct with respect to the Coq\u2019s semantics. This work is the first step in the building of certified analysers.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un nuevo trabajo de formalizaci\u00f3n en Coq titulado A certified JavaScript interpreter. El autor del trabajo es Martin Bodin (del INRIA de Rennes) en colaboraci\u00f3n con Alan Schmitt y Thomas Jensen. El trabajo es parte del proyecto JSCert cuyo objetivo es la construcci\u00f3n de modelos de JavaScript en Coq y el desarrollo&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[45,89,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2123"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=2123"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2123\/revisions"}],"predecessor-version":[{"id":2797,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2123\/revisions\/2797"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2123"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2123"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2123"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}