Towards automated verification of Bitcoin-based decentralised applications

The Bitcoin language SCRIPT has undergone several technically non-trivial updates, still striving from security and minimal risk exposure. Up-to-date, formal verification is of strong interest for SCRIPT programs that validate the correctness of the Bitcoin decentralised ledger, and allow more and more sophisticated protocols and decentralised applications to be implemented on top of Bitcoin transactions. We propose SCRIFY, a comprehensive framework for the verification of the current SCRIPT language: a symbolic semantics and execution model, a model checker, and a modular (dockered), open-source verifier. Given the SCRIPT code that locks a Bitcoin transaction, SCRIFY returns the minimal information needed to successfully execute it and authorise the transaction. Distinguishably, SCRIFY features both recently added SCRIPT operators and an enhanced analysis, which considers prior information in the ledger. The framework is proved correct and validated through significant examples.