informal-agoric-report-phase1

Formal Methods Assessment Report

Agoric Swingset Kernel and Userspace, Phase 1: Source Code Inspection and Protocol Modelling

09.11.2021 Initial revision: 08.07.2021

Contents Assessment overview 4 The project . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 The Agoric SwingSet Platform . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Scope of this report . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Conducted work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 Timeline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

Assessment Dashboard 7

Assessment Scope 8

TLA+ SwingSet Kernel Model 9 Kernel types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Kernel variables and actions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Kernel execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Kernel tests . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Future model evolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

Findings 14

IF-AGORIC1-01: Mismatched number of arguments 15 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

IF-AGORIC1-02: Incomplete type-tracking in the kernel 17 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

IF-AGORIC1-03: Undocumented function format change 18 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

IF-AGORIC1-04: Problematic pattern in processQueueMessage 20 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

IF-AGORIC1-05: Unrestricted number of vat slots per vat 21 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 Recommendation: . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

IF-AGORIC1-06: Unrestricted length of vat slot IDs 23 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

IF-AGORIC1-07: Scattered updates to kernel tables 24 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

IF-AGORIC1-08: Possible cycles in promise resolutions 25 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

IF-AGORIC1-09: Possible loss of vat termination events 26 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

IF-AGORIC1-10: Inconsistencies in vat bookkeeping 27 Involved artifacts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Recommendation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

Assessment overview The project In April 2021, Agoric engaged Informal Systems to conduct a formal methods assessment over the documentation and the current state of the implementation of Agoric SwingSet Kernel: the core component of the Agoric smart contracts platform.

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 transferrable, 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 The agreed-upon workplan consisted of the following tasks: • Task C.1. Examine the documentation and source code of SwingSet kernel, excluding the liveslots. – a rolling review over the assessment period, starting from commit 23ed67c0 • Task M.0. Construct the TLA+ model of the SwingSet kernel, modeling key interactions in the kernel: – interactions with vats via the syscall interface; – lifetime and evolution of kernel objects and promises; • Task P.1. Perform bounded verification of the TLA+ model focusing on OCAP model requirements. Taking into account the large size of the code base, it was decided that Informal Systems would only perform the source code and documentation review limited to the scope necessary to construct the TLA+ kernel model. Moreover, due to the inherent complexity of formal protocol modelling, it was decided that the scope of the assessment be determined by the time span allocated for it with some tasks continuing if necessary during the follow-up phases. This report covers Task C.1 and Task M.0 that were conducted May 6 through June 29, 2021 by Andrey Kuprianov, Senior Research Engineer at Informal Systems; Task P.1 turned out to be infeasible due to the timing constraints, and will be conducted in a follow-up phase.

Conducted work Starting May 6, Informal Systems conducted an assessment of the existing documentation and the code. Agoric gave a one-hour presentation with an overview over the protocol and a code walk-through with focus on the scope of the assessment. Our team started with reviewing SwingSet kernel documentation, to get an overview of the kernel design principles, and with the review of some critical components of Hardened JavaScript, which are foundational

to platform security. We then continued with the review of the SwingSet kernel source code; the code inspection was limited to the scope necessary to construct the TLA+ kernel model. After gaining a general understanding of kernel protocols and interactions, we continued with the modelling effort, and accurately captured interactions within the kernel in the TLA+ Swingset kernel model. Over the Keybase channel between Agoric and Informal we shared documents with preliminary findings, which we discussed during online meetings. In this document, we distilled the central findings into numbered findings, as well as briefly described the characteristics of the constructed TLA+ kernel model. Moreover, we opened issues for the findings in the Agoric-SDK repository.

Timeline • 06.05.2021: Start of assessment • 06.05.2021: Kickoff meeting with a code walk-through (1 hour) • 21.05.2021: Meeting Agoric/Informal with discussion of the first set of issues • 14.06.2021: Meeting Agoric/Informal with discussion of the second set of issues, and the first version of the TLA+ kernel model • 29.06.2021: Meeting Agoric/Informal with discussion of the final version of the TLA+ kernel model • 29.06.2021: End of assessment • 08.07.2021: Submission of the 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 well organized, well documented, and faithful to the specification. Despite the general high quality of the implementation work, we found several significant issues regarding code quality, data representation, code organization, and divergence from the specification. These are detailed in the relevant findings. The main source of issues seems to be the choice of JavaScript as the kernel implementation language with its weak and dynamic typing. While this choice is convenient in some cases and makes the implementation more concise, introducing strict type tracking into the kernel seems to be able to bring substantial benefits, and to eliminate many sources of potential bugs. As the first step in that direction, we have provided within the scope this assessment a typed TLA+ specification of the core kernel functionality. Already the process of the model construction has helped to identify some protocol and implementation issues; continuing this thread with model checking and model-based testing should bring a high level of assurance in the kernel correctness. We have also identified two resource exhaustion attacks that have not yet been dealt with in the current implementation, but may be resolved through the upcoming addition of metering to the kernel.

Assessment Dashboard Target Summary • Name: Agoric SwingSet Kernel • Specification & Code Version: commits 23ed67c0 through 5e1024e4 • Type: Specification and Implementation • Platform: JavaScript Engagement Summary • Dates: 10.05.2021 – 29.06.2021 • Method: Manual review & formal protocol modelling • Employees Engaged: 1 • Time Spent: 6 person-weeks Severity Summary

