Stellar Community Fund

By Solarkraft

Solarkraft: runtime monitoring

SCF #24

$50.0K

Legacy v5.0 Activation Award

Awarded

Runtime monitoring of Soroban smart contracts to aid developers and auditors in finding critical bugs before and in production

Products & Services

The product. Solarkraft is a tool for runtime monitoring of Soroban smart contracts. It tests whether a smart contract conforms to its specification during contract development, testing, and after contract deployment on the Stellar blockchain. The contract specification is written as an ensemble of TLA+ specifications, each capturing a property of the contract’s expected behavior. As an example, consider the timelock contract from the repository of Soroban examples:

Monitor 1 requires that “claim” is only called after “deposit”. Monitor 2 requires that the deposited balance equals the submitted amount. Monitor 3 requires that a claim can be made only by a claimant from the set of claimants that was passed earlier to the “deposit” method. Monitor 4 requires that the funds may be claimed only within the time bound that was passed to the “deposit” method earlier.

Solarkraft inspects invocations of the timelock contract’s methods in the history of Stellar transactions. Whenever Solarkraft finds a deviation from the expected behavior (as prescribed by the monitor specifications) it reports a monitoring alert. For more details, check the document on Technical Architecture. Importantly, monitors are small snippets of code, not an entire specification. This makes them more accessible formal artifacts than usual.

The problem. Smart contracts are backing billions of dollars in cryptocurrencies. At the same time, smart contracts are notoriously difficult to get right. One reason for that is that the code of the smart contracts is immutable, that is, they cannot be quickly patched, once deployed on mainnet. In this sense, smart contracts are further away from Web 2 software, which can be patched on the spot, and closer to hardware, where a single bug may cost millions of dollars. Another reason is that smart contracts are often written using an agile framework, when the requirements are figured out on-the-go, often by writing unit tests and integration tests. As a result, the expected behavior is poorly documented, if at all.

Formal methods promise to deliver hard guarantees about correctness of software. Even though we observe that formal methods enjoy stronger adoption in Web 3 than in Web 2, the use of formal methods is still quite limited in the blockchain space. In our experience, there are several hurdles in adoption of formal methods:

The value of a formal specification is not clear, unless it is directly connected to the source code and tools understood by engineers. Similar to code, engineers and researchers alike tend to write monolithic specifications that capture the entire contract behavior. As a result, the specification becomes as complex as the source code, just written in a specification language.

Consequently, the most common engineering practice looks as follows:

Engineers develop their contracts and write unit tests. Good engineering teams also write integration and end-to-end tests, and employ fuzzing or property-based testing. At some point, the contracts are deployed to a testnet, where the users are asked to break them; it is essentially a manual process. Since the users are not intimately familiar with the expected contract behavior, they just guess the intuitive properties of the contracts. After running the contracts on the testnet, the engineering team orders a security audit (sometimes, two or three), in which security experts try to break the contracts in all possible ways. Levels of expertise among auditing companies also vary greatly, and not being familiar with the contracts, the auditors are again trying to guess the core system properties to break.

As can be seen, the above practice is problematic in that it involves a lot of (incomplete) guessing, thus allowing critical bugs to sneak into production. Our goal is to connect and harden these activities via runtime monitoring using formal methods.

Our solution. To address the above-mentioned problems and strengthen current practices, we propose Solarkraft. In this project, we take into account our learnings from Atomkraft, the model-based testing tool that we developed for the Cosmos ecosystem in 2022, to develop the following novel and unique features:

