informal-agoric-report-phase2

Formal Methods Assessment Report

Agoric Swingset Kernel and Userspace, Phase 2: Adversarial Testing of Userspace Vat Interaction, and Modeling & Verification of Garbage Collection Protocol

09.11.2021 Initial revision: 21.10.2021

Contents Assessment Overview 3 The Project . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 The Agoric SwingSet Platform . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 Scope of this report . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Conducted work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Timeline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

Assessment Dashboard 6

Engagement Goals 7

Coverage 8 (MBT) Adversarial testing of inter-vat communication in userspace . . . . . . . . . . . . . . . . . . . . . . 8 (MBT) Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 (MBT) Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 (MBT) Method . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 (GC) Model-checked TLA+ model of garbage collector protocol . . . . . . . . . . . . . . . . . . . . . . . . 10 (GC) Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 (GC) Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 (GC) Method . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

Findings 13

IF-AGORIC2-01: Unprincipled use of OOP concepts has likely created technical debt 14 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

IF-AGORIC2-02: Make the code in gc-actions.js easier to understand 17 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

IF-AGORIC2-03: Do not overload isReachableFlag 20 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

IF-AGORIC2-04: retireImports dispatch does not have any effect on liveslots 21 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

IF-AGORIC2-05: Check the correctness of the retireImports syscall code with respect to timing 22 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

Assessment Overview The Project In April 2021, Agoric engaged Informal Systems to conduct a formal methods assessment of the documentation and the current state of the implementation of the Agoric SwingSet platform kernel and vat interactions.

The Agoric SwingSet Platform The Agoric SwingSet is the basis for development with the Agoric SDK, a development kit for writing smart contracts in a secure, hardened version of JavaScript. Smart contracts built with the Agoric SDK have mediated asynchronous communication, and messages can only be sent along references according to the rules of the Object Capabilities model that the SwingSet implements. The Object Capabilities (OCAP) model is a model for reasoning about communication. An Object-Capability is a transferable, unforgeable authorization to use a designated object. The SwingSet machine allows JavaScript code to communicate according to the model, and executes code in a userspace similar to that offered by a Unix operating system. The SwingSet kernel component operates analogously to a Unix kernel, and vats correspond to Unix userspace processes. The kernel provides services for isolation, composition, and communication between vats: it enforces the OCAP properties. The figure below shows a diagram of the architecture of the SwingSet kernel and two interacting vats. Each vat is a unit of synchrony and synchronous communication only occurs inside a single vat. The liveslots layers mediate access to the outside world from userspace code. Every remote object access is implemented via translation tables in the liveslots layers and the kernel, which operates by pulling work off from a run queue.

Scope of this report This report covers Phase 2 of the Swingset analysis, with Phase 1 results covered in the previous report. The agreed-upon workplan for Phase 2 consisted of the following tasks, as outlined in the diagram:

Task E.3. Swingset End-To-End Testing Plugin
Task A.1. Adversarial Kernel Modeling & Testing
Task C.2. Garbage Collection Code Inspection
Task M.2. Garbage Collection Model
Task P.2. Garbage Collection Safety & Liveness Proofs

This report covers the above tasks, with the exception that the tasks related to garbage collection protocol have been restricted to the communication between kernel and vats, but not including the virtual object manager or comms vat. The tasks were conducted 22.07.2021 through 28.09.2021 by Informal Systems by the following personnel: • Andrey Kuprianov: Principal Research Engineer at Informal Systems • Daniel Tisdall: Research Engineer at Informal Systems

Conducted work Starting 22nd July, Informal Systems conducted an assessment of the existing documentation and code. Our team started with reviewing the SwingSet package documentation to get an overview of the design principles of the system, and with a review of some critical components of Hardened JavaScript, which are critical for the security of the platform. Some of the effort included reviewing previously studied material, as we had a new team member join who was not familiar with the system from the first stage of the assessment. After developing an understanding we created an adversarial testing model and test driver, to exercise the userspace

capabilities of inter-communicating vats. The work includes a TLA+ model, as well as vat code written in JavaScript, and some additional scripts written in Python and Bash for pre and post processing steps. Additionally, we inspected documentation and code relevant to the working of the garbage collector protocol, restricted to the parts that relate to the kernel, and vats, but not including the virtual object manager or comms vat. We created an abstract TLA+ model of the protocol and model checked it. We found no errors, and the model checking search completely exhausted the state space. Informal Systems created issues in the agoric-sdk Github repository for a number of issues that we found over the course of the assessment. The issues can be found at the repository.

