PaperlayerView exact revision on arXiv

Source-linked AI summary

Raziel: Private and Verifiable Smart Contracts on Blockchains

David Cerezo Sánchez

arXiv:1807.09484v2cs.CR

TL;DR

Smart contracts on blockchains need privacy, confidentiality, and verifiability, while formal verification and cryptographic techniques each leave part of the problem unresolved. Raziel combines secure computation and formal verification to address these goals. The paper reports resolving the DAO and Gyges attacks and demonstrates practical viability with examples.

  • Problem

    Smart contracts require privacy, confidentiality, and verifiability, but cryptographic techniques and formal verification alone do not provide all these guarantees.

    Source: §1 · p. 2

  • Method

    Raziel combines secure computation with formal verification to provide smart contracts with privacy, correctness, and verifiability guarantees.

    Source: §1 · p. 2

  • Results

    Raziel reports resolving the DAO and Gyges attacks and demonstrates practical viability with examples.

    Source: §10 · p. 41

  • Takeaways & Limitations

    The paper concludes that the privacy, correctness, and verifiability problem for smart contracts has been successfully addressed within the demonstrated scope.

    Source: §10 · p. 41

    The threat model excludes side-channel and denial-of-service attacks.

    Source: §3.1 · p. 5

Abstract

from arXiv · show

Raziel combines secure multi-party computation and proof-carrying code to provide privacy, correctness and verifiability guarantees for smart contracts on blockchains. Effectively solving DAO and Gyges attacks, this paper describes an implementation and presents examples to demonstrate its practical viability (e.g., private and verifiable crowdfundings and investment funds). Additionally, we show how to use Zero-Knowledge Proofs of Proofs (i.e., Proof-Carrying Code certificates) to prove the validity of smart contracts to third parties before their execution without revealing anything else. Finally, we show how miners could get rewarded for generating pre-processing data for secure multi-party computation.

1 Introduction

Raziel addresses the need for smart contracts that protect confidentiality and privacy while remaining verifiable, combining cryptography with formal verification. Its contributions include secure computation, verifiable code, privacy-preserving proof certificates, and cost-reduction approaches.

1 Introduction

  • Raziel combines secure computation and formal verification to target smart-contract privacy, correctness, and verifiability.The introduction frames the combination as necessary because neither cryptographic techniques nor formal verification alone provides all the required guarantees.Source: §1 · p. 2
  • The introduction motivates better-protected smart contracts as necessary for blockchain-based digital businesses and a public interest.It identifies confidentiality, privacy, and efficient verification as desired qualities.Source: §1 · p. 2
  • Formal proofs can establish functional correctness and properties such as termination, security, preconditions, postconditions, and invariants, addressing DAO bugs and Gyges attacks.The paper says signed proofs conforming to trusted-organization specifications can prevent criminal contracts.Source: §1 · p. 2
  • Zero-knowledge proofs of proofs let a code producer demonstrate valid code proofs without revealing the proofs or smart-contract code.The paper proposes practical non-interactive certificates for general properties of code, while noting the underlying concept is not new [Blu87, BOGG+90, Pop04].Source: §1 · pp. 2–3
  • The outsourcing protocol supports offline parties and private parameter reuse, which previous approaches did not both allow [MGBF14, CMTB13, CLT14, CT16, BS14] [KMR11, KMR12].These are presented as features of the protocol for secure computation.Source: §1 · p. 2
  • The paper proposes rewarding miners for generating MPC preprocessing data, alongside cloud outsourcing, to reduce encrypted-computation costs.The proposal is framed in line with earlier attempts to replace wasteful proof-of-work [Kin13, MJS+14, BRSV17, ORP17].Source: §1 · p. 3

2 Background

The background introduces blockchains and smart contracts, secure multi-party computation, and formal verification as the technologies underpinning Raziel.

Blockchains

  • Blockchains are distributed ledgers of linked, unmodifiable blocks; permissionless networks lack access controls, while permissioned networks limit participation through identity systems.On-chain smart contracts run on all or many nodes and must minimize execution costs; off-chain frameworks support more complex processes.Source: §2 · p. 4

