TY - JOUR
T1 - KJS
T2 - A complete formal semantics of javascript
AU - Park, Daejun
AU - Stefanescu, Andrei
AU - Rosu, Grigore
PY - 2015/6
Y1 - 2015/6
N2 - This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the existing implementations of JavaScript, only Chrome V8's passes all the tests, and no other semantics passes more than 90%. In addition to a reference implementation for JavaScript, KJS also yields a simple coverage metric for a test suite: the set of semantic rules it exercises. Our semantics revealed that the ECMAScript 5.1 conformance test suite fails to cover several semantic rules. Guided by the semantics, we wrote tests to exercise those rules. The new tests revealed bugs both in production JavaScript engines (Chrome V8, Safari WebKit, Firefox SpiderMonkey) and in other semantics. KJS is symbolically executable, thus it can be used for formal analysis and verification of JavaScript programs. We verified non-trivial programs and found a known security vulnerability.
AB - This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the existing implementations of JavaScript, only Chrome V8's passes all the tests, and no other semantics passes more than 90%. In addition to a reference implementation for JavaScript, KJS also yields a simple coverage metric for a test suite: the set of semantic rules it exercises. Our semantics revealed that the ECMAScript 5.1 conformance test suite fails to cover several semantic rules. Guided by the semantics, we wrote tests to exercise those rules. The new tests revealed bugs both in production JavaScript engines (Chrome V8, Safari WebKit, Firefox SpiderMonkey) and in other semantics. KJS is symbolically executable, thus it can be used for formal analysis and verification of JavaScript programs. We verified non-trivial programs and found a known security vulnerability.
KW - JavaScript
KW - K framework
KW - Mechanized semantics
UR - http://www.scopus.com/inward/record.url?scp=84950973214&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84950973214&partnerID=8YFLogxK
U2 - 10.1145/2737924.2737991
DO - 10.1145/2737924.2737991
M3 - Article
AN - SCOPUS:84950973214
VL - 50
SP - 346
EP - 356
JO - ACM SIGPLAN Notices
JF - ACM SIGPLAN Notices
SN - 1523-2867
IS - 6
ER -