Treffer: Formal verification of safety properties of epoch processing in Beacon Chain.
Title:
Formal verification of safety properties of epoch processing in Beacon Chain.
Authors:
Rashid M; Department of Computer Science, IBADAT International University Islamabad, Pakpattan, Pakistan., Rasool I; Department of Computer Science, COMSATS University Islamabad, Sahiwal, Pakistan., Afzaal H; Department of Computer Science, University of Engineering and Technology, Lahore, Pakistan. hamraafzaal@hotmail.com.; Department of Computer Science, Information Technology University of the Punjab, Lahore, Pakistan. hamraafzaal@hotmail.com., Zafar NA; Department of Computer Science, COMSATS University Islamabad, Sahiwal, Pakistan.
Source:
Scientific reports [Sci Rep] 2025 Nov 22; Vol. 15 (1), pp. 43522. Date of Electronic Publication: 2025 Nov 22.
Publication Type:
Journal Article
Language:
English
Journal Info:
Publisher: Nature Publishing Group Country of Publication: England NLM ID: 101563288 Publication Model: Electronic Cited Medium: Internet ISSN: 2045-2322 (Electronic) Linking ISSN: 20452322 NLM ISO Abbreviation: Sci Rep Subsets: PubMed not MEDLINE; MEDLINE
Imprint Name(s):
Original Publication: London : Nature Publishing Group, copyright 2011-
References:
Zheng, Z., Xie, S., Dai, H.-N., Chen, X. & Wang, H. Blockchain challenges and opportunities: A survey. Int. J. Web Grid Serv. 14, 352–375 (2018). (PMID: 10.1504/IJWGS.2018.095647)
Afraz, N., Wilhelmi, F., Ahmadi, H. & Ruffini, M. Blockchain and smart contracts for telecommunications: Requirementsvs. cost analysis. IEEE Access (2023).
Iansiti, M. et al. The truth about blockchain. Harv. Bus. Rev. 95, 118–127 (2017).
Monrat, A. A., Schelén, O. & Andersson, K. A survey of blockchain from the perspectives of applications, challenges, and opportunities. IEEE Access 7, 117134–117151 (2019). (PMID: 10.1109/ACCESS.2019.2936094)
Saari, A., Vimpari, J. & Junnila, S. Blockchain in real estate: Recent developments and empirical applications. Land Use Policy 121, 106334 (2022). (PMID: 10.1016/j.landusepol.2022.106334)
Johnson, J. Is cardano a serious rival to ethereum? Available at SSRN 3886108 (2021).
Pierro, G. A. & Tonelli, R. Can solana be the solution to the blockchain scalability problem? In 2022 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER), 1219–1226 (IEEE, 2022).
Armknecht, F., Karame, G. O., Mandal, A., Youssef, F. & Zenner, E. Ripple: Overview and outlook. In Trust and Trustworthy Computing: 8th International Conference, TRUST 2015, Heraklion, Greece, August 24-26, 2015, Proceedings 8, 163–180 (Springer, 2015).
Lokhava, M. et al. Fast and secure global payments with stellar. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, 80–96 (2019).
Buterin, V. et al. Ethereum white paper. GitHub repository 1, 22–23 (2013).
Kim, C. Ethereum 2.0: How it works and why it matters. Coindesk: https://www.coindesk.com/wp-content/uploads/2020/07/ETH-2.0-072120. pdf (2020).
Tucci-Piergiovanni, S. Keynote: Blockchain consensus protocols, from bitcoin to ethereum 2.0. In 2022 IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events (PerCom Workshops), 1–1 (IEEE, 2022).
Neuder, M., Moroz, D. J., Rao, R. & Parkes, D. C. Low-cost attacks on ethereum 2.0 by sub-1/3 stakeholders. arXiv preprint arXiv:2102.02247 (2021).
Buterin, V. Ethereum: platform review. Opportunities and challenges for private and consortium blockchains 45, 1–45 (2016).
Buterin, V. et al. Combining ghost and casper. arXiv preprint arXiv:2003.03052 (2020).
Cassez, F., Fuller, J. & Asgaonkar, A. Formal verification of the ethereum 2.0 beacon chain. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 167–182 (Springer, 2022).
Rashid, M., Rasool, I., Zafar, N. A. & Afzaal, H. Formal modeling and verification of validator voluntarily exit in ethereum 2.0 beacon chain. In 2023 2nd International Conference on Emerging Trends in Electrical, Control, and Telecommunication Engineering (ETECTE), 1–6 (IEEE, 2023).
Clarke, E. M. & Wing, J. M. Formal methods: State of the art and future directions. ACM Comput. Surv. (CSUR) 28, 626–643 (1996). (PMID: 10.1145/242223.242257)
Baier, C. & Katoen, J.-P. Principles of model checking (MIT press, 2008).
Alturki, M., Bogdanas, D. et al. An Executable K Model of Ethereum 2 . 0 Beacon Chain Phase 0 Specification (2019).
Alturki, M. A. et al. Verifying gasper with dynamic validator sets in coq. Tech. Rep. (2020).
Afzaal, H., Imran, M. & Janjua, M. U. Formal verification of persistence and liveness in the trust-based blockchain crowdsourcing consensus protocol. Comput. Commun. 192, 384–401 (2022). (PMID: 10.1016/j.comcom.2022.06.014)
Rashid, M. et al. Formal verification and validation of iot-based railway gate controlling system at level crossing. In 2024 IEEE 1st Karachi Section Humanitarian Technology Conference (KHI-HTC), 1–6 (IEEE, 2024).
Rashid, M., Rasool, I., Zafar, N. A. & Afzaal, H. Formal modeling and verification of justification and finalization of checkpoints in ethereum 2.0 beacon chain. In 2024 IEEE 1st Karachi Section Humanitarian Technology Conference (KHI-HTC), 1–6 (IEEE, 2024).
Afzaal, H., Zafar, N. A., Tehseen, A., Kousar, S. & Imran, M. Formal verification of justification and finalization in beacon chain. IEEE Access 12, 55077–55102. https://doi.org/10.1109/ACCESS.2024.3389551 (2024). (PMID: 10.1109/ACCESS.2024.3389551)
Li, E., Serbănută, T., Diaconescu, D., Zamfir, V. & Rosu, G. Formalizing correct-by-construction casper in coq. In 2020 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 1–3 (IEEE, 2020).
Palmskog, K., Gligoric, M., Pena, L., Moore, B. & Roşu, G. Verification of casper in the coq proof assistant. Tech. Rep. (2018).
Losa, G. & Dodds, M. On the formal verification of the stellar consensus protocol. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) (Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2020).
Zheng, K., Liu, Y., Dai, C., Duan, Y. & Huang, X. Model checking pbft consensus mechanism in healthcare blockchain network. In 2018 9th International conference on information technology in medicine and education (ITME), 877–881 (IEEE, 2018).
Chand, S., Liu, Y. A. & Stoller, S. D. Formal verification of multi-paxos for distributed consensus. In International Symposium on Formal Methods, 119–136 (Springer, 2016).
Thin, W. Y. M. M., Dong, N., Bai, G. & Dong, J. S. Formal analysis of a proof-of-stake blockchain. In 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), 197–200 (IEEE, 2018).
Alturki, M. A. et al. Towards a verified model of the algorand consensus protocol in coq. In Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part I 3, 362–367 (Springer, 2020).
Tholoniat, P. & Gramoli, V. Formal verification of blockchain byzantine fault tolerance (2019). https://doi.org/10.48550/ARXIV (1909).
Braithwaite, S. et al. Formal specification and model checking of the tendermint blockchain synchronization protocol (short paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) (Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2020).
Woos, D. et al. Planning for change in a formal verification of the raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 154–165 (ACM, 2016).
Afzaal, H., Imran, M., Janjua, M. U. & Gochhayat, S. P. Formal modeling and verification of a blockchain-based crowdsourcing consensus protocol. IEEE Access 10, 8163–8183 (2022). (PMID: 10.1109/ACCESS.2022.3141982)
Afzaal, H., Imran, M. & Janjua, M. U. Formal verification of fraud-resilience in a crowdsourcing consensus protocol. Computers & Security 131, 103290 (2023). (PMID: 10.1016/j.cose.2023.103290)
Alturki, M. A. et al. Towards a verified model of the algorand consensus protocol in coq. In Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part I 3, 362–367 (Springer, 2020).
Fedotov, I. & Khritankov, A. Statistical model checking of common attack scenarios on blockchain. arXiv preprint arXiv:2109.02803 (2021).
Yoo, J., Jung, Y., Shin, D., Bae, M. & Jee, E. Formal modeling and verification of a federated byzantine agreement algorithm for blockchain platforms. In 2019 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE), 11–21 (IEEE, 2019).
Zamfir, V. Casper the friendly ghost: A “correct-by-construction” blockchain consensus protocol. Ethereum Foundation (2017).
Chen, H., Pendleton, M., Njilla, L. & Xu, S. A survey on ethereum systems security: Vulnerabilities, attacks, and defenses. ACM Comput. Surv. (CSUR) 53, 1–43 (2020).
Westerkamp, M. & Diez, M. Verilay: A verifiable proof of stake chain relay. In 2022 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 1–9 (IEEE, 2022).
Liya, B. et al. Decentralized e-commerce platform implemented using smart contracts. In 2023 3rd International Conference on Smart Data Intelligence (ICSMDI), 23–27 (IEEE, 2023).
Ramos, D. & Zanko, G. Ethereum 2.0–a review of the causes and consequences of the upcoming update to ethereum’s mainnet. Mobileyourlife.Com (2022).
Jiang, Z. et al. Exploring smart contract recommendation: towards efficient blockchain development. IEEE Trans. Serv. Comput. 16, 1822–1832 (2022).
Muthe, K. B., Vemuru, T. S. T., Sharma, K. & Mohammad, N. S. Decentranet-an ethereum, proxy re-encryption and ipfs based decentralized internet. In 2020 11th International Conference on Computing, Communication and Networking Technologies (ICCCNT), 1–5 (IEEE, 2020).
Patel, S., Sahoo, A., Mohanta, B. K., Panda, S. S. & Jena, D. Dauth: A decentralized web authentication system using ethereum based blockchain. In 2019 international conference on vision towards emerging trends in communication and networking (ViTECoN), 1–5 (IEEE, 2019).
Villafiorita, A., Weldemariam, K. & Tiella, R. Development, formal verification, and evaluation of an e-voting system with vvpat. IEEE Trans. Inf. Forensics Secur. 4, 651–661 (2009). (PMID: 10.1109/TIFS.2009.2034903)
Barnat, J., Brim, L. & Havel, V. Ltl model checking of parallel programs with under-approximated tso memory model. In 2013 13th International Conference on Application of Concurrency to System Design, 51–59 (IEEE, 2013).
Kumar, N. S. & Kumar, G. S. Modeling and verification of timed automaton based hybrid systems using spin model checker. In 2016 IEEE Annual India Conference (INDICON), 1–8 (IEEE, 2016).
Rehman, A., Latif, S. & Zafar, N. A. Automata based railway gate control system at level crossing. In 2019 International Conference on Communication Technologies (ComTech), 30–35 (IEEE, 2019).
Iqbal, M., Zafar, N. A. & Alkhammash, E. H. Formally identifying covid-19 patients for providing medical services using drones. In 2021 International Conference of Women in Data Science at Taif University (WiDSTaif), 1–6 (IEEE, 2021).
Rashid, M. et al. Formal verification of aircraft departure procedure using spin model checker. In 2023 18th International Conference on Emerging Technologies (ICET), 165–170 (IEEE, 2023).
Rashid, M. et al. Verification of safety of aircraft arrival procedure using spin model checker. In 2023 International Conference on Frontiers of Information Technology (FIT), 262–267 (IEEE, 2023).
Rashid, M., Rasool, I., Zafar, N. A. & AlKhammash, E. Formal verification of blockchain and iot-based e-voting system using spin. In 2023 2nd International Conference on Emerging Trends in Electrical, Control, and Telecommunication Engineering (ETECTE), 1–6 (IEEE, 2023).
Rashid, M. et al. Formal modeling and verification of iot-based smart waste management system using spin. In 2023 17th International Conference on Open Source Systems and Technologies (ICOSST), 1–6 (IEEE, 2023).
Rashid, M. et al. Formal modeling and verification of iot-based smart transport system using spin model checker. In 2024 IEEE 1st Karachi Section Humanitarian Technology Conference (KHI-HTC), 1–6 (IEEE, 2024).
Cortier, V. et al. Machine-checked proofs of privacy for electronic voting protocols. In 2017 IEEE Symposium on Security and Privacy (SP), 993–1008 (IEEE, 2017).
Halder, R., Proença, J., Macedo, N. & Santos, A. Formal verification of ros-based robotic applications using timed-automata. In 2017 IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE), 44–50 (IEEE, 2017).
Alam, Q. et al. A cross tenant access control (ctac) model for cloud computing: Formal specification and verification. IEEE Trans. Inf. Forensics Secur. 12, 1259–1268 (2017). (PMID: 10.1109/TIFS.2016.2646639)
Alam, Q. et al. Formal verification of the xdauth protocol. IEEE Trans. Inf. Forensics Secur. 11, 1956–1969 (2016).
Khalil, U., Uddin, M., Alaidaros, H. & Akhunzada, A. Nfts for the unassailable authentication of iot devices in cyber-physical systems: An implementation study. In Conference on Creativity, Technology, and Sustainability, 87–95 (Springer Nature Singapore Singapore, 2024).
Akhunzada, A. et al. A formal framework for web service broker to compose qos measures. In 2015 SAI Intelligent Systems Conference (IntelliSys), 532–536 (IEEE, 2015).
Alam, M. et al. Formal modeling and verification of security controls for multimedia systems in the cloud. Multimed. Tools Appl. 76, 22845–22870 (2017). (PMID: 10.1007/s11042-017-4853-0)
Nazir, A. et al. A high-level domain-specific language for siem (design, development and formal verification). Clust. Comput. 20, 2423–2437 (2017). (PMID: 10.1007/s10586-017-0819-2)
Bibi, I., Akhunzada, A. & Kumar, N. Deep ai-powered cyber threat analysis in iiot. IEEE Internet Things J. 10, 7749–7760 (2022). (PMID: 10.1109/JIOT.2022.3229722)
Imran, M. et al. Research perspectives and challenges of blockchain for data-intensive and resource-constrained devices. IEEE Access 10, 38104–38122 (2022). (PMID: 10.1109/ACCESS.2022.3162096)
Akhunzada, A., Al-Shamayleh, A. S., Zeadally, S., Almogren, A. & Abu-Shareha, A. A. Design and performance of an ai-enabled threat intelligence framework for iot-enabled autonomous vehicles. Comput. Electr. Eng. 119, 109609 (2024). (PMID: 10.1016/j.compeleceng.2024.109609)
Woodcock, J., Larsen, P. G., Bicarregui, J. & Fitzgerald, J. Formal methods: Practice and experience. ACM Comput. Surv. (CSUR) 41, 1–36 (2009). (PMID: 10.1145/1592434.1592436)
Holzmann, G. J. The model checker spin. IEEE Trans. Softw. Eng. 23, 279–295 (1997). (PMID: 10.1109/32.588521)
Cavada, R. et al. The nuxmv symbolic model checker. In Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26, 334–342 (Springer, 2014).
Pakonen, A., Pang, C., Buzhinsky, I. & Vyatkin, V. User-friendly formal specification languages-conclusions drawn from industrial experience on model checking. In 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA), 1–8 (IEEE, 2016).
Pang, C., Pakonen, A., Buzhinsky, I. & Vyatkin, V. A study on user-friendly formal specification languages for requirements formalization. In 2016 IEEE 14th International Conference on Industrial Informatics (INDIN), 676–682 (IEEE, 2016).
Rashid, M., Rasool, I., Zafar, N. A. & Afzaal, H. Formal verification of rewards and penalties mechanism of ffg attestations: Ethereum 2.0 beacon chain case study. IEEE Access (2025).
Afzaal, H., Zafar, N. A., Tehseen, A. & Kousar, S. Model checking of rewards and penalties in beacon chain. Int. J. Networked Distrib. Comput. 13, 7 (2025). (PMID: 10.1007/s44227-024-00050-z)
Afraz, N., Wilhelmi, F., Ahmadi, H. & Ruffini, M. Blockchain and smart contracts for telecommunications: Requirementsvs. cost analysis. IEEE Access (2023).
Iansiti, M. et al. The truth about blockchain. Harv. Bus. Rev. 95, 118–127 (2017).
Monrat, A. A., Schelén, O. & Andersson, K. A survey of blockchain from the perspectives of applications, challenges, and opportunities. IEEE Access 7, 117134–117151 (2019). (PMID: 10.1109/ACCESS.2019.2936094)
Saari, A., Vimpari, J. & Junnila, S. Blockchain in real estate: Recent developments and empirical applications. Land Use Policy 121, 106334 (2022). (PMID: 10.1016/j.landusepol.2022.106334)
Johnson, J. Is cardano a serious rival to ethereum? Available at SSRN 3886108 (2021).
Pierro, G. A. & Tonelli, R. Can solana be the solution to the blockchain scalability problem? In 2022 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER), 1219–1226 (IEEE, 2022).
Armknecht, F., Karame, G. O., Mandal, A., Youssef, F. & Zenner, E. Ripple: Overview and outlook. In Trust and Trustworthy Computing: 8th International Conference, TRUST 2015, Heraklion, Greece, August 24-26, 2015, Proceedings 8, 163–180 (Springer, 2015).
Lokhava, M. et al. Fast and secure global payments with stellar. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, 80–96 (2019).
Buterin, V. et al. Ethereum white paper. GitHub repository 1, 22–23 (2013).
Kim, C. Ethereum 2.0: How it works and why it matters. Coindesk: https://www.coindesk.com/wp-content/uploads/2020/07/ETH-2.0-072120. pdf (2020).
Tucci-Piergiovanni, S. Keynote: Blockchain consensus protocols, from bitcoin to ethereum 2.0. In 2022 IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events (PerCom Workshops), 1–1 (IEEE, 2022).
Neuder, M., Moroz, D. J., Rao, R. & Parkes, D. C. Low-cost attacks on ethereum 2.0 by sub-1/3 stakeholders. arXiv preprint arXiv:2102.02247 (2021).
Buterin, V. Ethereum: platform review. Opportunities and challenges for private and consortium blockchains 45, 1–45 (2016).
Buterin, V. et al. Combining ghost and casper. arXiv preprint arXiv:2003.03052 (2020).
Cassez, F., Fuller, J. & Asgaonkar, A. Formal verification of the ethereum 2.0 beacon chain. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 167–182 (Springer, 2022).
Rashid, M., Rasool, I., Zafar, N. A. & Afzaal, H. Formal modeling and verification of validator voluntarily exit in ethereum 2.0 beacon chain. In 2023 2nd International Conference on Emerging Trends in Electrical, Control, and Telecommunication Engineering (ETECTE), 1–6 (IEEE, 2023).
Clarke, E. M. & Wing, J. M. Formal methods: State of the art and future directions. ACM Comput. Surv. (CSUR) 28, 626–643 (1996). (PMID: 10.1145/242223.242257)
Baier, C. & Katoen, J.-P. Principles of model checking (MIT press, 2008).
Alturki, M., Bogdanas, D. et al. An Executable K Model of Ethereum 2 . 0 Beacon Chain Phase 0 Specification (2019).
Alturki, M. A. et al. Verifying gasper with dynamic validator sets in coq. Tech. Rep. (2020).
Afzaal, H., Imran, M. & Janjua, M. U. Formal verification of persistence and liveness in the trust-based blockchain crowdsourcing consensus protocol. Comput. Commun. 192, 384–401 (2022). (PMID: 10.1016/j.comcom.2022.06.014)
Rashid, M. et al. Formal verification and validation of iot-based railway gate controlling system at level crossing. In 2024 IEEE 1st Karachi Section Humanitarian Technology Conference (KHI-HTC), 1–6 (IEEE, 2024).
Rashid, M., Rasool, I., Zafar, N. A. & Afzaal, H. Formal modeling and verification of justification and finalization of checkpoints in ethereum 2.0 beacon chain. In 2024 IEEE 1st Karachi Section Humanitarian Technology Conference (KHI-HTC), 1–6 (IEEE, 2024).
Afzaal, H., Zafar, N. A., Tehseen, A., Kousar, S. & Imran, M. Formal verification of justification and finalization in beacon chain. IEEE Access 12, 55077–55102. https://doi.org/10.1109/ACCESS.2024.3389551 (2024). (PMID: 10.1109/ACCESS.2024.3389551)
Li, E., Serbănută, T., Diaconescu, D., Zamfir, V. & Rosu, G. Formalizing correct-by-construction casper in coq. In 2020 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 1–3 (IEEE, 2020).
Palmskog, K., Gligoric, M., Pena, L., Moore, B. & Roşu, G. Verification of casper in the coq proof assistant. Tech. Rep. (2018).
Losa, G. & Dodds, M. On the formal verification of the stellar consensus protocol. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) (Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2020).
Zheng, K., Liu, Y., Dai, C., Duan, Y. & Huang, X. Model checking pbft consensus mechanism in healthcare blockchain network. In 2018 9th International conference on information technology in medicine and education (ITME), 877–881 (IEEE, 2018).
Chand, S., Liu, Y. A. & Stoller, S. D. Formal verification of multi-paxos for distributed consensus. In International Symposium on Formal Methods, 119–136 (Springer, 2016).
Thin, W. Y. M. M., Dong, N., Bai, G. & Dong, J. S. Formal analysis of a proof-of-stake blockchain. In 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), 197–200 (IEEE, 2018).
Alturki, M. A. et al. Towards a verified model of the algorand consensus protocol in coq. In Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part I 3, 362–367 (Springer, 2020).
Tholoniat, P. & Gramoli, V. Formal verification of blockchain byzantine fault tolerance (2019). https://doi.org/10.48550/ARXIV (1909).
Braithwaite, S. et al. Formal specification and model checking of the tendermint blockchain synchronization protocol (short paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) (Schloss-Dagstuhl-Leibniz Zentrum für Informatik, 2020).
Woos, D. et al. Planning for change in a formal verification of the raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 154–165 (ACM, 2016).
Afzaal, H., Imran, M., Janjua, M. U. & Gochhayat, S. P. Formal modeling and verification of a blockchain-based crowdsourcing consensus protocol. IEEE Access 10, 8163–8183 (2022). (PMID: 10.1109/ACCESS.2022.3141982)
Afzaal, H., Imran, M. & Janjua, M. U. Formal verification of fraud-resilience in a crowdsourcing consensus protocol. Computers & Security 131, 103290 (2023). (PMID: 10.1016/j.cose.2023.103290)
Alturki, M. A. et al. Towards a verified model of the algorand consensus protocol in coq. In Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7–11, 2019, Revised Selected Papers, Part I 3, 362–367 (Springer, 2020).
Fedotov, I. & Khritankov, A. Statistical model checking of common attack scenarios on blockchain. arXiv preprint arXiv:2109.02803 (2021).
Yoo, J., Jung, Y., Shin, D., Bae, M. & Jee, E. Formal modeling and verification of a federated byzantine agreement algorithm for blockchain platforms. In 2019 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE), 11–21 (IEEE, 2019).
Zamfir, V. Casper the friendly ghost: A “correct-by-construction” blockchain consensus protocol. Ethereum Foundation (2017).
Chen, H., Pendleton, M., Njilla, L. & Xu, S. A survey on ethereum systems security: Vulnerabilities, attacks, and defenses. ACM Comput. Surv. (CSUR) 53, 1–43 (2020).
Westerkamp, M. & Diez, M. Verilay: A verifiable proof of stake chain relay. In 2022 IEEE International Conference on Blockchain and Cryptocurrency (ICBC), 1–9 (IEEE, 2022).
Liya, B. et al. Decentralized e-commerce platform implemented using smart contracts. In 2023 3rd International Conference on Smart Data Intelligence (ICSMDI), 23–27 (IEEE, 2023).
Ramos, D. & Zanko, G. Ethereum 2.0–a review of the causes and consequences of the upcoming update to ethereum’s mainnet. Mobileyourlife.Com (2022).
Jiang, Z. et al. Exploring smart contract recommendation: towards efficient blockchain development. IEEE Trans. Serv. Comput. 16, 1822–1832 (2022).
Muthe, K. B., Vemuru, T. S. T., Sharma, K. & Mohammad, N. S. Decentranet-an ethereum, proxy re-encryption and ipfs based decentralized internet. In 2020 11th International Conference on Computing, Communication and Networking Technologies (ICCCNT), 1–5 (IEEE, 2020).
Patel, S., Sahoo, A., Mohanta, B. K., Panda, S. S. & Jena, D. Dauth: A decentralized web authentication system using ethereum based blockchain. In 2019 international conference on vision towards emerging trends in communication and networking (ViTECoN), 1–5 (IEEE, 2019).
Villafiorita, A., Weldemariam, K. & Tiella, R. Development, formal verification, and evaluation of an e-voting system with vvpat. IEEE Trans. Inf. Forensics Secur. 4, 651–661 (2009). (PMID: 10.1109/TIFS.2009.2034903)
Barnat, J., Brim, L. & Havel, V. Ltl model checking of parallel programs with under-approximated tso memory model. In 2013 13th International Conference on Application of Concurrency to System Design, 51–59 (IEEE, 2013).
Kumar, N. S. & Kumar, G. S. Modeling and verification of timed automaton based hybrid systems using spin model checker. In 2016 IEEE Annual India Conference (INDICON), 1–8 (IEEE, 2016).
Rehman, A., Latif, S. & Zafar, N. A. Automata based railway gate control system at level crossing. In 2019 International Conference on Communication Technologies (ComTech), 30–35 (IEEE, 2019).
Iqbal, M., Zafar, N. A. & Alkhammash, E. H. Formally identifying covid-19 patients for providing medical services using drones. In 2021 International Conference of Women in Data Science at Taif University (WiDSTaif), 1–6 (IEEE, 2021).
Rashid, M. et al. Formal verification of aircraft departure procedure using spin model checker. In 2023 18th International Conference on Emerging Technologies (ICET), 165–170 (IEEE, 2023).
Rashid, M. et al. Verification of safety of aircraft arrival procedure using spin model checker. In 2023 International Conference on Frontiers of Information Technology (FIT), 262–267 (IEEE, 2023).
Rashid, M., Rasool, I., Zafar, N. A. & AlKhammash, E. Formal verification of blockchain and iot-based e-voting system using spin. In 2023 2nd International Conference on Emerging Trends in Electrical, Control, and Telecommunication Engineering (ETECTE), 1–6 (IEEE, 2023).
Rashid, M. et al. Formal modeling and verification of iot-based smart waste management system using spin. In 2023 17th International Conference on Open Source Systems and Technologies (ICOSST), 1–6 (IEEE, 2023).
Rashid, M. et al. Formal modeling and verification of iot-based smart transport system using spin model checker. In 2024 IEEE 1st Karachi Section Humanitarian Technology Conference (KHI-HTC), 1–6 (IEEE, 2024).
Cortier, V. et al. Machine-checked proofs of privacy for electronic voting protocols. In 2017 IEEE Symposium on Security and Privacy (SP), 993–1008 (IEEE, 2017).
Halder, R., Proença, J., Macedo, N. & Santos, A. Formal verification of ros-based robotic applications using timed-automata. In 2017 IEEE/ACM 5th International FME Workshop on Formal Methods in Software Engineering (FormaliSE), 44–50 (IEEE, 2017).
Alam, Q. et al. A cross tenant access control (ctac) model for cloud computing: Formal specification and verification. IEEE Trans. Inf. Forensics Secur. 12, 1259–1268 (2017). (PMID: 10.1109/TIFS.2016.2646639)
Alam, Q. et al. Formal verification of the xdauth protocol. IEEE Trans. Inf. Forensics Secur. 11, 1956–1969 (2016).
Khalil, U., Uddin, M., Alaidaros, H. & Akhunzada, A. Nfts for the unassailable authentication of iot devices in cyber-physical systems: An implementation study. In Conference on Creativity, Technology, and Sustainability, 87–95 (Springer Nature Singapore Singapore, 2024).
Akhunzada, A. et al. A formal framework for web service broker to compose qos measures. In 2015 SAI Intelligent Systems Conference (IntelliSys), 532–536 (IEEE, 2015).
Alam, M. et al. Formal modeling and verification of security controls for multimedia systems in the cloud. Multimed. Tools Appl. 76, 22845–22870 (2017). (PMID: 10.1007/s11042-017-4853-0)
Nazir, A. et al. A high-level domain-specific language for siem (design, development and formal verification). Clust. Comput. 20, 2423–2437 (2017). (PMID: 10.1007/s10586-017-0819-2)
Bibi, I., Akhunzada, A. & Kumar, N. Deep ai-powered cyber threat analysis in iiot. IEEE Internet Things J. 10, 7749–7760 (2022). (PMID: 10.1109/JIOT.2022.3229722)
Imran, M. et al. Research perspectives and challenges of blockchain for data-intensive and resource-constrained devices. IEEE Access 10, 38104–38122 (2022). (PMID: 10.1109/ACCESS.2022.3162096)
Akhunzada, A., Al-Shamayleh, A. S., Zeadally, S., Almogren, A. & Abu-Shareha, A. A. Design and performance of an ai-enabled threat intelligence framework for iot-enabled autonomous vehicles. Comput. Electr. Eng. 119, 109609 (2024). (PMID: 10.1016/j.compeleceng.2024.109609)
Woodcock, J., Larsen, P. G., Bicarregui, J. & Fitzgerald, J. Formal methods: Practice and experience. ACM Comput. Surv. (CSUR) 41, 1–36 (2009). (PMID: 10.1145/1592434.1592436)
Holzmann, G. J. The model checker spin. IEEE Trans. Softw. Eng. 23, 279–295 (1997). (PMID: 10.1109/32.588521)
Cavada, R. et al. The nuxmv symbolic model checker. In Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26, 334–342 (Springer, 2014).
Pakonen, A., Pang, C., Buzhinsky, I. & Vyatkin, V. User-friendly formal specification languages-conclusions drawn from industrial experience on model checking. In 2016 IEEE 21st International Conference on Emerging Technologies and Factory Automation (ETFA), 1–8 (IEEE, 2016).
Pang, C., Pakonen, A., Buzhinsky, I. & Vyatkin, V. A study on user-friendly formal specification languages for requirements formalization. In 2016 IEEE 14th International Conference on Industrial Informatics (INDIN), 676–682 (IEEE, 2016).
Rashid, M., Rasool, I., Zafar, N. A. & Afzaal, H. Formal verification of rewards and penalties mechanism of ffg attestations: Ethereum 2.0 beacon chain case study. IEEE Access (2025).
Afzaal, H., Zafar, N. A., Tehseen, A. & Kousar, S. Model checking of rewards and penalties in beacon chain. Int. J. Networked Distrib. Comput. 13, 7 (2025). (PMID: 10.1007/s44227-024-00050-z)
Grant Information:
FY22-0695 Ethereum Foundation
Contributed Indexing:
Keywords: Beacon Chain; Blockchain; Consensus layer of Ethereum; Epoch Processing; Model Checking; SPIN
Entry Date(s):
Date Created: 20251122 Latest Revision: 20251213
Update Code:
20251213
PubMed Central ID:
PMC12696112
DOI:
10.1038/s41598-025-27396-w
PMID:
41274908
Database:
MEDLINE
Weitere Informationen
In Consensus layer of Ethereum, the Beacon Chain is the main component that maintains details related to validator status, attestations, penalties, and rewards according to the behavior of validators. A large amount of Ethers (ETH, Ethereum cryptocurrency) of different validators are at stake in Consensus layer of Ethereum right now and any change in ETH value due to slashing or rewards is managed by the Beacon Chain. Beacon Chain is a safety-critical system and any error or bug in it can affect the complete network of Consensus layer of Ethereum. A single mistake can cause a huge loss of ETH on stake and problems such as invalid block insertion and security attacks. The reference implementation of Beacon Chain developed by the Ethereum Foundation gives a complete operational description of the Beacon Chain. In this work, we focus on the formal modeling and verification of reference implementation of the epoch processing of Beacon Chain to ensure that the Beacon Chain epoch mechanism is designed correctly and robustly and that there exists very little chance of any bug. To achieve this goal, we utilize model checking, the most effective technique based on formal methods that is used to ensure the correctness of safety-critical systems. In this work, formal modeling is done for the epoch processing operations of the Beacon Chain using Process Meta Language (PROMELA). For verification purposes, safety properties are defined for each epoch processing operation of the Beacon Chain, and we formalize these properties using Linear Temporal Logic (LTL). Formal models and LTL formulas are given as input to the model checker to check whether these formal models satisfy LTL formulas. The SPIN model checker is utilized for the formal verification of the Beacon Chain.
(© 2025. The Author(s).)
Declarations. Competing interests: The authors declare no competing interests.