Secure Multi-Party Computation

  • MPC lets multiple parties jointly compute over inputs without disclosing them, aiming for input privacy and correctness.The background distinguishes semi-honest, covert, and malicious security models and lists techniques including secret sharing, oblivious transfer, garbled circuits, and ORAM.Source: §2 · p. 4

Formal verification

  • Formal verification uses mathematical methods to prove or disprove software correctness against formal specifications.Deductive verification annotates contracts to generate proof obligations for theorem provers or satisfiability-modulo-theories solvers.Source: §2 · p. 4

3 Model and Goals

Raziel targets formally verified, privacy-preserving smart contracts for parties seeking to protect private financial information and obtain execution guarantees. Its model assumes mutual distrust, trusts each party's environment and the blockchain, and supports execution with or without external nodes.

3 Model and Goals

  • Raziel aims to facilitate formally verified, privacy-preserving smart contracts using secure computation for parties protecting private financial information.Source: §3 · p. 5

3.1 Threat Model and Assumptions

  • The threat model treats parties as potentially malicious and mutually distrustful, while assuming each trusts its own environment and the blockchain.The rest of the system is untrusted; side-channel and denial-of-service attacks are excluded.Source: §3.1 · p. 5

3.2 Goals

  • Parties check proofs or certificates before execution, then provide private inputs to nodes running secure computation, or compute among themselves without external nodes.The resulting outputs may be stored on the blockchain under a consensus protocol.Source: §3.2 · p. 5

4 Private Smart Contracts

Raziel uses secure multi-party computation (MPC) to protect smart-contract computations, with execution and protocol choices adapted to blockchain costs and network conditions. The section also describes oracle-based execution, alternative financial standards, and an open protocol framework.

4 Private Smart Contracts

  • Raziel selects MPC because it has mature production options and a less trusting threat model than trusted hardware, while homomorphic encryption and obfuscation are considered infeasible for the intended use.The paper notes SGX vulnerabilities and the need to deploy new hardware to fix some hardware bugs.Source: §4 · pp. 5–6

4.1 Off-chain computation

  • More than 18 billion times more expensive: Ethereum execution of 10 million multiplications costs far more than performing them on a modern computer.The paper also compares 7 billion AND gates per second for secure computation with 316 GIPS for an 8-core processor, reporting an approximate 45.14 slowdown.Source: §4.1 · pp. 6–7
  • For on-chain computation, the design relaxes full replication by running a query on a restricted set of nodes and recording its result with an invoke; off-chain calls can use oracle-like protocols.The restricted set must be large enough to provide consensus.Source: §4.1 · p. 7

4.1.1 Latency and its impact

  • Protocol choice depends on latency: low-latency parties can use fast secret sharing, while high-latency settings call for constant-round protocols or cloud outsourcing.The paper proposes two protocol suites to maximize performance across latency settings.Source: §4.1.1 · pp. 7–8

4.2 Blockchain Solutions

  • Blockchain integration varies by platform: Fabric can run complex procedures in chaincode, whereas Ethereum’s gas costs make oracles a better option for complex execution.For Ethereum oracle calls, parameters should be encrypted; large results may be stored on IPFS with a pointer returned to the contract.Source: §4.2 · pp. 8–9

4.2.1 Alternative Protocols and Standards

  • The approach could also be adopted for financial messaging standards such as FIX and FpML.FIX supports trade communication; FpML is an XML messaging standard for over-the-counter derivatives.Source: §4.2.1 · p. 9

4.3 Functionality and Protocol

  • The functionality and protocols form an open framework for instantiating different MPC protocols as research advances.The specified functionality identifies blockchain nodes, participating parties, a smart contract, and parties’ private inputs.Source: §4.3 · pp. 9–10

2. Results are returned and/or saved on the blockchain B

This section describes when secure-computation results are returned or recorded on the blockchain, along with blockchain interaction, cloud outsourcing, and incentivized MPC preprocessing and their security conditions. It also covers secure-cover probability, deposits to deter Sybil attacks, and applications of secure computation in commercial, financial, game-theoretic, and statistical settings.