Timeline • 22.07.2021: Start of assessment • 26.07.2021: Bootstrap discussion: update from the Agoric side; setting the goals, priorities & timeline • 01.09.2021: Intermediate meeting: preliminary demo of userspace adversarial testing & discussion on modeling the garbage collection protocol • 23.09.2021: Final demo of userspace MBT & demo/discussion of GC modeling and verification • 28.09.2021: End of assessment • 21.10.2021: First draft of this report • 02.11.2021: Correction suggestions received from Agoric • 09.11.2021: Submission of the final version of this report

Conclusions Overall we found the code to be organized, reasonably well documented, and faithful to the specification. Despite the general high quality of the implementation work in terms of correctness, we found several significant issues regarding code quality, code organization, and possible divergence from the specification and documentation. These are detailed in the relevant findings. The main source of issues seems to be the high complexity of the code in function bodies, and ‘class’ object definitions. This complexity can be considered a symptom of a greater problem, namely that the code does not use an Object Oriented Programming style, and is instead written in a procedural style. Indeed, much of the code does not exhibit clear separation of concerns, and has side effects which make it difficult to reason about. Code comprehension is difficult, and is likely to hinder developers from effectively working on the codebase as the project matures. The difficulty in understanding is not decreased by the use of JavaScript as a language, and the extensive use of creating objects dynamically via various factory functions, which make it hard to follow the thread of execution between method calls. Departing from the issues relating to code structure, we did not find any significant semantic errors in either the garbage collector protocol, or the inter-vat communication implementation. None of the pathways tested or modelled deviated from the expected behavior.

Assessment Dashboard Target Summary • Name: Agoric SwingSet inter-vat communication in userspace code and garbage collection protocol • Type: Documentation and implementation • Platform: JavaScript • Artifacts: – Agoric SDK at commit 774cb6ad30 Engagement Summary • Dates: 22.07.2021 – 28.09.2021 • Method: Manual review & formal protocol modelling & protocol verification & adversarial testing • Employees Engaged: 2 • Time Spent: 9 person-weeks

Engagement Goals The scope of the assessment developed over time as a result of a series of meetings between the Agoric and Informal teams. The highest priority aspects of the system were determined to be

The Object-Capability model, and its implementation
The garbage collector protocol It was determined that Informal Systems would do analysis of 1) and 2) by way of adversarial (model-based) testing, and protocol model checking. In particular, during this phase of the assessment, Informal Systems checked the object capability (OCAP) system by applying adversarial testing to check and generate interactions among vats communicating in the userspace. Additionally, Informal Systems created a TLA+ model of one part of the garbage collector protocol functionality, namely the garbage collection flows in the kernel and the kernels interactions with exporting and importing vats.

Coverage (MBT) Adversarial testing of inter-vat communication in userspace (MBT) Overview Users write code which executes in vats, and vats are able to communicate by sending messages and objects to each other. Informal Systems applied adversarial (model-based) testing to test the code paths that implement the inter-vat communication and Object-Capability model. Informal Systems created a TLA+ model of a system consisting of a number of vats which non-deterministically create one of three object types and also interact with created objects in several ways. An execution consists of several steps of object creation and interaction. The SwingSet code is tested by converting executions generated by the model checker into a runnable script, and running the script with vat driver code implemented in the system. In a model step vats either create a reference to themselves, or a promise and a resolver function for the created promise, or they perform actions with existing objects.

Vat Reference Vats can interact with a vat reference by calling a (remote) .send method on the reference, which takes an object as an argument. The .send method gives the subject vat the capability to use the argument object in future steps of the execution. Vats can also interact with a vat reference by passing it as an argument to the resolver of a promise. Any vat which had the capability to access the promise will subsequently have access to the resolved-to vat.

Promise and Resolver Vats can interact with a promise by awaiting the result, or passing it as an argument in a .send method call on a vat reference. Vats can interact with a promise resolver function object by either passing it as an argument in a .send method call, or executing it (resolving the promise) with a vat reference or promise resolver object as argument.

Illustration The figure below shows a representation of two subsequent model states. Each vat can access a subset of the items (objects) in the shared universe. Access is represented by dotted lines. Vat references are coloured, promises are pink and resolvers to promises are purple. Promises and their resolvers are also numbered correspondingly.

