Security Analysis and Formal Verification on Blockchain and its Applications

At its core, blockchain is a distributed database that maintains a continuously growing list of records, called blocks, which are securely linked using cryptographic techniques. Each block contains a cryptographic hash of the previous block, a timestamp, and transaction data, making it virtually tamper-proof and resistant to modification. This structure ensures that once a block is added to the chain, the information it contains is immutable and can be trusted by all participants in the network. Blockchains have become an integrated part of our financial infrastructures. Being monetary yet fully automated, blockchain and its applications are unanimously deemed impracticable before undergoing necessary verification.

This monograph reviews the previous attempts at verifying two fundamental properties of blockchains: correctness and security. First, it summarizes and categorizes the correctness and security flaws encountered by real-world blockchains. Second, it systematizes the development of formal verification to address the flaws in blockchains, covering the aspects of models, specifications, and techniques. Third, it unveils the progress of security analysis for mitigating the flaws, unveiling the analysis principles being followed, the flaw oracles being devised, and the detection methods being used. Finally, the monograph summarizes the remaining challenges and visions of the trend in the near future.

Throughout this monograph, future blockchain verification advances are identified, especially in expanding its applicability, making specification generation easier, and discovering previously unknown vulnerabilities. By identifying gaps such as missing tools for infrastructure-level components and the difficulty of writing formal specifications, this monograph aims to motivate the development of more automated, intelligent, and practical verification frameworks.