2. Results are returned and/or saved on the blockchain B

  • After the executing nodes run the contract, results are returned to the parties and/or written to the blockchain only if consensus is reached.Parties supply private and non-private inputs; they must agree on the preferred secure-computation engine, or computation does not proceed. On permissioned chains, executing nodes should be party-operated servers, while uncontrolled servers require an outsourcing protocol.Source: §2 · p. 11

4.4 Experimental Results

  • Table 1 reports wall-clock milliseconds for MPC execution across several engines and economically significant application examples.The supplied passages describe examples including private auctions, exchange options, crowdfunding, and investment funds, but provide no table cell values.Source: §4.4 · p. 11, Table 1 · p. 14

4.5 Modes of Interaction

  • Secure computation may run on blockchain nodes or on the parties themselves, be outsourced to the cloud, or use mined MPC preprocessing data.The passage points to later sections for the cloud-outsourcing and preprocessing modes.Source: §4.5 · pp. 14–15

4.6 Outsourcing Secure Computations for Cloud-based Blockchains

  • Cloud outsourcing is designed to let parties remain offline during execution and reuse private parameters, while restricting an adversary from corrupting both parties and blockchain nodes [KMR11].A multiparty non-interactive key exchange establishes shared secrets between computing parties and executing nodes, avoiding a PKI infrastructure described as more cumbersome for public permissionless ledgers [BZ13, MZ17].Source: §4.6 · p. 15

Functionality B.1: Outsourcing for Cloud-based Blockchains

  • Protocol B.2 securely realizes cloud-based outsourcing against static corruptions in the semi-honest model, assuming secure channels and a garbling scheme with privacy, obliviousness, and correctness.The protocol derives a shared key, uses encrypted inputs and a pivot table to map them to garbled-circuit inputs, and evaluates the contract at blockchain nodes.Source: Functionality B.1: Outsourcing for… · pp. 16–18

4.7 Mining pre-processing data for Secure Multi-Party Computation

  • Miners could earn crypto-tokens for preprocessing MPC data, which accounts for 50–80% of total execution time depending on the function and protocol.The proposal has offline preprocessing parties generate authenticated shares, which are reshared among computing parties before secure computation.Source: §4.7 · pp. 18–19

4.7.1 Security setting

  • A secure cover associates outsourcing parties with subsets of executing parties so at least one honest outsourcing party is linked to an honest executing party; random assignment is described as adversary-resistant with negligible failure probability.The setting permits corruption of a majority in either group, but not all parties in either group; the assignment algorithm assumes each outsourcing party sends to l ≥ ⌈nE/nO⌉ executing parties.Source: §4.7.1 · p. 19
  • When all but one party is corrupt in each of E and O, the probability of obtaining a secure cover is l/nE.The preceding passage presents a general probability expression for obtaining a secure cover.Source: §4.7.1 · p. 20

4.7.2 Preventing Sybil attacks

  • Requiring parties to deposit funds that are confiscated for abnormal behavior can deter Sybil attacks while preserving anonymity and preventing intentional waste of pre-processing data.Examples of abnormal behavior include selective failure attacks and aborts.Source: §4.7.2 · p. 20

4.8 Other Applications

  • Secure computation could remove financial intermediaries and enable private crypto-banking, confidential risk-sharing [EAA11], credit scoring [DDN+15, Lie13], and stock markets without trusted auctioneers.Other cited uses include financial supervision [FKOS13], privacy in online marketplaces [CHK+11], and claim-or-refund transactions to remove escrows [Kum16].Source: §4.8 · p. 20
  • Game-theoretic applications include private tâtonnement algorithms [WC14], privacy-preserving auctions [AACM16, AV17], and incentive-compatible mechanisms [NPS99, EL03].The cited work also describes privately sharing utility functions and incentivizing data-driven collaboration among competing parties [AGP15].Source: §4.8 · pp. 20–21
  • Statistical applications include benchmarking companies within a sector [BTW11] and establishing correlation and causation between confidential datasets [BKK+15].Source: §4.8 · p. 21

5 Verifiable Smart Contracts