At time t_{k} vat A can access the resolver r1 for promise p1 even though it cannot access p1. It resolves the promise to vA, a reference to itself that it has access to. Vat C has access to p1 so in the subsequent state at time t_{k+1} vat C has access to the item that p1 resolved to (vA).

(MBT) Results We did not uncover any error in the code by running the executions. We did also intentionally introduce errors (one at a time) into the SwingSet source code to ensure that our test driver was able to find them.

Executions run (all error free) We generated and ran 1700 tests consisting of a sequence of model steps (max 9). The below table shows three batches of tests run, making 1700 in total. The Num vats column contains the number of vats modelled in the execution. The Universe size column contains the maximum number of objects (vat references, promises or resolvers) present in the system. The Pattern column contains a description of the model behavior that an execution on the corresponding batch matches.

Num executions Num vats Universe size Pattern 1297 2 4 There is at least one send step. 303 2 4 Each vat does a step, and some step resolves a promise that another vat has access to. 100 3 5 Each vat does a step, and some step resolves a promise that another vat has access to.

(MBT) Method There are three components to the adversarial (model-based) testing implemented.

The TLA+ model The model used for generating executions for testing.
Glue code used to convert TLA+ traces into scripts which can be followed by the test driver Python and Bash scripts are used to convert TLA+ executions into .json scripts which can be interpreted by the JavaScript code to run the system. The scripts take care of parsing the TLA+ executions, doing conversions, and running the scripted executions by calling the swingset-runner executable with a script filename as argument. There is also code to parse the logs generated by the test executions for any error messages.
JavaScript code used to run scripts against the SwingSet kernel The vat code consists of a bootstrap vat source file, and another vat source file, which is used by all the vats in the execution. The TLA+ model models the universe of objects which can be interacted with using a single array to store the objects, however in the JavaScript code it is necessary for each vat to maintain a local Map that stores the objects it has access to. Therefore the conversion from a TLA+ execution to a runnable script must perform some logic which tracks the universe of objects and assigns object ids to each of them, which running vat code can use for lookups. The logic of this conversion can be found in the states_to_driver_script.py artifact. The stdout stream of a running test execution is captured and the contents is scanned for keywords in the set {“err”, “warning”, “panic”, “kernel”}. Additionally, it is checked that a sentinel string is present “Bootstrap Done.”. The presence of a keyword or the absence of the sentinel string indicates a problem. The summarize_results.py artifact can be run to check each stdout stream for a problem. The entry point for running a test execution against the system is found at packages/swingset-runner-alt/bin/runner-alt. The swingset-runner-alt package is a modified version of the swingset-runner package. It was not possible to run the system using the original swingset-runner package (see issue), so slight modifications were made to parts of the code that setup the system in order to work around the problem. None of the functional parts of the code were changed (for example the kernel or liveslots code). In order to confirm the working of the adversarial testing driver we introduced errors into the SwingSet source code. The adversarial testing executions were able to detect the presence of all the introduced errors. Descriptions of each of the errors introduced can be found in intentionally_introduced_errors.md.

(GC) Model-checked TLA+ model of garbage collector protocol (GC) Overview The garbage collector protocol consists of three major psuedo-components which may be reasoned about in a modular manner. These are 1) the protocol between the kernel and liveslots, 2) the protocol between liveslots and the JavaScript engine garbage collector and 3) the comms vat protocol. We created a TLA+ model of 1) in this phase of the assessment. We modelled the protocol for the lifetime of a single object exported by one vat and imported by one vat following the liveslots protocol rules, and one vat ignoring the liveslots protocol rules. In this manner we check the protocol in the presence of malicious behavior. The model models the execution flow of kernel and vat (liveslots) syscalls and dispatch calls, with the effects of each relevant syscall and dispatch being applied to the model state. The syscalls modelled are

dropImport
retireImport
retireExport and the dispatch calls modelled are
dropExport
retireImport

retireExport The initial model state is the state in which an object has been exported by the exporting vat, and imported by both importing vats. The model execution follows a sequence of steps involved in freeing the object from each of the relevant kernel and liveslots data structures.

(GC) Results The TLC model checker explored the entire state space consisting of 311 distinct states in under 1 second of running time. The checker did not find any violation of any of the invariant properties that we

Excerpt (19995 of 42598 characters). Read the whole page on informalsystems/audits ↗

← Back to Documentation