Stellar Community Fund

By Solarkraft

Solarkraft

SCF #29

$67.0K

Legacy v5.0 Community Award

Awarded

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

Products & Services

The product. Solarkraft is a runtime monitoring tool of Soroban smart contracts. It tests whether on-chain invocations of the smart contract conform to a developer-written monitor specification, and flags deviations. Runtime monitoring applies to all phases of the engineering lifecycle and aids developers, auditors, and users. Importantly, Solarkraft monitors are small snippets of code, not a monolithic specification. This makes them more accessible formal artifacts than usual. We provide additional details in the Technical Architecture document.

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. Another reason is that smart contracts are often written using an agile framework, where 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. The most common engineering practices (manual specification and code review, testing, security audits) are problematic in that they involve a lot of (incomplete) guessing, thus allowing critical bugs to sneak into production. Formal methods promise to deliver hard guarantees about the correctness of software. Even though we observe that formal methods enjoy stronger adoption in web3 than in web2, the use of formal methods is still quite limited in the blockchain space. In our experience, this is because formal specification is too far removed from an engineer's day-to-day practice.

Our solution. Solarkraft takes a middle ground between practical engineering methods and Formal Methods. Our goal is to connect and harden smart contract development and auditing via runtime monitoring backed by formal methods. We take into account our learnings from Atomkraft, the model-based testing tool that we developed for the Cosmos ecosystem in 2022, but propose the following novel and unique features:

We propose to write multiple modular monitor specifications for individual features, as opposed to a monolithic specification of the entire contract behavior. These are easier to write, read, and verify. Moreover, there is a good chance of reuse.

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”.

Solarkraft integrates well into the development process. This brings immediate value to engineers. They can both test their contracts and observe monitor alerts in the development stage, and keep running the same monitors after contract deployment.

Solarkraft will be of value to contract auditors too. Auditors often have limited time frames for discovering security bugs (in contrast to malicious actors!). Drawing from our experience in auditing projects in the Ethereum and Cosmos ecosystems, 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.

Integration with Stellar. When it comes to developing sustainable tooling, we believe in value-driven development:

To this end, our proposal for this Community Award is to engage with the Soroban community to collaborate on a real-life case study and support it in Solarkraft (e.g., with Blend, Phoenix, Soroswap, Xyclones, etc). Since Solarkraft is open source, we expect the learnings to benefit the entire Soroban developer community.

We will also address test generation for Soroban smart contracts, similar to a fuzzer. This generator will use the monitor specifications as guidance to generate both successful and failing test cases, similar to how we did it with Atomkraft. In contrast to Atomkraft, where we generated inputs for long executions of large specifications, Solarkraft will take a different approach: we generate inputs for a single step of the synchronous product of simple monitor specifications. This approach should scale much better than the standard bounded model checking of large specifications.

Immediate value is also generated by performing security audits. Our team could use Solarkraft in the future to audit Soroban contracts. Since Solarkraft is open source, we expect other auditing teams to get value out of it as well.

Why Stellar? Stellar is appealing because of the technical maturity of its ecosystem. We appreciate the thoughtfulness with which Stellar has been designed and implemented.

References Atomkraft Model-based Testing Tool: https://github.com/informalsystems/atomkraft

Requested Budget

$67.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.