Raziel uses proof-carrying code to let consumers check properties of untrusted smart contracts before execution. The section presents broad proof targets while noting that verification effort can grow substantially with specification size.

5 Verifiable Smart Contracts

  • Formal verification of smart contracts remains complex and cumbersome in existing approaches, with even C described as too low-level for the required proof details.The paper argues that smart contracts should be written in high-level languages rather than assembly-like ones.Source: §5 · p. 21
  • The proofs can cover properties beyond output correctness, including invariants, termination, security, resource use, and economic or legal requirements.The paper contrasts this multi-purpose approach with work focused only on computed-output correctness.Source: §5 · p. 21
  • Proof-carrying code lets consumers check proofs against their security policy before executing untrusted code, without trusting the producer or adding runtime overhead.The code must be annotated and detailed proofs generated, which can be complex and costly.Source: §5 · p. 22
  • Verification has a substantial scaling burden: effort relates linearly to proof size, while statement size relates quadratically to final proof size.The paper says complete proofs become extremely complex when verification is not considered during contract design.Source: §5 · p. 23
  • Verification can be scaled to the setting: some permissioned blockchains may publish annotated contracts without the PCC toolchain or a theorem prover.This reverses the burden of proof to code consumers while still providing annotations.Source: §5 · pp. 21, 23

1. Annotated smart contracts

The subsection states that annotated smart contracts are automatically tested using heuristics or concolic execution.

1. Annotated smart contracts

  • Annotated smart contracts are automatically tested using heuristics or concolic execution.Source: §1 · p. 23

3. Annotated smart contracts with full/partial proofs

Raziel combines annotated smart contracts and proof-carrying certificates, with a case study and techniques for reducing certificate costs. It also describes zero-knowledge proofs of proofs that let a producer demonstrate certificate validity without revealing the proofs or contract code.

3. Annotated smart contracts with full/partial proofs

  • The case study applies annotated proof-carrying code to crowdfunding and identifies exchange proofs of assets, liabilities, and solvency as another application.The proposed combination uses annotated contracts with the zero-knowledge proofs described in Section 5.3.Source: §3 · p. 23, §5.1 · p. 23

5.1 Case Study

  • The crowdfund case study reports 30% certificate-size overhead and proof-generation time approximately correlated with compiled-program size.Proof-verification time is described as less correlated with compiled-program size; the reported time formulas use a modern laptop.Source: §5.1 · p. 24

5.2 On the Size of Certifiable Certificates

  • Certificate-size reduction techniques include reflection, deep embedding, static analysis, certificate partitioning, abstract interpretation, and sequent-calculus reconstruction.For abstract interpretation, reducing certificate size trades off against checking time; the consumer may regenerate the fixed point at increased checking cost.Source: §5.2 · p. 25
  • The section also considers transmitting a proof generator for execution by the consumer instead of transmitting the proof itself.The consumer would regenerate the proof using a virtual machine.Source: §5.2 · p. 25

5.3 Zero-Knowledge Proofs of Proofs

  • Proof-carrying certificates can be presented through zero-knowledge proofs of proofs, demonstrating proof validity without revealing the proofs or smart-contract code.The proposed approach uses ZKBoo to prove knowledge of a certificate that passes its validation circuit, with soundness error 2^-80.Source: §5.3 · p. 26
  • ZKBoo is presented as the preferred choice for non-interactive zero-knowledge proofs of certificate validity, while zk-SNARKs require setup assumptions and are slower to prove.The passage also describes later proof-size improvements: ZKB++ proofs are less than half the size of ZKBoo proofs, and Ligero proofs are four times shorter than ZKB++ proofs.Source: §5.3 · p. 26

6 Private and Verifiable Smart Contracts

Raziel’s combined private and verifiable smart-contract implementation uses Obliv-Java for secure computation and JML annotations for verification. Verification results are discharged as proof-carrying code.

6 Private and Verifiable Smart Contracts

  • Obliv-Java supports private smart-contract development, while JML annotations provide verification whose results are discharged as proof-carrying code.The text describes Obliv-Java as a modified Open-JDK for secure computation, with variables annotated using @Obliv(partyId).Source: §6 · p. 27

