BitMLx: Secure Cross-chain Smart Contracts For Bitcoin-style Cryptocurrencies
Federico Badaloni, Sebastian Holler, Chrysoula Oikonomou, Pedro Moreno-Sanchez, Clara Schneidewind
TL;DR
BitMLx introduces a domain-specific language for secure cross-chain smart contracts that operate across Bitcoin-like blockchains. It compiles BitMLx contracts into per-chain BitML contracts and generates honest-user strategies to coordinate multi-chain execution, with formal guarantees that honest participants end up with at least as much funds as in the BitMLx execution. The paper provides a rigorous compilation framework, an intermediate semantics layer, and a correctness proof that links BitMLx behavior to coherent per-chain executions, addressing adversarial schedulers and misbehavior via a compensation mechanism. Practical demonstrations include multichain donations, cross-chain payments with an exchange service, and multichain loans with mediators, alongside a discussion of assumptions, collateral, and limitations. Together, these results show a principled path to secure, scalable cross-chain applications without bespoke cryptographic protocols for each use case.
Abstract
A smart contract is an interactive program that governs funds in the realm of a single cryptocurrency. Yet, the many existing cryptocurrencies have spurred the design of cross-chain applications that require interactions with multiple cryptocurrencies simultaneously. Currently, cross-chain applications are implemented as use-case-specific cryptographic protocols that serve as overlay to synchronize smart contract executions in the different cryptocurrencies. Hence, their design requires substantial expertise, as well as a security analysis in complex cryptographic frameworks. In this work, we present BitMLx, the first domain-specific language for cross-chain smart contracts, enabling interactions with several users that hold funds across multiple Bitcoin-like cryptocurrencies. We contribute a compiler to automatically translate a BitMLx contract into one contract per involved cryptocurrency and a user strategy that synchronizes the execution of these contracts. We prove that an honest user, who follows the prescribed strategy when interacting with the several contracts, ends up with at least as many funds as in the corresponding execution of the BitMLx contract. Last, but not least, we implement the BitMLx compiler and demonstrate its utility in the design of illustrative examples of cross-chain applications such as multi-chain donations or loans across different cryptocurrencies.