※ All videos of this session are available in here
Seong Ju Kang, Korea Post
Sachiko Yoshihama, IBM Research – Tokyo
Grigore Rosu, University of Illinois at Urbana-Champaign
Title : Blockchain-based Postal Services at Korea Post
Seong Ju Kang
President, Korea Post
Abstract : Korea Post’s challenge to seek for new business opportunities from blockchain technology is underway. Korea Post is reviewing to apply blockchain technology to each of its business segments: postal, savings, and insurance. For postal business, we are planning to introduce mobile e-post box system which enables a reliable transmission of e-mail by applying blockchain technology to prevent any forgery or modification. For savings business, we are planning to realize a more affordable and time-saving foreign currency remittance service by sharing real-time records through blockchain technology. For insurance business, we have implemented an automatic request and payment process for insurance premium by linking the insurer with hospitals through blockchain technology. Korea Post will continue its efforts to enhance customer reliability on blockchain technology for a further development and to create new business values as one of the leading governmental agencies in the 4th Industrial Revolution field.
Bio : Seong Ju Kang has been serving as the President of Korea Post since November 2017. Prior to the present position, he served in various public positions such as Director General of ICT Policy and R&D Bureau, Ministry of Science and ICT (April 2008 to Nov. 2017), Minister-Counselor at the Permanent Delegation of Korea to the OECD (Feb. 2011 to Mar. 2013), Assistant Secretary to the President at the Office of the President (Feb. 2007 to Feb. 2008) and Director of ICT Planning and Coordination, Ministry of Information and Communications (Dec. 1997 to Feb. 2007), mainly covering ICT policy including e-government, cyber security, economic development, government innovation and regional development. Seong Ju Kang received his MS degree from Syracuse University and PhD degree from Penn State University in public administration and MIS. He also taught at the School of Public Administration at the Catholic University of Korea and Penn State University.
Senior Technical Staff Member, Senior Manager at IBM Research – Tokyo
Abstract : Blockchain started as a technology to underpin bitcoin, but it has been expanding its use cases beyond cryptocurrencies. Enterprise use of blockchain is gaining wide attention both in financial and non-financial industries. For example, blockchain and smart contracts allow organizations to share not only data but also application logic and rules, which enables transformation of cross-organizational business processes. However, the blockchain is still in its early stage as a business platform, and there are many challenges that need to be addressed. This talk will review key technical challenges of blockchain, such as security, privacy, and scalability in real-world examples, and how these challenges are being addressed in Hyperledger Fabric, one of the most significant open source projects for enterprise-level blockchain platforms. At the application layer, improving the safety of smart contracts is a pressing issue. Since each smart contract is a computer program that autonomously runs on blockchain, any errors in the logic could lead to financial losses. I will introduce our research project on automatic generation of smart contracts that allows to generate executable smart contract programs from human-understandable contract documents. Our approach is based on document templates and contract specification defined in a temporal logic-based language.
Bio : Dr. Sachiko Yoshihama is a Senior Technical Staff Member and Senior Manager at IBM Research – Tokyo. She leads a team that focuses on financial and blockchain solutions. Her research interest is to bring advanced concepts and technologies to practice and address real-world problems to transform industries. She served as a technical leader and advisor in a number of blockchain projects in Japan and Asia both in financial and non-financial industries. She joined IBM T.J. Watson Research Center in 2001, and then moved to IBM Research – Tokyo in 2003 and worked on research in information security technologies, including trusted computing, information flow control, and Web security. She served as a technology innovation leader at IBM Research Global Labs HQ in Shanghai in 2012, where she helped define research strategies for developing countries. She received Ph.D from Yokohama National University in 2010. She is a member of ACM, a senior member of Information Processing Society of Japan, and a member of IBM Academy of Technology.
Title : Formal Design, Implementation and Verification of Blockchain Languages
Professor of Computer Science, University of Illinois at Urbana-Champaign
Abstract : Many of the recent cryptocurrency bugs and exploits are due to flaws or weaknesses of the underlying blockchain programming languages or virtual machines. The usual post-mortem approach to formal language semantics and verification, where the language is firstly implemented and used in production for many years before a need for formal semantics and verification tools naturally arises, simply does not work anymore. New blockchain languages or virtual machines are proposed at an alarming rate, followed by new versions of them every few weeks, together with programs (or smart contracts) in these languages that are responsible for financial transactions of potentially significant value. Formal analysis and verification tools are therefore needed immediately for such languages and virtual machines. We present recent academic and commercial results in developing blockchain languages and virtual machines that come directly equipped with formal analysis and verification tools. The main idea is to generate all these automatically, correct-by-construction from a formal specification. We demonstrate the feasibility of the proposed approach by applying it to two blockchains, Ethereum and Cardano.
Bio : Grigore Rosu is a professor in the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where he leads the Formal Systems Laboratory (FSL), and the president and CEO of Runtime Verification, Inc (RV). His research interests encompass both theoretical foundations and system development in the areas of formal methods, software engineering and programming languages. Before joining UIUC in 2002, he was a research scientist at NASA Ames. He obtained his Ph.D. at the University of California at San Diego in 2000. He was offered the CAREER award by the NSF, the Dean’s award for excellence in research by the College of Engineering at UIUC in 2014, and the outstanding junior award by the Computer Science Department at UIUC in 2005. He won the ASE IEEE/ACM most influential paper award in 2016 (for an ASE 2001 paper), the Runtime Verification test of time award (for an RV 2001 paper), the ACM SIGSOFT distinguished paper awards at ASE 2008, ASE 2016, and OOPSLA 2016, and the best software science paper award at ETAPS 2002.