Finding Severity # Findings High-Severity Issues 0 Medium-Severity Issues 4 05, 08, 09, 10 Low-Severity Issues 5 01, 02, 03, 04, 06 Informational-Severity Issues 1 07 Total 10

Finding Severities • Informational: The issue does not pose an immediate risk (it is subjective in nature). Findings with informational severity are typically suggestions around best practices or readability. • Low: The issue is objective in nature, but the security risk is relatively small or does not represent a security vulnerability. • Medium: The issue is a security vulnerability that may not be directly exploitable or may require certain complex conditions in order to be exploited. • High: The issue is an exploitable security vulnerability. Category Breakdown

Finding Category # Findings Protocol 0 Implementation 4 05, 06, 08, 09, Code Structure 6 01, 02, 03, 04, 07, 10 Total 10

Finding Categories • Protocol: A flaw or problem in an abstract protocol or algorithm. • Implementation: A problem with the source code. For example a bug, a divergence from a specification, or a poor choice of data structure. • Code structure: A problem that impacts the extent to which the project is maintainable and understandable by developers in the long term. • Documentation: A lack of documentation, or insufficient clarity, accuracy, understandability or readability of existing documentation.

Assessment Scope The scope of the assessment has been defined as the Agoric SDK SwingSet kernel, with minimal dependencies necessary to construct the formal kernel model. During the assessment, we have inspected the following source repositories: • endojs/endo/packages/ses: – commit f7dcf050 • Agoric/agoric-sdk/packages/SwingSet/kernel (a rolling review over the assessment period): – 10.05 - 19.05: commit 23ed67c0 – 20.05 - 26.05: commit 0cae5d77 – 27.05 - 01.06: commit 069201d6 – 02.06 - 06.06: commit 9feea167 – 07.06 - 10.06: commit ae2ac52fc – 11.06 - 29.06: commit 5e1024e4

TLA+ SwingSet Kernel Model One of the main goals of the formal methods assessment was constructing a formal TLA+ model of the SwingSet kernel that faithfully represents interactions with vats via the syscall interface as well as the lifetime and evolution of kernel objects and promises.

Kernel types The file kernel_typedef.tla describes kernel-specific types and typed constants. Here is the excerpt with the most important kernel types:

Kernel variables and actions The main model file kernel.tla contains: • variables (representing the kernel state) • parameterized actions (which modify the state) • action preconditions (when are the action parameters considered valid) • variables that are changed / unchanged by each action The kernel state in this version of the model is described by the following 13 state variables:

Each parameterized action is modelled after the source code, by reproducing at the abstract level what happens in the implementation. Here we show only one such parameterized action, CreateVat:

Kernel execution The file kernel_exec.tla defines execution semantics for the kernel: • constants (representing the model search space) • initialization of state variables and constants • externally observable actions • scheduling of actions The model concisely describes the whole kernel state (E stands for Exported, I for Imported, V for Vat, K for Kernel, O for Object, P for Promise; thus e.g. EVO stands for Exported Vat Object):

This file also defines the externally observable actions and steps based on the parameterized actions from kernel.tla Actions are defined as follows: • Do not change unchanged variables (this allows to search over all possible inputs) • Save the action being executed in the “action” variable

• If the action precondition is satisfied, perform an update • Otherwise do not perform an update, but set the “error” variable instead Steps differ from actions in that they quantify existentially on action parameters, using model constants

The execution semantics is defined in terms of prioritized processing of enabled steps:

Kernel tests Finally, the file kernel_test.tla defines unit tests for the kernel model; those tests serve as simple soundness checks for the model, ensuring e.g. that all variables are updated correctly on all logical branches. Below are a couple of tests for the CreateVat action which make sure that the creation of (un)known vat is processed soundly.

Future model evolution The current version of the SwingSet kernel model accurately represents the interactions between kernel and vats, and the life cycle of kernel objects and promises. Unfortunately, the precise model is too heavy in terms of the state space for the invariants to be efficiently model checked. We can identify the following future steps: • Formulate OCAP model properties (such as “connectivity begets connectivity”) as model invariants; • Construct specialized, abstracted versions of the main kernel model for: – OCAP invariants; – Kernel garbage collection protocol and its invariants; – Kernel scheduling/metering and its invariants; • Prove refinement relations between the main model and its abstracted variants; • Perform bounded verification of the above invariants on the abstracted variants of the kernel model; • Construct and execute model-based tests, thus providing security assurance via checking implementation conformance to the formal specification.

Findings ID Title Severity Category Issue IF-AGORIC1-01 Mismatched number of arguments Low Structure sdk#3172 IF-AGORIC1-02 Incomplete kernel type-tracking Low Structure sdk#3173 IF-AGORIC1-03 Undocumented function format change Low Structure sdk#3174 IF-AGORIC1-04 Problematic pattern in processQueueMessage Low Structure IF-AGORIC1-05 Unrestricted number of slots per vat Medium Impl. sdk#3243 IF-AGORIC1-06 Unrestricted length of vat slot IDs Low Impl. sdk#3242 IF-AGORIC1-07 Scattered updates to kernel tables Info Structure sdk#3312 IF-AGORIC1-08 Possible cycles in promise resolutions Medium Impl. sdk#3313 IF-AGORIC1-09 Possible loss of vat termination events Medium Impl. sdk#3315 IF-AGORIC1-10 Inconsistencies in vat bookkeeping Medium Structure sdk#3316

Excerpt (19999 of 40793 characters). Read the whole page on informalsystems/audits ↗

← Back to Documentation