How Formal Analysis and Verification Add Security to Blockchain-Based Systems

Abstract

We firstly figure out the security requirements needed for blockchain based systems and smart contracts. Then we propose technology layers for such systems and application and security considerations for each layer. Next we explore the applicability of formal analysis for each layer and pick three layers which are good targets of evaluation by formal analysis. Then, we propose the framework of apply- ing formal analysis to help secure blockchain-based systems. An explanation of the limitations of formal verification follows. At the end of this talk, we conclude the direction to the framework to design application code and system which facilitate formal analysis and formal verification.