Lakshmi Padmaja Maddali, Meena Singh Dilip Thakur, R. Vigneswaran, M A Rajan · 6 authors
Many enterprise (permissioned) blockchain applications demand low latency to commit their transactions on the ledger. One way to reduce latency is by reducing the number of peers required to execute/endorse a transaction in a secure and consistent way. However, by reducing the number of endorsements, blockchain network can be vulnerable to attacks such as collusion. In this paper, we introduce a novel scheme VeriBlock to overcome this problem. Our idea is to reduce the redundant execution of smart contracts without compromising on the security of the blockchain system by leveraging Verifiable Computing (VC) (which provides mathematically verifiable proof of execution) and Trusted Execution Environment (TEE) (which provides an attestation of the code executed) approaches. We also implemented these approaches to derive insights. In the proposed scheme, few nodes execute the smart contact logic and all the other nodes verify it. We propose two different models in the proposed scheme, 1. Endorser-Verify model, where the verification is done as part of transaction endorsement, and 2. Committer- Verify model, where the verification is done at the time of transaction commit. We have built Endorser-Verify model using Hyperledger Fabric blockchain platform, Pinocchio and Intel SGX as VC and TEE respectively and performance of the proposed scheme is analyzed by running bidding use case. Based on the results, we observe that the running time for VC based technique is in the order of magnitude two when compared with the naive implementation. On the other hand the performance of SGX is better than VC based approach.
We try to verify properties of the Bitcoin-S library, a Scala implementation of parts of the Bitcoin protocol. We use the Stainless verifier which supports programs in a fragment of Scala called Pure Scala. Since Bitcoin-S is not written in this fragment, we extract the relevant code from it and rewrite it until we arrive at code that we successfully verify. In that process we find and fix two bugs in Bitcoin-S.
Blaž Podgorelec, Marjan Herieko, Muhamed Turkanović
Currently, developers and researchers are dedicated to finding better ways to achieve greater scalability of various blockchain platforms. Focused on the Ethereum blockchain platform, the state channels are currently the only maturely researched and implemented a solution for achieving scalability. However, there are still several problems, such as transparency of state channel networks, transaction traceability, and the incapability that the off-chain state is transferred back on the blockchain network in an ad-hoc manner. To solve the aforementioned problems, we propose a novel state channel solution in the form of a State Channel as a Service, which, although off-chain, still incorporates a secure distributed and decentralized network. This solves the challenge of transparency and traceability while giving users the confidence that only the valid last off-chain state is transferred back on the blockchain network. With the proposed solution, there is no need for users to monitor state channel activities for possible malicious actions. Implementation was performed in the form of a payment channel system, presenting a potential use case for the SCaaS. Furthermore, we performed a security and performance analysis, which shows that the solution is secure and by a factor of 12 more efficient than the classical on-chain payment systems. To evaluate and prove the contributions of the proposed solution, quantitative, and qualitative comparisons with selected related works (i.e., Raiden and Celer) were also performed.
Traditional centralized access control has some shortcomings in robustness, trustworthiness and circulation. Blockchains have the advantages of fault tolerance and trust. Smart contracts have the characteristics of automatic execution and flexible expansion. Tokens can well record credential information and transfer easily. In this paper, blockchain, smart contract and token are integrated and applied to access control to solve the shortcomings of traditional access control. First, access control, blockchain, smart contract and token are briefly described. Second, this paper proposes a solution by giving the general data structure of access control token, elaborating the equivalence, split, merge and verification algorithms of access control token, and explaining the system architecture of token-based access control. Last, this paper uses a token-based access control simulation system to verify that token-based access control has certain comparative advantages in robustness, trustworthiness, circulation, concurrency and so on.
Randomness is typically thought to be essential for zero knowledge protocols. Following this intuition, Goldreich and Oren (Journal of Cryptology 94) proved that auxiliary-input zero knowledge cannot be achieved with a deterministic prover. On the other hand, positive results are only known in the honest-verifier setting, or when the prover is given at least a restricted source of entropy. We prove that removing (or just bounding) the verifier’s auxiliary input, deterministic-prover zero knowledge becomes feasible:
Assuming non-interactive witness-indistinguishable proofs and subexponential indistinguishability obfuscation and one-way functions, we construct deterministic-prover zero-knowledge arguments for Open image in new window against verifiers with bounded non-uniform auxiliary input.
Assuming also keyless hash functions that are collision-resistant against bounded-auxiliary-input quasipolynomial-time attackers, we construct similar arguments for all of Open image in new window .
Cryptocurrencies are more than a decade old and several issues have been discovered since their then. One of these issues is a partial negation of the intent to “democratize” money by decentralizing control of the infrastructure that creates, transmits, and stores monetary data. The Programmatic Proof of Work (ProgPoW) algorithm is intended as a possible solution to this problem for the Ethereum cryptocurrency. This paper examines ProgPow’s claim to be Application Specific Integrated Circuit (ASIC) resistant. This is achieved by isolating the proof-of-work code from the Ethereum blockchain, inserting the ProgPoW algorithm, and measuring the performance of the new implementation as a multithread CPU program, as well as a GPU implementation. The most remarkable difference between the ProgPoW algorithm and the currently implemented Ethereum Proof-of Work is the addition of a random sequence of math operations in the main loop that require increased memory bandwidth. Analyzing and comparing the performance of the CPU and GPU implementations should provide an insight into how the ProgPoW algorithm might perform on an ASIC.
The main incentives of blockchain technology are distribution and distributed change, consistency, and consensus. Beyond just being a distributed ledger for digital currency, smart contracts add transaction protocols to blockchains to execute terms of a contract in a blockchain network. Inter-blockchain (IBC) protocols define and control exchanges between different blockchains.
The Isabelle Infrastructure framework has been designed to serve security and privacy for IoT architectures by formal specification and stepwise attack analysis and refinement. A major case study of this framework is a distributed health care scenario for data consistency for GDPR compliance. This application led to the development of an abstract system specification of blockchains for IoT infrastructures.
In this paper, we first give a summary of the concept of IBC. We then introduce an instantiation of the Isabelle Infrastructure framework to model blockchains. Based on this we extend this model to instantiate different blockchains and formalize IBC protocols. We prove the concept by defining the generic property of global consistency and prove it in Isabelle.
The OWASP Top Ten List is a widely-recognized tool for identifying vulnerabilities in web applications. Since blockchain-specific security guidance is currently lacking, mapping existing frameworks, such as OWASP, to the blockchain can help in the identification of potential vulnerabilities in blockchain systems. While the OWASP Top Ten List is designed to describe the vulnerabilities that web application developers face, nine of ten of the OWASP vulnerabilities also apply to blockchain systems. The exception, XML External Entities (XXE), is not applicable due to the lack of use of XML in blockchain.
We give a construction of a non-interactive zero-knowledge (NIZK) argument for all \(\mathsf {NP}\) languages based on a succinct non-interactive argument (SNARG) for all \(\mathsf {NP}\) languages and a one-way function. The succinctness requirement for the SNARG is rather mild: We only require that the proof size be \(|\pi |=\mathsf {poly}(\lambda )(|x|+|w|)^c\) for some constant \(c<1/2\), where |x| is the statement length, |w| is the witness length, and \(\lambda \) is the security parameter. Especially, we do not require anything about the efficiency of the verification.
We study adaptive security of delayed-input Sigma protocols and non-interactive zero-knowledge (NIZK) proof systems in the common reference string (CRS) model. Our contributions are threefold:
We exhibit a generic compiler taking any delayed-input Sigma protocol and returning a delayed-input Sigma protocol satisfying adaptive-input special honest-verifier zero knowledge (SHVZK). In case the initial Sigma protocol also satisfies adaptive-input special soundness, our compiler preserves this property.
We revisit the recent paradigm by Canetti et al. (STOC 2019) for obtaining NIZK proof systems in the CRS model via the Fiat-Shamir transform applied to so-called trapdoor Sigma protocols, in the context of adaptive security. In particular, assuming correlation-intractable hash functions for all sparse relations, we prove that Fiat-Shamir NIZKs satisfy either:
(i)
Adaptive soundness (and non-adaptive zero knowledge), so long as the challenge is obtained by hashing both the prover’s first round and the instance being proven;
(ii)
Adaptive zero knowledge (and non-adaptive soundness), so long as the challenge is obtained by hashing only the prover’s first round, and further assuming that the initial trapdoor Sigma protocol satisfies adaptive-input SHVZK.
We exhibit a generic compiler taking any Sigma protocol and returning a trapdoor Sigma protocol. Unfortunately, this transform does not preserve the delayed-input property of the initial Sigma protocol (if any). To complement this result, we also give yet another compiler taking any delayed-input trapdoor Sigma protocol and returning a delayed-input trapdoor Sigma protocol with adaptive-input SHVZK.
Verifiable mix nets, and specifically proofs of (correct) shuffle, are a fundamental building block in numerous applications: these zero-knowledge proofs allow the prover to produce a public transcript which can be perused by the verifier to confirm the purported shuffle. They are particularly vital to verifiable electronic voting, where they underpin almost all voting schemes with non-trivial tallying methods. These complicated pieces of cryptography are a prime location for critical errors which might allow undetected modification of the outcome.The best solution to preventing these errors is to machine-check the cryptographic properties of the design and implementation of the mix net. Particularly crucial for the integrity of the outcome is the soundness of the design and implementation of the verifier (software). Unfortunately, several different encryption schemes are used in many different slight variations which makes it infeasible to machine-check every single case individually. However, a particular optimised variant of the Terelius-Wikström mix net is, and has been, widely deployed in elections including national elections in Norway, Estonia and Switzerland, albeit with many slight variations and several different encryption schemes.In this work, we develop the logical theory and formal methods tools to machine-check the design and implementation of all these variants of Terelius-Wikström mix nets, for all the different encryption schemes used; resulting in provably correct mix nets for all these different variations. We do this carefully to ensure that we can extract a formally verified implementation of the verifier (software) which is compatible with existing deployed implementations of the Terelius-Wikström mix net. This gives us provably correct implementations of the verifiers for more than half of the national elections which have used verifiable mix nets.Our implementation of a proof of correct shuffle is the first to be machine-checked to be cryptographically correct and able to verify proof transcripts from national elections. We demonstrate the practicality of our implementation by verifying transcripts produced by the Verificatum mix net system and the CHVote e-voting system from Switzerland.
Mikhail Mandrykin, Jake O’Shannessy, Jacob Payne, Ilya Shchepetkov
As smart contracts are growing in size and complexity, it becomes harder and harder to ensure their correctness and security. Due to the lack of isolation mechanisms a single mistake or vulnerability in the code can bring the whole system down, and due to this smart contract upgrades can be especially dangerous. Traditional ways to ensure the security of a smart contract, including DSLs, auditing and static analysis, are used before the code is deployed to the blockchain, and thus offer no protection after the deployment. After each upgrade the whole code need to be verified again, which is a difficult and time-consuming process that is prone to errors. To address these issues a security protocol and framework for smart contracts called Cap9 was developed. It provides developers the ability to perform upgrades in a secure and robust manner, and improves isolation and transparency through the use of a low level capability-based security model. We have used Isabelle/HOL to develop a formal specification of the Cap9 framework and prove its consistency. The paper presents a refinement-based approach that we used to create the specification, as well as discussion of some encountered difficulties during this process.
Many important cryptographic primitives offer probabilistic guarantees of security that can be specified as quantitative hyperproperties; these are specifications that stipulate the existence of a certain number of traces in the system satisfying certain constraints. Verification of such hyperproperties is extremely challenging because they involve simultaneous reasoning about an unbounded number of different traces. In this paper, we introduce a technique for verification of quantitative hyperproperties based on the notion of trace enumeration relations. These relations allow us to reduce the problem of trace-counting into one of model-counting of formulas in first-order logic. We also introduce a set of inference rules for machine-checked reasoning about the number of satisfying solutions to first-order formulas (aka model counting). Putting these two components together enables semi-automated verification of quantitative hyperproperties on infinite state systems. We use our methodology to prove confidentiality of access patterns in Path ORAMs of unbounded size, soundness of a simple interactive zero-knowledge proof protocol as well as other applications of quantitative hyperproperties studied in past work.
Abstract Solidity is the dominant programming language for Ethereum smart contracts. This paper presents a high-level formalization of the Solidity language with a focus on the memory model. The presented formalization covers all features of the language related to managing state and memory. In addition, the formalization we provide is effective: all but few features can be encoded in the quantifier-free fragment of standard SMT theories. This enables precise and efficient reasoning about the state of smart contracts written in Solidity. The formalization is implemented in the SOLC-VERIFY verifier and we provide an extensive set of tests that covers the breadth of the required semantics. We also provide an evaluation on the test set that validates the semantics and shows the novelty of the approach compared to other Solidity-level contract analysis tools.