idea: static analysis for unexpected throws

[dckc]

In a Jan 17 comment, @jhnaldo writes:

We are currently developing JSAVER, a JavaScript static analyzer, based on the JavaScript syntax and semantics extracted from ECMAScript specification via JISET. While the current version of JSAVER is a prototype implementation, we checked that it can successfully analyze all applicable JavaScript programs in Test262: ECMAScript Test Suite (ECMA TR/104).

On the other hand, our team also has developed SAFE, a JavaScript static analyzer for ECMAScript 5.1, with abstract semantics designed by hand in several years.

I cannot find JSAVER. Is it shared publicly yet? So this SAFE tool seems to be the closest thing with an open issues list...

I have an idea for a static analysis tool to check for unexpected throws. Expected throws would be denoted as assert(cond) or assert.typeof(x, 'string') or assert.equal(a, b) or the like. If any code path could lead to a throw other than an explicit assert, the tool should report that as a problem. I expect this would be extremely valuable in establishing that input validation has been done thoroughly. For example, in issues such as:

• Validate Zoe inputs Agoric/agoric-sdk#4068

I would appreciate any thoughts you would like to share on how to go about making such a tool.

Feel free to write to me at connolly@agoric.com if you prefer that over a github issue such as this.

cc @erights

[jhnaldo]

Hi @dckc, the tool JSAVER has been a private project because of the double-blinded conference review process. Recently, we accepted the paper and opened it to the public in the following repository:

• https://github.com/kaist-plrg/jsaver/

Please look at this repository if you are interested in JavaScript static analysis with evolving language specifications.

For the exception analysis you mentioned, I believe it is possible to detect such unexpected throws using SAFE or JSAVER. However, I have two concerns about it.

First, it might require manual modeling of opaque code. Many existing real-world JavaScript programs require host-dependent functions, such as DOM APIs or Node.js APIs. Since they are opaque code, we should manually define their modeling to analyze such JavaScript programs.

Second, JavaScript static analysis has lower analysis precision than other languages because of the highly-dynamic nature of JavaScript. As a result, it might cause false alarms of unexpected throws. Nevertheless, I believe that we could alleviate it via optimization with reasonable assumptions.

[dckc]

Excellent! Thank you!

This limitation is not a problem for us:

Many existing real-world JavaScript programs require host-dependent functions, such as DOM APIs or Node.js APIs.

Our system excludes such host-dependent functions: https://agoric.com/documentation/guides/js-programming/hardened-js.html#hardening-javascript-limiting-globals-with-compartments

[turadg]

JavaScript static analysis has lower analysis precision than other languages because of the highly-dynamic nature of JavaScript

TypeScript could help with that.

• Proposal: new "invalid" type to indicate custom invalid states microsoft/TypeScript#23689
• Throw types microsoft/TypeScript#40468