This is the first in a series of posts introducing Solarkraft, a TLA+-based runtime monitoring solution for Soroban smart contracts. We start with an overview of smart contracts, their principal vulnerabilities, the traditional model of securing smart contracts, and how Solarkraft proposes a different approach.
Solarkraft was developed in collaboration by Igor Konnov, Jure Kukovec, Andrey Kuprianov, and Thomas Pani.
Since the advent of smart contract-enabled blockchains like Ethereum and Stellar, smart contracts have become the power engines underlying decentralized applications on blockchains. These self-executing contracts are computer programs that automate digital agreements and transactions, enabling trustless interactions without intermediaries. They hold considerable potential for finance, supply chains, and other digital coordination problems. They also come with a hard constraint: software bugs can be extraordinarily expensive.
The high cost of tiny errors
Unlike traditional software, smart contracts are immutable after deployment. Even if a vulnerability is found, it is not possible to patch a deployed smart contract on the fly. A smart contract transaction also cannot simply be undone. Once it has taken place, it is permanently recorded on the blockchain. It is now very unlikely that blockchain validators would agree to halt an entire blockchain to let contract authors remedy an issue.
Smart contract immutability and blockchain finality are a double-edged sword. They guarantee tamper-proof execution, but they also mean that patching a bug or reverting a malicious transaction after the fact may be impossible. A single error can have severe consequences:
- Financial losses. Attackers can exploit vulnerabilities to steal cryptocurrency or other assets locked in smart contracts. The DAO hack in 2016 resulted in the loss of over 60 million USD worth of ETH. In 2023, an attacker targeted Euler Finance and stole assets worth about 200 million USD from its flash-loan protocol.
- Service disruption and frozen funds. Bugs can render a dApp unusable or freeze funds. In 2017, a bug in the Parity multisig wallet contracts froze over 300 million USD worth of funds.
- Systemic risk. DeFi protocols are increasingly interconnected. A single bug can trigger a domino effect across protocols and ecosystems, as seen in flash-loan attacks against Cream Finance and related protocols.
The combination of risks emphasizes the need for thorough security practices throughout the development lifecycle of smart contracts.
The traditional model of securing smart contracts
Traditionally, securing smart contracts targets individual stages of the development lifecycle:
- Development. Smart contracts are coded by individual developers or teams. Solid teams write unit tests and integration tests. Advanced teams may use fuzz tests. This often happens in a development environment that does not reflect the final production environment.
- Staging and testing. Teams deploy contracts to a production-like testnet. Manual testing is common and easily misses important bugs. More experienced teams automate integration and end-to-end tests.
- Pre-release security audit. Before going live, security-conscious teams order security audits from audit firms, independent auditors, or contest platforms. Auditors review a fixed commit of the source code. Some use fuzzing or formal modeling, but many skip advanced techniques to keep time investment low.
- Deployment on mainnet. After known vulnerabilities have been patched, contracts go live. From that moment they must withstand persistent, creative, and destructive attackers.
The team behind Solarkraft has experience across several stages of blockchain and smart-contract development: developing fuzzing and model-based testing tools, developing formal-methods tooling, specifying and model-checking protocols and smart contracts, and auditing protocols from L1 chains to smart contracts.
Runtime monitors: guardians of the blockchain
The traditional security model is error-prone. It involves many actors with different skill levels and targets individual development phases with different methods. Runtime monitoring offers a security approach that cuts across development phases.
Runtime monitoring is a proactive approach that monitors a smart contract for expected and abnormal behavior as soon as it executes. It can happen during all phases of the development lifecycle and can supplement tests, audit reports, and other artifacts developed by the traditional approach.
The basic Solarkraft workflow is:
- Monitor specification. Developers define a runtime monitor that captures expected contract behavior in TLA+. These specifications outline preconditions, postconditions, and failure conditions.
- Monitoring in action. The Solarkraft fetcher observes the blockchain for contract invocations and retrieves transaction data.
- Verification and catching deviations. The Solarkraft verifier compares on-chain transaction data to expected behavior defined in the monitor specification. This off-chain component runs the Apalache model checker.
- Alerts. If the verifier detects a deviation, it can take predefined actions such as pausing a contract or raising an on-chain or off-chain alert.
Solarkraft introduces two ideas that later posts explore in detail: small modular monitor specifications and a hybrid monitoring approach.
Advantages of runtime monitoring
- Proactive approach. Runtime monitoring can catch bugs close to execution time, limiting or preventing financial losses and disruptions.
- Continuous monitoring. Unlike tests and audits, runtime verification provides ongoing checks throughout a contract's lifecycle.
- Early detection. Runtime monitoring can identify potential issues early in execution, allowing quicker mitigation and reducing the attack window.
In the following posts, we explore how to specify contract behavior using TLA+, how Solarkraft's specification and monitoring strategies work, and how runtime verification can be integrated into development workflows for more secure and reliable smart contracts.
Development of Solarkraft was supported by the Stellar Development Foundation with an Activation Award from the Stellar Community Fund of 50,000 USD in XLM.
