Penerapan Metode Model Checking Untuk Menemukan Distributed Concurrency Bug Pada Ethereum

ARBA SASMOYO, Dr-Ing, MHD. Reza M.I. Pulungan, M. Sc.

2019 | Tesis | MAGISTER ILMU KOMPUTER

Distributed Concurrency Bug (DC bug) merupakan bug yang terjadi akibat terjadinya interaksi antara beberapa node pada suatu sistem terdistribusi. DC bug terjadi akibat oleh faktor-faktor yang bersifat non-deterministic, sehingga sulit untuk ditemukan dan dicegah. Suatu sistem terdistribusi biasanya memiliki banyak kemungkinan kejadian non-deterministic yang dapat terjadi. Oleh karena itu akan sangat sulit bagi pengembang untuk mengantisipasi semua kemungkinan tersebut. Model checking merupakan suatu metode yang digunakan untuk mengeksplorasi state suatu sistem dan menemukan state yang tidak diinginkan. Biasanya model checking bekerja pada model dari suatu sistem. Penelitian ini mencoba untuk menggunakan model checking untuk menemukan DC bug pada implementasi Ethereum. Model checking akan mencari state yang mengakibatkan terjadinya crash pada salah satu node pada network Ethereum. Hasil penelitian menunjukkan bahwa model checking dapat mengeksplorasi state yang dihasilkan dari interaksi beberapa node Ethereum dan dapat menemukan bug yang mengakibatkan crash pada salah satu node. Akan tetapi integrasi model checker dengan Ethereum dilakukan dengan pengubahan kode pada Ethereum. Walaupun integrasi menjadi lebih fleksibel, cara ini menghasilkan integrasi yang dimungkinkan untuk tidak kombatibel dengan Ethereum versi berbeda. Selain itu, model checker harus diarahkan untuk menghadang aksi lokal tertentu, karena tidak dimungkinkan untuk menghadang semua aksi lokal yang mungkin terjadi dengan mengubah kode secara manual.

Distributed Concurrency Bug (DC bug) is a bug that occurs because of interaction between nodes in distributed systems. DC bug is caused by non deterministic factors, so it is hard to find and to prevent. A distributed systems usually have many possible non deterministic events. It will be hard for developers to anticipate all those possible events. Model checking is a method that is used to explore state of a system and find unwanted states. Usually model checking runs on a model of a system. This research tries to use model checking to find DC bug in Ethereum's implementation. Model checking will find state that causes a node to crash in Ethereum network. Results showed that model checking was able to explore states from the interaction of Ethereum nodes and find a bug that causes crash on a node. However integration between model checker and Ethereum was done by modifying Ethereum's code. Although the integration was more flexible, it caused the integration to have a chance of incompatibility between different Ethereum versions. In addition, model checker had to be guided to intercept relevant local action, because it is not possible to intercept all possible local actions by modifying the code manually.

Kata Kunci : distributed concurrency bug, distributed model checking, ethereum, sistem terdistribusi/distributed concurrency bug, distributed model checking, ethereum, distributed system