We propose to write multiple monitor specifications for individual features, as opposite to a monolithic specification of the contract behavior. Individual monitor specifications are easier to write, read, and verify. Moreover, there is a good chance that some of these partial specifications may be reused across the contracts. For instance, a monitor that captures token transfer does not have to differ for different contracts. We map contract values to specification values, which is known as “abstraction”. This will be easier and more natural to do than mapping specification values to contract values, which is known as “concretization”. We integrate our monitoring tool into the development process. This brings immediate value to the engineers. Not only can they test their contracts and observe monitor alerts in the development stage, the monitors can still be run after the contract deployment. Solarkraft will be of value to contract auditors too. Auditors often have a very tight time schedule for discovering security bugs. In our experience when auditing projects in the Cosmos ecosystem and participating in Code4rena competitions, it is quite challenging to write a complete specification that faithfully represents a collection of contracts (though we managed to do that in a few cases). With the approach outlined in this proposal, abnormal contract behavior can be discovered much faster, by writing simpler abstract monitor specifications.

Solarkraft is a tool on top of the Apalache model checker. Apalache is one of the two main model checking engines for TLA+, the specification language developed by Leslie Lamport, together with the model checker TLC. Unlike TLC, which is an explicit state model checker, Apalache is symbolic, thus allowing one to handle very large or unbounded data domains, and which scales on some industrial examples better than TLC. We have been developing Apalache since 2016: The project started at TU Wien (Austria), then continued at Inria Nancy (France), Interchain Foundation (Switzerland), and Informal Systems (Canada/Switzerland/Austria). Apalache has always been published under the Apache 2.0 license, making it the perfect platform to leverage and extend for Solarkraft.

When it comes to the question of developing a sustainable product, we believe that the easiest way to bootstrap Solarkraft is to use it in the security audits. In the future, our team could use Solakraft to audit Soroban contracts. Since Solarkraft will be open source, other auditing teams may get value out of it too. Also, engineers may see value in developing monitor specifications, leading to more robust smart contracts that are easier to develop, audit and verify.

On a technical side, we do not address the issue of generating inputs for the smart contracts. In the activation phase, we assume that this could be done either manually, or by employing a fuzzer (or a set of generators as used in property-based testing). In the future phase, we could automatically generate input values with Apalache, similar to how we did it with Atomkraft.

Finally, you may wonder why we propose to write monitors in TLA+ instead of Rust. There are several reasons:

Since we want an individual monitor to capture partial behavior of the contract, abstract transitions of a single monitor will be non-deterministic in most cases. TLA+ naturally expresses non-deterministic behavior, whereas Rust is deterministic by design. If we proceed to input generation in the post-activation phases, it is much easier to solve symbolic constraints for a high-level specification language such as TLA+ than for a real implementation language such as Rust, which has to take care of every single execution detail including memory management. In addition to that, we see value in the ability to analyze the behavior of the monitors with the model checker. For instance, we could check whether a monitor is never stuck, which would indicate a contradiction in the specification.

Requested Budget

$50.0K

Team

We are a team of independent researchers in formal methods and security.

Dr. Thomas Pani (project lead). Website: https://thpani.net/ | Twitter: https://twitter.com/audithare | LinkedIn: https://www.linkedin.com/in/thpani/
Igor Konnov, PhD. Website: https://konnov.phd | Twitter: https://twitter.com/k0nn0v | LinkedIn: https://www.linkedin.com/in/igor-konnov-at/

We have a proven track record of past collaboration at TU Wien and Informal Systems and as independent contractors, that is, both in an academic environment as well as in the blockchain industry. As part of larger teams, we have been building products such as the Apalache model checker, the Atomkraft model-based testing tool, and the Quint specification language. We have a solid experience of working independently and remotely. In addition to that, we are all located in Vienna (Austria), which makes it possible for us to coordinate offline, when needed. Our combined work experience spans TU Wien: Vienna University of Technology (Austria), Inria Nancy (France), Google (USA), and Informal Systems (Canada/Switzerland/Austria). Together we have strong expertise in applied and fundamental formal methods research; development of verification, testing, and security tools; software engineering; software & network security; and blockchain security audits. In formal methods, we have academic and industry experience in modeling and verification of distributed and concurrent systems, design of model checking algorithms and satisfiability checking procedures. Our expertise and independence from any company guarantees our ability to achieve the stated goals, thus adding resiliency to the project.