7 Functionalities and Protocols

Raziel specifies protocols that verify smart contracts before securely executing them on private inputs. The paper states security results for standard and extended verification, and describes extensions for malicious security and private function evaluation.

7.1 General Overview

  • The overview figure organizes the paper’s functionalities and their realized protocols into corresponding top and bottom portions.Source: Figure 7.1 · p. 27

7.2 Detailed Description

  • The general execution protocol verifies the contract and then securely executes it on parties’ private inputs, returning computation results to the parties.The protocol combines standard verification functionality with secure computation functionality.Source: §7.2 · pp. 28, 30

7.3 Security Analysis

  • Protocol 6.4 realizes private and verifiable smart-contract functionality against static corruptions in the semi-honest model, augmented with code verifiability.The analysis assumes semi-honest security of the underlying building blocks, including Yao’s protocol and oblivious transfer with OT-extension.Source: §7.3 · p. 30

7.4 Extended verification of smart contracts

  • The extended protocol checks trusted-party signatures and specification conformance before secure computation, and its theorem states security with extended code verifiability.The extended verification step may be computationally expensive, but need only be repeated when the contract is modified.Source: §7.4 · pp. 32–34

7.5 Malicious security

  • The protocols can be updated to use malicious-security secure-computation frameworks, with security then relying on their corresponding definitions and proofs.For ORAMs, the text points to specialized protocols for security against malicious adversaries.Source: §7.5 · p. 34

7.6 Private Function Evaluation

  • Private function evaluation keeps the smart-contract function known only to one party, while other parties learn no more than circuit size and input/output counts.The described approach uses secure function evaluation of a Universal Circuit programmed by the party holding the function.Source: §7.6 · p. 35
  • Universal-circuit size is described as Ω(k log k), while reported online times are 1–4% of total execution in WAN settings and 2–5% in LAN settings.The passage notes that pre-processing could ameliorate execution times despite the circuit-size blowup.Source: §7.6 · p. 35

8 Economic Impact and Legal Analysis

The section considers legal and economic implications of privacy-preserving smart contracts, including privacy as quasi-property and the effects of secure computation on information markets (p016–p020).

8.2 A Solution to Arrow’s Paradox

  • Secure computation lets distrustful parties value private information without disclosure, addressing Arrow’s Paradox while preserving the producer’s market power and allowing costless resale.The paper notes that practical use must account for secure computation’s slowdown.Source: §8.2 · p. 36

8.3 Expansion of Trade Secrecy

  • Trade-secret law offers a durable protection for software, while secure computation can hinder reverse engineering and may support stronger trade secrecy.The paper expects similar effects to those associated with stronger trade-secret law, including increased R&D, reduced patenting, and increased trade flows.Source: §8.3 · pp. 36–37

8.4 Verifiability and Self-Enforcement

  • Third-party specifications can let governments, regulators, or standards bodies check whether smart contracts conform, tempering concerns about strict self-enforcement.The paper frames contracting parties as private lawmakers while allowing third parties to specify properties contracts must formally verify.Source: §8.4 · pp. 37–38

8.5 Markets for Smart Contracts

  • Private smart contracts could create markets by protecting algorithmic value or, more practically, by transferring encrypted data processed by the contracts.The paper says secure computation can protect even open-source software and that safe trading could justify higher development costs.Source: §8.5 · p. 38

8.6 Effects on Currency Competition

  • Private and verifiable smart contracts could provide market power to issuers and users through natural monopolies on encrypted programs.The section situates this possibility within discussion of currency competition and diverse cryptocurrency functionalities.Source: §8.6 · pp. 38–39

8.7 Token vs. Account-based Cryptocurrencies

  • Smart contracts’ privacy and formal-verification capabilities make them a proposed fit for the more complex technology required by account-based cryptocurrencies.The section contrasts account-based currencies with token-based systems and cites possible efficiency gains from the former.Source: §8.7 · p. 39

8.8 Impact on Market Structures

  • The effect on financial-industry concentration is difficult to estimate because many variables interact, though the paper predicts shadow banking will increase.It cites financial technology as accounting for 35% of shadow banking growth.Source: §8.8 · pp. 39–40

