Ensuring the authenticity and integrity of products in a supply chain while maintaining privacy is a significant challenge. Traditional blockchain-based verification systems often expose sensitive information, such as location, batch ID, and manufacturer identity. To address this, we propose a zk-Rollup-based privacy-preserving identity and transaction verification system that leverages Zero-Knowledge Proofs (ZKPs) to ensure trust without revealing confidential data. Our architecture includes a producer and a manufacturer, where the producer generates verifiable proofs of product origin, and the manufacturer appends metadata such as manufacturing date and expiry. A centralized server aggregates producer and manufacturer data, generating zk-SNARK proofs for each transaction. The system employs zk-Rollups for efficient transaction batching, significantly reducing on-chain gas fees and improving scalability. Additionally, all data is end-to-end encrypted using SHA-256, ensuring robust security. Users and third parties can verify proof validity using a QR code-based authentication mechanism, which queries the server endpoint without exposing private details. Performance evaluations demonstrate significant improvements in proof generation time, verification latency, and cost efficiency. Our proposed solution enables secure and scalable supply chain verification, preserving privacy while maintaining transparency and trust. The results indicate that zk-Rollups reduce gas fees by a factor of 10x, making the system feasible for real-world applications. Future work will focus on further optimizing proof generation and exploring decentralized identity solutions for enhanced security.
Abstract This paper introduces semi-competitive differential game logic $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , which enables verification of safety-critical applications that involve interactions between two agents. In $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , these interactions are specified as games on hybrid systems with two players that may collaborate with each other when helpful and may compete when necessary. The players in the hybrid games of $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> have individual goals that may overlap, leading to nonzero-sum games. This makes $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> especially well-suited for verifying situations where players, e.g., share safety objectives but otherwise pursue different goals, so that zero-sum assumptions lead to overly conservative results. Additionally, $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> solves the subtlety that even though each player may benefit from knowledge of the other player’s goals, e.g., concerning shared safety objectives, unsafe situations might still occur if every player were to mutually assume the other player would act to avoid unsafety. The syntax and semantics, as well as a sound and relatively complete proof calculus are presented for $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> . The relationship between $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> and zero-sum differential game logic $$\textsf {dG}\mathcal {L}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:mi>L</mml:mi> </mml:mrow> </mml:math> is discussed and the purpose of $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> illustrated in a canonical example.
Zero Knowledge (ZK) proofs are protocols with growing applications in fields such as cryptography. They can be particularly difficult to design and thus have multiple domain-specific languages (DSLs) to aid a programmer in their construction. Analysis methods for these protocols are then typically language-specific, greatly limiting their utility. Most languages compile user code into a midpoint polynomial-circuit called a rank one constraint system (R1CS). We provide tools to analyse these R1CS circuits which hence have much broader applicability than existing tools. Specifically, we design and implement a tool for equivalence up to renaming and scaling, useful to avoid repeating a laborious step of the ZK process. As implemented, the tool can handle circuits on the order of millions of constraints. Additionally, we provide methods to extract a directed acyclic hierarchical structure via clustering to guide an automated property prover with recursive proving. Such a structure typically exists in DSL code but is lost when compiled to R1CS and is required to make larger circuits feasible to pass to a property prover. The guidance given by our clustering methods to the property prover Civer gave comparable results to the guidance of the original structure present in the code and finished in faster time.
Igor Konnov, Jure Kukovec, Thomas Pani, Roberto Saltini · 5 authors
We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique challenges it poses for formal verification. Our primary tools are TLA+ for specification and the Apalache model checker for verification. Our formalization builds on the executable Python specification of 3SF. To begin, we manually translate this specification into TLA+, revealing significant combinatorial complexity in the definition of Accountable Safety. To address these challenges, we introduce several layers of manual abstraction: (1) replacing recursion with folds, (2) substituting abstract graphs with integers, and (3) decomposing chain configurations. To cross-validate our results, we develop alternative encodings in SMT (CVC5) and Alloy. Despite the inherent complexity, our results demonstrate that exhaustive verification of Accountable Safety is feasible for small instances - supporting up to 7 checkpoints and 24 validator votes. Moreover, no violations of Accountable Safety are observed, even in slightly larger configurations. Beyond these findings, our study highlights the importance of manual abstraction and domain expertise in enhancing model-checking efficiency and showcases the flexibility of TLA+ for managing intricate specifications.
Computer programs control vital infrastructure, safeguard national security, and process all financialtransactions, making their correctness and security paramount. Formal verification is a key tool for program trust and assurance. However, as the complexity of computer systems grows, the complexity of their properties does as well. While traditional verification has focused on proving safety, the same techniques do not extend to other properties of interest, such as liveness, correct execution, and cryptographic properties, like zero-knowledge security. While these properties are valuable in cloud computing, where execution is outsourced to untrusted third-party providers, they remain understudied. This dissertation presents new languages, proof systems, and techniques targeting the verifica-tion of programs and their executions. Domain-specific languages (DSLs) are key in this effort. By restricting program syntax to a mathematically well-understood subset, we prove important proper- ties. This dissertation introduces four new languages and proof systems: Ticl, a structural temporal logic for modularly proving complex liveness specifications for infinite, nondeterministic programs; Reef, a system for verifiable regular expression matching that keeps matched text confidential; Otti, a framework for proving correct execution of optimization problems like machine learning training; and Zippel, a language for implementing and automatically verifying properties of non-interactive zero-knowledge protocols. Each one of those works shows that, by carefully designing languages and proof systems for specificdomains, we can have both expressive languages, and practical verification of complex properties which were previously difficult, or impossible to prove. We demonstrate this through case studies in distributed systems, secure computation, and cryptographic protocols.
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa · 7 authors
Abstract This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for existing solvers due to their inability to exploit multimodular structure. To address this issue, our method partitions constraints by modulus and uses lifting and lowering techniques to share information across subsystems, supported by algebraic tools like weighted Gr bner bases. Our experiments show that the proposed method outperforms existing state-of-the-art solvers in verifying cryptographic implementations related to Montgomery arithmetic and zero-knowledge proofs.
Muhammad Rashid, Imran Rasool, Nazir Ahmad Zafar, Hamra Afzaal
Ethereum 2.0 stands out as a progressive decentralized blockchain platform, drawing attention for its security, scalability, and flexibility. Central to Ethereum 2.0 is the Beacon Chain, serving as the cornerstone managing validator rewards, penalties, attestations, and slashing mechanisms. Rewards and Penalties Mechanism (RPM) is of particular importance within the Beacon Chain as it includes validator balances based on their attestation behavior. Despite the critical role of RPM in maintaining the reliability and security of the Beacon Chain, the absence of formal verification work employing model checking is notable. Therefore, this research endeavors to fill this gap by employing formal verification technique to assess the RPM’s behavior concerning Friendly Finality Gadget (FFG) attestations. Utilizing Process Meta Language (PROMELA), a formal model of the RPM is specified, encompassing safety and liveness properties crucial for its robust functioning. The properties, including invalid attestation, integrity, fairness, availability, failure to attest, and inactivity imposition, are formalized through Linear Temporal Logic (LTL). Subsequently, the formal model alongside the specified properties is subjected to verification using the SPIN model checker. The properties are analyzed with respect to verification time, states visited, and memory usage. The outcome of this research contributes to a rigorous analysis of the RPM’s behavior. This work not only enhances an understanding of Beacon Chain’s operational dynamics but also underscores the importance of formal verification in ensuring the reliability and security of blockchain protocols.
Abstract Circuit languages like Circom and Gnark have become essential tools for programmable zero-knowledge cryptography, allowing developers to build privacy-preserving applications. These domain-specific languages (DSLs) encode both the computation to be verified (as a witness generator ) and the corresponding arithmetic circuits , from which the prover and verifier can be automatically generated. However, for these programs to be correct, the witness generator and the arithmetic circuit need to be mutually consistent in a certain technical sense, and inconsistencies can result in security vulnerabilities. This paper formalizes the consistency requirement for circuit DSLs and proposes the first automated technique for verifying it. We evaluate the method on hundreds of real-world circuits, demonstrating its utility for both automated verification and uncovering errors that existing tools are unable to detect.
Weihan Li, Zongyang Zhang, Yanpei Guo, Sherman S. M. Chow · 5 authors
Zero-knowledge range proof (ZKRP) asserts that a committed integerVlies in a given range like$[{0, 2^{n}-1}]$without other leakages ofV. It is vital in various privacy-preserving systems. Moving forward, the quest for post-quantum security is still in its infancy; the proof size of state-of-the-art lattice-based ZKRP (Lyubashevsky et al., CCS 20 and Couteau et al., Eurocrypt 21) remains linear inn, directly impacting the long-term sustainability in applications such as immutable ledgers. Confronting this unresolved impasse, we propose SHARP-PQ,i.e., succinct hash-based arbitrary-range proof with post-quantum security. SHARP-PQ offers proof size poly-logarithmic ton, optimized batch proofs, and versatile (new) capabilities. Its success stems from the improved inner product argument and exploitation of homomorphism. Empirically, SHARP-PQ features at least$10\times $smaller proof size for multiple ranges over lattice-based ZKRPs while maintaining competitive prover and verifier times. SHARP-PQ also outperforms ZKRPs directly constructed from hash-based generic zero-knowledge proofs at most$10 \times $.
(English) The advent of the internet, marked by pivotal developments such as the launch of Arpanet and the standardization of HTTP, has irrevocably changed the fabric of modern society. Centralized platforms like Microsoft, Google, Apple, and Amazon have dominated this digital landscape, offering many services ranging from cloud computing to online storage. However, the centralized nature of these services has raised significant concerns regarding user privacy, data integrity, and the potential for censorship. In response to these issues, the open-source community has explored peer-to-peer alternatives, notably in the realm of distributed file systems, ledgers, and blockchain technology. Blockchains, popularized by the emergence of Bitcoin, promote a democratized service model that challenges the centralized status quo. Yet, they are not without their own challenges, including decentralization, security, privacy, and performance. This thesis delves into the nuances of blockchain technology, focusing on Ethereum's transition from Proof of Work (PoW) to Proof of Stake (PoS) and its implications on network hardware requirements, topology, and overall performance. The development of Ethereum serves as a small-scale reflection of the broader ambitions and challenges in transitioning to Decentralized Finance (DeFi) platforms. Despite significant theoretical advancements in consensus mechanisms and scalability solutions, real-world implementations and experimental validations remain sparse. This work aims to bridge this gap by comprehensively analysing Ethereum's PoS transition by examining the interlaced relationships between software logic, hardware configurations, and network dynamics. Through novel measurement models and tools, this thesis contributes to a deeper understanding of how Ethereum's architectural changes impact its ecosystem and its participants' behaviours. Lastly, the research presented in this thesis illustrates the technical and operational challenges facing Ethereum and similar blockchain platforms and proposes a series of contributions that advance the field. This work empirically analyses the future enhancements in blockchain technology by exploring the implications of the network and its topology, to the viability of decentralized validation processes, and the potential for scaling solutions like Data Availability Sampling. The open-source tools and methodologies developed within the thesis scope represent the commitment to transparency and collaboration, which follows the spirit of the decentralized communities it seeks to serve. Through a mix of theoretical exploration and empirical research, this thesis aims to provide a deeper and more detailed understanding of Ethereum PoS' design choices, its capabilities and the limitations this one represents in future steps and upgrades, leading the way for more resilient, scalable, and decentralized digital infrastructures. (Català) L'arribada d'Internet, marcada per avenços fonamentals com el llançament d'Arpanet i l'estandardització de HTTP, ha canviat irrevocablement el teixit de la societat moderna. Les plataformes centralitzades com Microsoft, Google, Apple i Amazon han dominat aquest panorama digital, oferint serveis que van des de la computació al núvol fins a l'emmagatzematge en línia. No obstant això, la naturalesa centralitzada d'aquests serveis ha generat importants preocupacions pel que fa a la privacitat de l'usuari, la integritat de les dades i la possibilitat de censura. En resposta a aquests problemes, la comunitat de codi obert ha explorat alternatives d'igual a igual, especialment en l'àmbit dels sistemes d'arxius distribuïts i la tecnologia blockchain. Les blockchains, popularitzades pel sorgiment de Bitcoin, han proposat fins i tot un model de servei democratitzat que desafia l'statu quo centralitzat. No obstant això, no estan exemptes de desafiaments, incloent la descentralització, la seguretat, la privacitat i el rendiment. Aquesta tesi aprofundeix en les dinàmiques de la tecnologia blockchain, centrant-se en la transició d'Ethereum de Proof of Work (PoW) a Proof of Stake (PoS) i les seves implicacions en els requisits, la topologia de la xarxa i el rendiment general del maquinari. El desenvolupament d'Ethereum serveix com un reflex a petita escala de les ambicions i els desafiaments més amplis en la transició a plataformes de finances descentralitzades (DeFi). Malgrat els importants avenços teòrics en els mecanismes de consens i les solucions d'escalabilitat, les implementacions al món real i les validacions experimentals segueixen sent escasses. Aquesta tesi té com a objectiu tancar aquesta bretxa analitzant exhaustivament la transició PoS d'Ethereum mitjançant l'examen de les relacions entrellaçades entre la lògica del programari, les configuracions de maquinari i la dinàmica de la xarxa. A través de nous models i eines de mesura, aquesta tesi contribueix a una comprensió més profunda de com els canvis arquitectònics d'Ethereum impacten en el seu ecosistema i els comportaments dels seus participants. Per últim, la investigació presentada en aquesta tesi il·lustra els desafiaments tècnics i operatius que enfronten Ethereum i plataformes blockchain similars, i proposa una sèrie de contribucions que esperem serveixin per fer avançar el mon de les blockchains. La tesi analitza empíricament les millores futures en la tecnologia blockchain explorant les implicacions de la xarxa i la seva topologia, la viabilitat dels processos de validació descentralitzats i el potencial per escalar solucions com el mostreig de disponibilitat de dades. Les eines i metodologies de codi obert desenvolupades dins de l'abast de la tesi representen el compromís amb la transparència i la col·laboració, que segueix l'esperit de les comunitats descentralitzades a les que busquem servir. A través d'una combinació d'exploració teòrica i investigació empírica, aquesta tesi té com a objectiu proporcionar una comprensió més profunda i detallada de les opcions de disseny d'Ethereum PoS, les seves capacitats i les limitacions que això representa en futurs passos i actualitzacions, obrint el camí cap a una solució més resilient i escalable per a infraestructures digitals descentralitzades. (Español) La llegada de Internet, marcada por avances fundamentales como el lanzamiento de Arpanet y la estandarización de HTTP, ha cambiado irrevocablemente el tejido de la sociedad moderna. Plataformas centralizadas como Microsoft, Google, Apple y Amazon han dominado este panorama digital, ofreciendo servicios que van desde computación en la nube hasta almacenamiento en línea. Sin embargo, la naturaleza centralizada de estos servicios ha generado importantes preocupaciones con respecto a la privacidad del usuario, la integridad de los datos y la posibilidad de censura. En respuesta a estos problemas, la comunidad de código abierto ha explorado alternativas de igual a igual, especialmente en el ámbito de los sistemas de archivos distribuidos, los libros de contabilidad y la tecnología blockchain. Las blockchains, popularizadas por el surgimiento de Bitcoin, promueven un modelo de servicio democratizado que desafía el status quo centralizado. Sin embargo, no están exentos de desafíos, incluida la descentralización, la seguridad, la privacidad y el rendimiento. Esta tesis profundiza en los matices de la tecnología blockchain, centrándose en la transición de Ethereum de Proof of Work (PoW) a Proof of Stake (PoS) y sus implicaciones en los requisitos, la topología de la red y el rendimiento general del hardware. El desarrollo de Ethereum sirve como un reflejo a pequeña escala de las ambiciones y desafíos más amplios en la transición a plataformas de finanzas descentralizadas (DeFi). A pesar de los importantes avances teóricos en los mecanismos de consenso y las soluciones de escalabilidad, las implementaciones en el mundo real y las validaciones experimentales siguen siendo escasas. Esta tesis tiene como objetivo cerrar esta brecha analizando exhaustivamente la transición PoS de Ethereum mediante el examen de las relaciones entrelazadas entre la lógica del software, las configuraciones de hardware y la dinámica de la red. A través de novedosos modelos y herramientas de medición, esta tesis contribuye a una comprensión más profunda de cómo los cambios arquitectónicos de Ethereum impactan su ecosistema y los comportamientos de sus participantes. Por último, la investigación presentada en esta tesis ilustra los desafíos técnicos y operativos que enfrentan Ethereum y plataformas blockchain similares y propone una serie de contribuciones que hacen avanzar el campo. La tesis analiza empíricamente las mejoras futuras en la tecnología blockchain explorando las implicaciones de la red y su topología, la viabilidad de los procesos de validación descentralizados y el potencial para escalar soluciones como el muestreo de disponibilidad de datos. Las herramientas y metodologías de código abierto desarrolladas dentro del alcance de la tesis representan el compromiso con la transparencia y la colaboración, que sigue el espíritu de las comunidades descentralizadas a las que busca servir. A través de una combinación de exploración teórica e investigación empírica, esta tesis tiene como objetivo proporcionar una comprensión más profunda y detallada de las opciones de diseño de Ethereum PoS, sus capacidades y las limitaciones que esto representa en futuros pasos y actualizaciones, abriendo el camino hacia una solución más resiliente y escalable. e infraestructuras digitales descentralizadas.
Zeiger is a pencil puzzle consisting of a rectangular grid, with each cell having an arrow pointing in horizontal or vertical direction. Some cells also contain a positive integer. The objective of this puzzle is to fill a positive integer into every unnumbered cell such that the integer in each cell is equal to the number of different integers in all cells along the direction an arrow in that cell points to. In this paper, we prove that deciding solvability of a given Zeiger puzzle is NP-complete via a reduction from the not-all-equal positive 3SAT (NAE3SAT+) problem. We also construct a card-based physical zero-knowledge proof protocol for Zeiger, which enables a prover to physically show a verifier the existence of the puzzle's solution without revealing it.
Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho, Youcheng Sun · 5 authors
This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification.
Alexandr Kuznetsov, Alex Rusnak, Anton Yezhov, Dzianis Kanonik · 6 authors
Zero-knowledge proofs have emerged as a powerful tool for enhancing privacy and security in blockchain applications. However, the efficiency and scalability of proof systems remain a significant challenge, particularly in the context of Merkle tree inclusion proofs. Traditional proof aggregation techniques based on AND logic suffer from a high verification complexity and data communication overhead, limiting their practicality for large-scale applications. In this paper, we propose a novel proof aggregation approach based on OR logic, which enables the generation of compact and universally verifiable proofs for Merkle tree inclusion. By adapting and extending the concept of OR composition from Sigma protocols, we achieve a proof size that is independent of the number of leaves in the tree, and verification can be performed using any single valid leaf hash. This represents a significant improvement over AND aggregation, which requires the verifier to process all leaf hashes. We formally define the OR aggregation logic; describe the process of generating universal proofs; and provide a comparative analysis that demonstrates the advantages of our approach in terms of proof size, verification data, and universality. Furthermore, we discuss the potential of combining OR and AND aggregation logics to create complex acceptance functions, enabling the development of expressive and efficient proof systems for various blockchain applications. The proposed techniques have the potential to significantly enhance the scalability, efficiency, and flexibility of zero-knowledge proof systems, paving the way for more practical and adaptive solutions in large-scale blockchain ecosystems.
Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This paper introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system. The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC4, is proposed to represent the implementation of the method. Experiments show that AC4 demonstrates a increase in the solved rate, showing a 29% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.
Ethereum has recently switched to a Proof of Stake consensus protocol called Gasper. We analyze Gasper using PRISM+ , an extension of the probabilistic model checker PRISM with primitives for modeling blockchain data types . PRISM+ is therefore used to rapidly and automatically analyze the robustness of Gasper when tuning, up or down, several basic parameters of the protocol, such as network latencies and number of validators. We also study the effectiveness of Gasper in updating stakes and its resilience to three attacks: the balance, bouncing and time attacks.
Muhammad Ikram Mohd Rashid, Imran Rasool, Nazir Ahmad Zafar, Hamra Afzaal
New to the Ethereum platform with version 2.0 is the Beacon chain. Validator status, attestation information, and many more are maintained via the proof-of-stake (PoS) consensus protocol, which is relied upon. The Ethereum 2.0 beacon chain relies on the validation and completion of checkpoints to validate and finish all the blocks associated with those checkpoints. By formally verifying it using the SPIN model checker, this research tackles the issue of the dependability and security of the Beacon Chain’s justification and finalization operations. Due of its novelty (launched in 2020), there is little any literature on the subject. Additionally, no previous study has formally verified the beacon chain using the SPIN model checker. The study makes use of PROMELA, a formal specification language, to formally outline the reasoning and finalization method of the Ethereum 2.0 Beacon Chain. Utilizing the SPIN Model Checker, a program graph is generated for this procedure, which formulaically expresses safety features via the use of linear temporal logic (LTL). To make sure everything is in order, we run the SPIN model checker with the program graph and LTL formulae as inputs to see whether the program graph satisfies the properties. This is the formal verification process.