Earlier this year, Agoric engaged Informal Systems to begin formally verifying the kernel component of the JavaScript VM (SwingSet), a foundational layer of the Agoric stack that partitions risk by dividing the execution environment into vats. As the isolation properties and communications functionality that SwingSet provides across vats, promises, and objects are integral to the safety guarantees of the Agoric ecosystem, it is important to assess the correctness and soundness of such critical code.
Today, we are excited to announce a long-term partnership with Informal Systems that will further our formal verification efforts, and to share the formal methods assessments reports focused on some of Agoric’s most critical code.
Formal Verification, the ultimate math exam
As software becomes increasingly complex, it is important to be able to build confidence in its security, efficiency, and resilience. Testing throughout the development process is an important step towards understanding how code functions, but even the most rigorous unit testing, linting, fuzzing, and static/dynamic analysis can not prove that a code implementation is correct, that a specific architectural property exists, or that there are no bugs or unexpected functionalities lurking under the surface.
When an extremely high degree of confidence in software integrity is required, formal verification methods are put to use in order to prove the properties and behavior of critical software like cryptography, communication protocols, or even seL4, which is widely considered to be the most secure operating system in existence. By using mathematical reasoning and proofs to verify that a system is an accurate representation of its specified design and behavior, formal methods analysis can provide strong mathematical assurances that software is sound. Additionally, formal validation provides a framework and tooling that enables reasoning about code and its expected behavior, which is especially important for developing an understanding of complex code. Through automated testing and model checking, it is possible to gain assurance that critical code has high levels of liveness, safety, and integrity.
On their own, security assessments and various code analysis techniques can not provide strong assurances about the security and integrity of source code. As part of a layered approach to security that includes application security reviews, third party vulnerability disclosure, comprehensive threat modeling, purple teaming, and rigorous software testing, the vulnerability assessments and formal methods assessments that are underway in the Agoric stack are on beginning to provide strong safety and security assurances that will reduce risk for everyone in the Agoric ecosystem.
Making it formal with Informal Systems
Informal Systems is a leading provider of formal methods analysis in the blockchain space. For the Cosmos ecosystem, with $130 billion in assets under management, they performed protocol design and verification of the Tendermint consensus protocol and Inter Block Chain (IBC) protocol. As core contributors to the Cosmos Network, the Informal team has made significant code contributions to Tendermint consensus, the IBC protocol, and to developing tools and processes that improve the quality and experience of software engineering. Because of their strong track record and ongoing efforts in formally verifying the code that comprises the Cosmos Network, the Informal Systems team was a natural fit for an initial formal methods assessment of the Agoric code, and for a year-long engagement that seeks to formally verify major components of the Agoric ecosystem.
At best, an assessment is a snapshot that captures a code’s strengths and weaknesses. Formal verification requires a significant investment of time and effort to yield results, especially when modeling an ever-changing codebase that is under active development. In order to continuously demonstrate that code is sound and correct, it is necessary to ensure that models reflect the latest code changes, and that model checking happens when a code change is introduced. As part of our year-long engagement with Informal Systems, keeping our models up to date is an important goal. As the TLA+ models continue to grow and improve alongside the Agoric codebase, we look forward to seeing increasingly complex proofs that can deeply examine critical properties of code all the way into the smart contract layer. As part of our long-term engagement, Informal Systems will continue to contribute to the wider fields of software verification and the TLA+ community by sharing best practices and findings in the form of conference talks and papers. To learn more about what they’ve been able to achieve so far, tune in to their Twitter account or read the first published paper to emerge from our partnership, “TLA+ Specification and Model Checking of the Agoric Smart Contracts Kernel” by Andrey Kuprianov and Daniel Tisdall. (The talk from the TLA+ Conference 2021 is great, too!)
So far, so good in the SwingSet Kernel
During the first phase of the engagement that focused on source code inspection and protocol modeling, the Informal Systems team began reviewing the SwingSet documentation and source code to begin developing a deep understanding of the system. As their expertise in the code grew, they began using TLA+ to construct a model of the kernel code with a focus on interactions and the life span of objects and promises. This initial model of the code became an invaluable asset that would later be used for a deeper inspection of the code in the next phase.
During the second phase of the engagement, the Informal Systems team iterated on their knowledge of the SwingSet source code, and began adversarial testing of user space vat interactions, and modeling and verification of the garbage collection protocol.
Within the scope of Phase 1 and 2 assessments:
No high severity issues were discovered.
Fifteen findings emerged in the areas of code structure, data representation, code organization, and divergence from the specification. The Informal Systems team has also provided valuable feedback that will yield improvements in Agoric’s kernel documentation for all.
An early examination of the object capabilities model in Phase 1 suggests that the implementation is sound.
No significant semantic errors in either the garbage collector protocol or the inter-vat communication implementation were found.
During Phase 2, none of the pathways tested or modeled deviated from the expected behavior.
To learn more about Phases 1 + 2 of Informal Systems’ work with Agoric, read the reports or learn more about the findings on Github.
Thanks for reading. You can join the Agoric community on Twitter, Discord, Telegram, and LinkedIn, subscribe to our monthly newsletter, and catch us at upcoming events.
