A Trusted Mechanised JavaScript Specification

Gareth Smith, Imperial College.

A Trusted Mechanised JavaScript Specification

JSCert Logo http://jscert.org/popl14/

A Trusted Mechanised JavaScript Specification

Inria
  • Martin Bodin
  • Arthur Charguéraud
  • Alan Schmitt
Imperial
  • Daniele Filaretti
  • Philippa Gardner
  • Sergio Maffeis
  • Daiva Naudziuniene
  • Gareth Smith

JavaScript Specifications

  • Initial Implementation (Netscape Navigator 1995)
  • ECMAScript 3 standard (1999)
  • Formal definition for the full language, justification via closeness to specification and proofs of safety properties (APLAS'08)
  • ECMAScript 5 (2009)
  • λJS: translation into a λ-calculus with references, justification via testing (ECOOP'10)
  • Program logic for a core part of the language (POPL'12)
  • λS5: like λJS for ES5 strict mode
  • F* to JavaScript via λJS, a full abstraction result (POPL'13)

This Talk

JSCert Trust

Coverage

JSCert Coverage

Coverage

JSCert Coverage

ES5 ↔ JSCert

Connecting ES5 to JSCert

ES5 ↔ JSCert

Connecting ES5 to JSCert

ES5 ↔ JSCert

Connecting ES5 to JSCert

Reading the Coq

This:
red_stat_while1
Can be read as this:
red_while_2a_2b

While

  1. Let V = empty.
  2. Repeat
    1. Let exprRef be the result of evaluating Expression.
    2. If ToBoolean(GetValue(exprRef)) is false, return (normal, V, empty).
    3. Let stmt be the result of evaluating Statement.
    4. If stmt.value is not empty, let V = stmt.value.
    5. If stmt.type is not continue || stmt.target is not in the current label set, then
      1. If stmt.type is break and stmt.target is in the current label set, then
        1. Return (normal, V, empty).
      2. If stmt is an abrupt completion, return stmt.

While

  1. Let V = empty.
red_while_1

While

  1. Repeat
    1. Let exprRef be the result of evaluating Expression.
    2. If ToBoolean(GetValue(exprRef)) is false, return (normal, V, empty).
red_while_2a_2b

While

  1. Repeat
    1. If ToBoolean(GetValue(exprRef)) is false, return (normal, V, empty).
red_while_2b_false

This Talk

JSCert Trust

Testing

Total #Test262 Tests
11746
Chapters 8-14
2782
#Passes in 8-14
1796
Total #Passes
2633
Remaining test failures due to: use of for-in, chapter 15 library use, the parser, buggy tests.

ES5 ↔ JSCert

Connecting ES5 to JSCert

JSCert ↔ JSRef

Connecting JSCert to JSRef

Bugs Found

This Talk

JSCert Trust
JSCert Trust
JSCert Trust

JSCert Statistics

ECMA Standard
280 pages
Declarative JSCert
3000 lines
Computable JSRef
2000 lines
Correctness Proof
3500 lines
Effort
8 people, part time, 1 year
URL
http://jscert.org

Try JSCert!