8.9 The Valuation of Secrecy and the Privacy Multiplier

  • Private smart contracts can preserve a secrecy discount while allowing the same data to be sold repeatedly without exhausting its exclusivity, a valuation effect the paper calls the Privacy Multiplier.The cited formula’s parameters include time to maturity, dividend yield, and secret-data price volatility.Source: §8.9 · p. 40

9 Related work

The related work spans privacy-preserving transactions, MPC, and verification, while distinguishing Raziel’s focus on smart contracts and pre-execution proof-carrying code.

MPC and smart-contract platforms

  • Enigma lacks formal semantics and verification libraries for proof-carrying code, while WYS* is not blockchain-integrated and does not offer proof-carrying code.The paper also notes Enigma’s non-constant-round protocols and Bitcoin-only ledger support.Source: §9 · p. 40

Privacy systems

  • Chainspace includes private smart-contract examples but provides zero-knowledge proofs only after execution; ZeroCash and Monero secure transactions rather than smart contracts.The paper notes that secure transactions are a restricted case of cryptographic smart contracts.Source: §9 · p. 41

Cryptographic verification

  • Accountable algorithms provide compliance proofs after decisions, whereas Raziel’s certificates establish smart-contract proof validity before execution without revealing the proofs or code.The paper also distinguishes earlier restricted languages for zero-knowledge proofs of knowledge from its general-purpose proof-of-proofs approach.Source: §9 · p. 41

Related approaches

  • Other cited work combines MPC with Bitcoin for fairness or verifies leakage in MPC, while Oyente symbolically executes Ethereum contracts.The paper contrasts these projects’ aims with improving smart-contract privacy, correctness, and verifiability.Source: §9 · p. 41

10 Conclusions, subsequent and future work

The paper concludes that Raziel addresses smart-contract privacy, correctness, and verifiability, with examples offered as evidence of practical viability. It also describes subsequent work on persistent garbled-circuit state and identifies ongoing development and future upgrade needs.

10 Conclusions, subsequent and future work

  • The paper reports resolving DAO and Gyges attacks while improving smart-contract privacy, correctness, and verifiability, and presents examples of practical viability.The examples are described as demonstrations, not quantitative evaluations.Source: §10 · p. 41

10.1 Subsequent work

  • Saving and restoring garbled-circuit state brings the technique closer to secret sharing; cited follow-on work includes partial, reactive, and reusable garbled circuits.Partial garbled circuits map evaluator wire labels from a previous circuit to valid labels in the next computation.Source: §10.1 · pp. 41–42

10.2 Future work

  • Perpetual contracts storing encrypted computation may eventually need encrypted-content updates to upgrade their security level; Raziel remains under development.The paper also identifies realistic threat models and abstractions for SGX as difficult to derive.Source: §10.2 · p. 42, §10.1 · p. 42

A Outsourcing Secure Computations for Cloud-based Blockchains

The appendix presents a security argument for outsourcing secure computation to blockchain nodes, describing a hybrid proof and separate cases for corrupted nodes and parties.

Security result

  • Protocol B.2 securely realizes Functionality B.1 against static corruptions in the semi-honest model when the garbling scheme satisfies privacy, obliviousness, and correctness.The theorem states secure-channel assumptions between parties and blockchain nodes.Source: A Outsourcing Secure Computations for… · p. 58

Corruption cases

  • The proof treats corruption of an executing node separately from corruption of a party, with party-view indistinguishability attributed to secure channels.For corrupted parties, the simulator’s result differs by selecting correct garbled values from the ideal functionality rather than evaluating the circuit.Source: A Outsourcing Secure Computations for… · pp. 58–60

Proof strategy

  • The proof uses hybrid games to replace real inputs with random values, encrypt pivot-table entries, and substitute simulated garbled circuits before reaching the ideal-world view.The hybrids rely on pseudorandomness, encryption indistinguishability, and garbled-circuit security.Source: A Outsourcing Secure Computations for… · pp. 58–59

Related papers

Loading 1807.09484v2…