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.
Smart contracts are programs stored on a blockchain ledger, thus being immutable after deployment, which makes assessment of their correctness before deployment vital. Extended finite state machines (EFSM) offer a structured framework for modeling complex systems, thus providing a systematic approach to scrutinize smart contract functionalities. This paper describes a methodology to automatically convert from the abstract syntax tree of a smart contract to an EFSM model. A smart contract implementing a casino is the specific use case, and verification of the EFSM model reveals it to be blocking. This blocking represents that a malicious player can lock the funds of the casino so that they can never be retrieved.
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 article 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, AC 4 , is proposed to represent the implementation of the method. Experiments show that AC 4 demonstrates an increase in the solved rate, showing a 36.7% 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.
As blockchains shift from energy-hungry Proof-of-Work to capital-intensive Proof-of-Stake, they trade electricity costs for a new vulnerability: the risk of a capital run that can destabilize consensus and security. We model investors who choose between staking their coin to earn rewards or exiting to cash out, potentially triggering mass withdrawals. These "staking runs" are more likely when protocols are weak, when failure would hit coin prices hard, or when staking rewards are low. Leverage worsens things: margin calls accelerate exits and amplify run dynamics. Longer lock-up periods slow the run but may not prevent it. Previous research shows that low rewards are good for protocol security. We show they also raise the risk of a run. A run on a major Proof-of-Stake chain---like Ethereum---could destabilize the entire crypto ecosystem, threatening DeFi platforms that depend on it.
The communities of blockchains and distributed ledgers have been stirred up by the introduction of zero-knowledge proofs (ZKPs). Originally designed to solve privacy issues, ZKPs have now evolved into an effective remedy for scalability concerns and are applied in Zcash (internet money like Bitcoin). To enable ZKPs, Rank-1 Constraint Systems (R1CS) offer a verifier for bi-linear equations. To accurately and efficiently represent R1CS, several language tools like Circom, Noir, and Snarky have been proposed to automate the compilation of advanced programs into R1CS. However, due to the flexible nature of R1CS representation, there can be significant differences in the compiled R1CS forms generated from circuit language programs with the same underlying semantics. To address this issue, this paper uses a data-flow-based R1CS paradigm algorithm, which produces a standardized format for different R1CS instances with identical semantics. By using the normalized R1CS format circuits, the complexity of circuits' verification can be reduced. In addition, this paper presents an R1CS normalization algorithm benchmark, and our experimental evaluation demonstrates the effectiveness and correctness of our methods.
In this paper, we propose a physical protocol to verify the first nonzero term of a sequence using a deck of cards. The protocol lets a prover show the value of the first nonzero term of a given sequence to a verifier without revealing which term it is. Our protocol uses $Θ(1)$ shuffles, which is asymptotically lower than that of an existing protocol of Fukusawa and Manabe which uses $Θ(n)$ shuffles, where $n$ is the length of the sequence. We also apply our protocol to construct zero-knowledge proof protocols for three well-known logic puzzles: ABC End View, Goishi Hiroi, and Toichika. These protocols enables a prover to physically show that he/she know solutions of the puzzles without revealing them.
Junrui Liu, Ian Kretz, Hanzhi Liu, Bryan E‐Xin Tan · 10 authors
Zero-knowledge (ZK) proof systems have emerged as a promising solution for building security-sensitive applications. However, bugs in ZK applications are extremely difficult to detect and can allow a malicious party to silently exploit the system without leaving any observable trace. This paper presents Coda, a novel statically-typed language for building zero-knowledge applications. Critically, Coda makes it possible to formally specify and statically check properties of a ZK application through a rich refinement type system. One of the key challenges in formally verifying ZK applications is that they require reasoning about polynomial equations over large prime fields that go beyond the capabilities of automated theorem provers. Coda mitigates this challenge by generating a set of Coq lemmas that can be proven in an interactive manner with the help of a tactic library. We have used Coda to re-implement 77 arithmetic circuits from widely-used Circom libraries and applications. Our evaluation shows that Coda makes it possible to specify important and formally verify correctness properties of these circuits. Our evaluation also revealed 6 previously-unknown vulnerabilities in the original Circom projects.
As zero-knowledge proofs gain increasing adoption, the cryptography community has designed domain-specific languages (DSLs) that facilitate the construction of zero-knowledge proofs (ZKPs). Many of these DSLs, such as Circom, facilitate the construction of arithmetic circuits, which are essentially polynomial equations over a finite field. In particular, given a program in a zero-knowledge proof DSL, the compiler automatically produces the corresponding arithmetic circuit. However, a common and serious problem is that the generated circuit may be underconstrained, either due to a bug in the program or a bug in the compiler itself. Underconstrained circuits admit multiple witnesses for a given input, so a malicious party can generate bogus witnesses, thereby causing the verifier to accept a proof that it should not. Because of the increasing prevalence of such arithmetic circuits in blockchain applications, several million dollars worth of cryptocurrency have been stolen due to underconstrained arithmetic circuits. Motivated by this problem, we propose a new technique for finding ZKP bugs caused by underconstrained polynomial equations over finite fields. Our method performs semantic reasoning over the finite field equations generated by the compiler to prove whether or not each signal is uniquely determined by the input. Our proposed approach combines SMT solving with lightweight uniqueness inference to effectively reason about underconstrained circuits. We have implemented our proposed approach in a tool called QED 2 and evaluate it on 163 Circom circuits. Our evaluation shows that QED 2 can successfully solve 70% of these benchmarks, meaning that it either verifies the uniqueness of the output signals or finds a pair of witnesses that demonstrate non-uniqueness of the circuit. Furthermore, QED 2 has found 8 previously unknown vulnerabilities in widely-used circuits.
This paper introduces an abstract blockchain model that employs the Burn-to-Claim cross-blockchain protocol [1]. This multi-level simulator models a virtual environment of nodes running on the Ethereum Virtual Machine (EVM). Developed using the $$CSP\#$$ language [2], it has undergone formal verification with the model checker PAT. Focusing on inter-network operations, our model ( https://github.com/b-pillai/Burn-to-Claim-formal-verification ) examines the properties of correctness, security, and atomicity using PAT. Surprisingly, atomicity, assumed to be inherent in the time-lock mechanism of the Burn-to-Claim protocol, does not always hold. We establish its validity under specific assumptions while confirming the protocol’s correctness and security under the added assumptions.
Alex Ozdemir, Gereon Kremer, Cesare Tinelli, Clark Barrett
Abstract We study satisfiability modulo the theory of finite fields and give a decision procedure for this theory. We implement our procedure for prime fields inside the cvc5 SMT solver. Using this theory, we construct SMT queries that encode translation validation for various zero knowledge proof compilers applied to Boolean computations. We evaluate our procedure on these benchmarks. Our experiments show that our implementation is superior to previous approaches (which encode field arithmetic using integers or bit-vectors).
Due to the popularity of smart contracts in the modern financial ecosystem, there has been growing interest in formally verifying their correctness and security properties. Most existing techniques in this space focus on common vulnerabilities like arithmetic overflows and perform verification by leveraging contract invariants (i.e., logical formulas hold at transaction boundaries). In this paper, we propose a new technique, based on deep reinforcement learning, for automatically learning contract invariants that are useful for proving arithmetic safety. Our method incorporates an off-line training phase in which the verifier uses its own verification attempts to learn a policy for contract invariant generation. This learned (neural) policy is then used at verification time to predict likely invariants that are also useful for proving arithmetic safety. We implemented this idea in a tool called Cider and incorporated it into an existing verifier (based on refinement type checking) for proving arithmetic safety. Our evaluation shows that Cider improves both the quality of the inferred invariants as well as inference time, leading to faster verification and hardened contracts with fewer run-time assertions.
Norine Coenen, Bernd Finkbeiner, Jana Hofmann, Julia Tillman
Smart contracts are small but highly security-critical programs that implement wallets, token systems, auctions, crowd funding systems, elections, and other multi-party transactions on the blockchain. A broad range of methods has been developed to ensure that a smart contract is functionally correct. However, smart contracts often additionally need to satisfy certain hyperproperties, such as symmetry, determinism, or an information flow policy. In this paper, we show how a synthesis method for smart contracts can ensure that the contract satisfies its desired hyperproperties. We build on top of a recently developed synthesis approach from specifications in the temporal logic TSL. We present HyperTSL, an extension of TSL for the specification of hyperproperties of infinite-state software. As a preprocessing step, we show how to detect if a hyperproperty has an equivalent formulation as a (simpler) trace property. Finally, we describe how to refine a synthesized contract to adhere to its HyperTSL specification.
The formal description and verification of networks of cooperative and interacting agents is made difficult by the interplay of several different behavioral patterns, models of communication, scalability issues. In this paper, we will explore the functionalities and the expressiveness of a general-purpose process algebraic framework for the specification and model checking based analysis of collective and cooperative systems. The proposed syntactic and semantic schemes are general enough to be adapted with small modifications to heterogeneous application domains, like, e.g., crowdsourcing systems, trustworthy networks, and distributed ledger technologies.
Les preuves vérifiables de manière probabiliste (PCP, de l'anglais "probabilistically checkable proofs), les preuves interactives (IP, pour "interactive proofs") ou encore les preuves à divulgation nulle de connaissance ("zero-knowledge proofs") ont la particularité d'admettre une vérification probabilististe. Ces systèmes de preuves probabilistes interviennent dans les constructions de schémas de calcul vérifiable, des protocoles cryptographiques permettant de vérifier très rapidement qu'un long calcul a été correctement effectué. En 2016, un nouveau modèle de preuve a été introduit par Ben-Sasson, Chiesa et Spooner : celui des preuves interactives par oracle (IOP, pour "interactive oracle proofs"). Ce modèle généralise à la fois les PCPs et les IPs et a suscité beaucoup d'intérêt depuis son introduction. Le modèle IOP a mené à d'intéressants résultats théoriques sur les arguments non-interactifs succincts et transparents ainsi qu'à des déploiements industriels.Un problème récurrent dans les constructions de systèmes de preuves probabilistes est celui de tester efficacement la proximité à un code correcteur d'erreurs. Le but est de déterminer si un certain mot appartient à un code linéaire donné, ou bien s'il est éloigné de tout mot de ce code. Les tests de proximité à des codes polynomiaux peuvent être interprétés comme des tests de bas degré. Par exemple, un important sous-protocole utilisé dans de nombreuses constructions pratiques est un "IOP of Proximity" pour les codes de Reed-Solomon (Ben-Sasson et al., ICALP 2018).Dans cette thèse, nous proposons dans le modèle IOP des protocoles permettant de vérifier la proximité à des codes correcteur d'erreurs.En nous inspirant du test de proximité pour les codes de Reed-Solomon de Ben-Sasson et al., nous commençons par formuler un cadre abstrait et générique pour construire des "IOPs of Proximity" pour des codes linéaires et en analysons formellement les propriétés. Nous appliquons ensuite cette méthodologie à différentes familles de codes généralisant les codes de Reed-Solomon. Il s'agit d'une part de codes définis à partir d'évaluations de polynômes multivariés et, d'autre part, de codes de géométrie algrébrique définis sur des courbes. Nos protocoles permettent de tester la proximité à des codes présentant des propriétés attrayantes par rapport aux codes de Reed-Solomon (telles que des alphabets de petite taille), tout en ayant une efficacité similaire à la construction de Ben-Sasson et al.
Kunjian Song, Nedas Matulevicius, Eddie B. de Lima Filho, Lucas C. Cordeiro
Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0.
Bernd Finkbeiner, Jana Hofmann, Florian Kohn, Noemi Passing
Smart contracts are small but highly error-prone programs that implement agreements between multiple parties. We present a reactive synthesis approach for the automatic construction of smart contract state machines. Towards this end, we extend temporal stream logic (TSL) with universally quantified parameters over infinite domains. Parameterized TSL is a convenient logic to specify the temporal control flow, i.e., the correct order of transactions, as well as the data flow of the contract's fields. We develop a two-step approach that 1) synthesizes a finite representation of the - in general - infinite-state system and 2) splits the system into a compact hierarchical architecture that enables the implementation of the state machine in Solidity. We implement the approach in our prototype tool SCSynt, which - within seconds - automatically constructs Solidity code that realizes the specified control flow.
Transactions involving multiple blockchains are implemented by cross-chain protocols. These protocols are based on smart contracts, programs that run on blockchains, executed by a network of computers. Because smart contracts can automatically transfer ownership of cryptocurrencies, electronic securities, and other valuable assets among untrusting parties, verifying the runtime correctness of smart contracts is a problem of compelling practical interest. Such verification is challenging since smart contract execution is time-sensitive, and the clocks on different blockchains may not be perfectly synchronized. This paper describes a method for runtime monitoring of blockchain executions. First, we propose a generalized runtime verification technique for verifying partially synchronous distributed computations for the metric temporal logic (MTL) by exploiting bounded-skew clock synchronization. Second, we introduce a progression-based formula rewriting scheme for monitoring \MTL specifications which employ SMT solving techniques and report experimental results.