search

Agoric / agoric-sdk

monorepo for the Agoric Javascript smart contract platform
Apache License 2.0
328 stars 207 forks source link

Automatic tracking of types in SwingSet kernel #3173

Open andrey-kuprianov opened 3 years ago

andrey-kuprianov commented 3 years ago

Surfaced from @informalsystems Agoric Audit of Agoric/agoric-sdk/SwingSet hash 23ed67c070a6ea04fb305d469283107b1d3d65f3

The SwingSet kernel is written in JavaScript, and thus uses weak and dynamic typing. This may lead to a lot of subtle and undetectable bugs, that would be easy to detect if a language with strict typing is used. Luckily, there is an easy JavaScript -> TypeScript migration path, that brings a lot of benefits early. Even a very quick experiment with renaming all SwingSet .js files into .ts files, and running the TypeScript compiler, allowed to find these issues (among others):

> yarn tsc

src/kernel/initializeKernel.ts(23,24): error TS2554: Expected 2 arguments, but got 1.
src/kernel/initializeKernel.ts(120,60): error TS2554: Expected 1 arguments, but got 2.
src/kernel/kernel.ts(334,9): error TS2554: Expected 2 arguments, but got 1.
src/kernel/kernel.ts(405,7): error TS2554: Expected 3 arguments, but got 2.
src/kernel/kernel.ts(440,9): error TS2554: Expected 3 arguments, but got 2.
src/kernel/kernel.ts(456,17): error TS2554: Expected 3 arguments, but got 2.
src/kernel/kernel.ts(462,17): error TS2554: Expected 3 arguments, but got 2.
src/kernel/kernel.ts(477,13): error TS2554: Expected 3 arguments, but got 2.
src/kernel/liveSlots.ts(534,7): error TS2322: Type '(value: any) => void' is not assignable to type '() => any'.
src/kernel/liveSlots.ts(536,7): error TS2322: Type '(value: any) => void' is not assignable to type '() => any'.
src/kernel/liveSlots.ts(756,17): error TS2554: Expected 7 arguments, but got 1.
src/kernel/state/kernelKeeper.ts(279,18): error TS2554: Expected 1 arguments, but got 0.
src/kernel/state/kernelKeeper.ts(301,15): error TS2345: Argument of type '(text: string, reviver?: (this: any, key: string, value: any) => any) => any' is not assignable to parameter of type '(value: unknown, index: number, array: unknown[]) => any'.
  Types of parameters 'reviver' and 'index' are incompatible.
    Type 'number' is not assignable to type '(this: any, key: string, value: any) => any'.
src/kernel/vatManager/manager-local.ts(73,48): error TS2554: Expected 1 arguments, but got 2.
src/kernel/vatManager/manager-local.ts(99,48): error TS2554: Expected 1 arguments, but got 2.
src/kernel/vatTranslator.ts(155,51): error TS2554: Expected 2 arguments, but got 1.
src/worker-protocol.ts(31,28): error TS2345: Argument of type 'Buffer' is not assignable to parameter of type 'string'.

This only surfaces the problem; adding type annotations will definitely uncover more issues. The real problem with JavaScript is that it is too liberal, and allows to do modifications to the code locally, without considering the far-reaching effects of those changes. As a result, the programmer is forced to do manually the job of a type checker, which can be in fact easily automated to prevent serious bugs.

Recommendation: Consider switching SwingSet kernel to TypeScript, or to track the type information automatically by other means.

erights commented 3 years ago

Recommendation: Consider switching SwingSet kernel to TypeScript, or to track the type information automatically by other means.

As we have already discussed verbally with @andrey-kuprianov

As stated literally, we will not convert our code from JavaScript to TypeScript. However, Agoric has adopted the properjs style of using TypeScript types in jsdoc comments and arranging our tooling to engage the TypeScript type checker to check our code against those types. This provides most of the benefits of writing in TypeScript directly while avoiding two big security hazards of writing in TypeScript:

  1. TypeScript is, by design, an unsound type system. It is still extremely valuable at catching many bugs. The security hazard is a programmer reading TypeScript code may believe the types as if they were guaranteed or enforced, when in fact they may easily be violated, both accidentally and maliciously. By moving the types to the comments, the programmer is much more likely to reason operationally about the semantics of the code they are reading while taking the type declarations to be no more than machine readable comments about the code.
  2. TypeScript is translated to JavaScript. It is the JavaScript that is executed. Every time there is an allegedly-semantics-preserving translation between the code the user wrote and the code that the JS engine executes, we have new security risks. The notion of "semantics preserving" that the authors of these translators have in mind is invariably weaker than the semantics preservation that we need.

All that said, the point of @andrey-kuprianov 's recommendation is still correct. Most of that code is not adequately typed using these typescript-in-jsdoc type declarations. Improving that will have exactly the benefits @andrey-kuprianov states.