title: New poster:An Infrastructure for Tractable Verification of JavaScript
---
Petar Maksimovic presented a poster at the UK Cyber Security Research Conference in London on the group's work on the JSCert project.
The dynamic nature of JavaScript and its complex semantics make it a difficult target for verification.
To address this issue, we develop JS-2-JSIL, a compiler from JavaScript (ECMAScript 5 strict) to a simple intermediate goto language, JSIL.
We design JS-2-JSIL to be step-by-step faithful to the ECMAScript standard, systematically testing it against the official ECMAScript conformance test suite, and proving it
correct with respect to a fragment of the ES5 Strict operational semantics.
We develop JSIL logic, a separation logic for JSIL that we prove sound with respect to its operational semantics, and a semiautomatic verification tool based on this logic.
Together, these results allow us to verify Hoare triples for JavaScript using JSIL logic and JS-2-JSIL.
