A Trusted Mechanised JavaScript Specification

Gareth Smith, Imperial College.

A Trusted Mechanised JavaScript Specification

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

red_while_2a_2b

While

Let V = empty.
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

Let V = empty.

red_while_1

While

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

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

Finally completion values (SpiderMonkey, V8, WebKit).
for-in enumerates over properties deleted from prototype during enumeration (SpiderMonkey).
Dead code changing completion values (V8).
Shadowing non-enumerable properties still enumerated (V8, WebKit first reported by Mark Miller).
Typo in for-in spec (ES6).
Broken "informative algorithm" (ES6).
Underspecified Enumerate internal method (ES6).
Shadowing non-enumerable properties should not be enumerated (Test262).
No-one knows what test 12.6.4-2 is for (Test262).
NPE checking lg.proto (Test262).

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