Invited Lecture: Formal Analysis and Verification and Blockchain-Based Systems

Abstract

For long years, formal methods and formal analysis usually collect much attention in designing mechanisms, products and systems, to eliminating errors and troubles. Communication protocol and cryptographic protocol is one of the important area where formal analysis is applied to reduce the possibility of attacks and vulnerability. Currently we use many cryptographic protocols in our life and they are already fundamental of our communication. Recently, we are proceeding the next stage where cryptographic protocol acts a fundamental role of ecosystem. Bitcoin and Blockchain opens our eyes for decentralized ecosystem by combination of cryptographic protocol, P2P network and consensus algorithm. At this moment, the security of this well-balanced but complicated combination is not fully proven. Moreover, blockchain is a foundation of many applications and we should care about security of entire application and systems based on blockchain technology. In this tutorial, we will study how formal analysis helps evaluating the security of entire blockchain based systems. We analyze the entire blockchain based system with dividing into 6 security layers, then explore the possibility of applying formal analysis to each layers with examples. We also discuss a way to securing smart contract, which is one of the most promising application of blockchain technology. Research on security of blockchain based system is in its quite early stage, therefore, we need more research on formal analysis theory and methodology. We will discuss the further research directions to securing next foundation of trust.