Scriptable and composable SNARKs in the trusted hardware model 1

Abstract

Non-interactive zero-knowledge proof or argument (NIZK) systems are widely used in many security sensitive applications to enhance computation integrity, privacy and scalability. In such systems, a prover wants to convince one or more verifiers that the result of a public function is correctly computed without revealing the (potential) private input, such as the witness. In this work, we introduce a new notion, called scriptable SNARK, where the prover and verifier(s) can specify the function (or language instance) to be proven via a script. We formalize this notion in UC framework and provide a generic trusted hardware based solution. We then instantiate our solution in both SGX and Trustzone with Lua script engine. The system can be easily used by typical programmers without any cryptographic background. The benchmark result shows that our solution is better than all the known SNARK proof systems w.r.t. prover’s running time (1000 times faster), verifier’s running time, and the proof size. In addition, we also give a lightweight scriptable SNARK protocol for hardware with limited state, e.g., $Θ (λ)$ bits. Finally, we show how the proposed scriptable SNARK can be readily deployed to solve many well-known problems in the blockchain context, e.g. verifier’s dilemma, fast joining for new players, etc.

Keywords

Scriptable SNARK universal composition trusted hardware model

1. Introduction

Collaboration is one of the main driving forces for the sustainable advancement of our civilization, growing from small-size tributes, to cities, and then to large-scale states. Being a part of the modern society, we are interacting with hundreds of known/unknown entities either physically or remotely. The main motivation of this work is to introduce new concepts and frameworks to enable more effective collaborations. One potential candidate tool is a well-known cryptographic primitive—zero knowledge (ZK) proof/argument system. In a ZK system, two players, the prover and the verifier, are involved; on one hand, the prover who holds a valid witness of an NP statement, is able to convince the verifier that the statement is true without revealing the corresponding witness; on the other hand, if the prover does not know any valid witness of the statement, then he cannot convince the verifier. ZK systems can be used to enable trustworthy collaborations: all players in a protocol are required to prove the correctness of their behaviors in the protocol execution. However, to enable effective collaborations, desired properties are expected, and we will elaborate them below.

1.1. Our design goals

In a large-scale collaboration network, it is infeasible for a party to prove the correctness of its computation to all other parties one by one. The first property we need from ZK systems, is (1) non-interactiveness in the sense that the prover only needs to prove the correctness of the computation once, and the prover then can send the same proof to all other parties i.e., the verifiers. From now on, we use NIZK to denote non-interactive ZK systems. The second desirable property we need is (2) succinctness, given the fact that the bottleneck for large-scale collaboration is the capacity of the underlying peer-to-peer network communication. Furthermore, as already mentioned, we note that in a typical application scenario a single prover will prove the same statement to many verifiers. In this unbalanced setting, a desirable NIZK proof system should have the property of (3) lightning fast verification time.

Up to now, those properties have already been achieved by a number of existing NIZK proof systems, such as zk-SNARK [7,23,52], zk-STARK [4], etc. However, these NIZK systems have not been widely used in practice yet. A significant barrier is the that the computation of prover is very heavy. The state-of-the-art NIZK systems needs hours to prove large statement even on a powerful PC (32 cores and 512 GB RAM [4]), let alone portable devices such as smartphones, tablets, and IoT devices. We aim to develop a NIZK system with the property of (4) lightweight prover.

To enable wide adoption of NIZK in the real world, the design must be (5) deployment friendly. The underlying cryptographic machinery should be transparent to the developers, and the protocol can be operated without cryptographic background. Unfortunately, all existing NIZK proof systems for universal language require re-compilation of both prover and verifier’s executable binary files for every new language instance.

1.2. Our approach

We propose a new primitive, called scriptable SNARK, with the goal of achieving all desirable properties above. This new primitive allows the developers to specify the language instance or computation to be verified via a script without any re-compilation. Similar to NIZK proof systems for universal language, a scriptable SNARK system can support multiple language instances, depending on the script language design and the script engine execution environment. Different from existing SNARK systems for universal language, our scriptable SNARK is very easy to use; for a new language instance, the players can easily define the scripts and no further compilation is required.

We study our scriptable SNARK in the UC framework [13,14]: we define an ideal functionality for scriptable SNARK, and then give two efficient realizations in the trusted hardware model. To the best of our knowledge, there is no UC-secure SNARK protocol proposed in the literature. The main reason is that the extractable soundness property of SNARKs in the CRS/RO model require unfalsifiable assumptions [24], such as the knowledge assumption, which is not UC-friendly. Kosba et al. [37] has made an attempt on constructing composable NIZK systems, but their protocol is not succinct. To bypass this impossibility result, our protocols utilize a stronger setup assumption, trusted hardware model.

Defining scriptable SNARK. We introduce a new notion called scriptable SNARK. Unlike the conventional SNARK, the scriptable SNARK allows the users to specify the relation to be proven via a script. More precisely, the prover only can prove a certain relation in the conventional SNARK, while the prover is allowed to prove any script execution as long as the script is supported.

Formally, we assume both the prover and the verifiers have agreed on the function/script, denoted as $C$ , the public input, denoted as ${Input}_{pub}$ , and the (public) output, denoted as $Output$ ; in addition, the prover keeps a private input, denoted as ${Input}_{priv}$ , such that $C ({Input}_{pub}, {Input}_{priv}) = Output$ . The prover is able to prove the verifiers that he knows a private input ${Input}_{priv}$ that would make the script execution $C ({Input}_{pub}, {Input}_{priv})$ to generate output $Output$ . We note that not all scripts can be supported; each scriptable SNARK system is parameterized by a predicate $Q$ , and $Q (C, {Input}_{pub}, {Input}_{priv}, Output) = 1$ for any valid script $C$ . The predicate $Q$ is defined by the script language design and the script engine execution environment.

An NP language $L$ is defined by its polynomial-time decidable relation $R$ ; namely, $L : = {x : \exists w s.t. (x, w) \in R}$ . In practice, for each relation $R$ , we assume there exists a corresponding script $C_{R}$ such that $C_{R} (x, w) = 1$ iff $(x, w) \in R$ ; otherwise, $C_{R} (x, w) = 0$ . To use the scriptable SNARK system for an NP language, the prover and the verifiers set ${Input}_{pub} : = x$ , ${Input}_{priv} : = w$ , $Output : = 1$ , and the script as $C_{R}$ . The notion is formally modeled in the UC framework.

Constructing scriptable SNARKs. We then present a generic scriptable SNARK construction in the trusted hardware model. Trusted hardware can enable an isolated and trusted computation environment where security sensitive data can be stored and processed with confidentiality and integrity guarantees. Most existing trusted hardware based applications, e.g., [22] emphasize on the confidentiality aspect, while the security of our construction mainly relies on the computational integrity guaranteed by trusted hardware. The main idea is as follows. Recall that in a NIZK proof, the prover and the verifier have common input $(C_{R}, {Input}_{pub} : = x)$ . The potentially malicious prover wants to convince the verifiers that he knows a witness ${Input}_{priv} : = w$ such that $C_{R} ({Input}_{pub}, {Input}_{priv}) = 1$ . Since the trusted hardware can guarantee computation integrity even when the host is malicious, we can let $O_{HW}^{Q}$ to execute the relationship decision algorithm $b \leftarrow C_{R} (x, w)$ and sign the output b. To bind the decision algorithm and statement, we let $O_{HW}^{Q}$ sign $(C_{R}, x, b)$ without revealing the witness w. Therefore, by checking the signature, the verifier is convinced that the prover must know a witness w such that $C_{R} (x, w) = 1$ if $(C_{R}, x, 1)$ is signed by $O_{HW}^{Q}$ . Similarly, for general computation, the private input ${Input}_{priv}$ is not signed; therefore, zero-knowledge property is preserved even if the signature leaks the signed message.

Compared with [ 60 ]. The construction proposed in the preliminary version [60] requires the trusted hardware to have large enough state that at least linearly depends in the size of the statement $| x |$ and/or the size of the witness $| w |$ ; moreover, typically, we want to hardware to be programmable. In practice, such powerful trusted hardware is not widely accessible; is it possible to design a scriptable SNARK scheme that can work with trusted hardware with limited state and functionality, such as smart card, USB tokens, etc? In this work, we propose another scheme that can work with trusted hardware with $(Θ (λ))$ -size state.

A new construction for lightweight trusted hardware. Note that, in our previous approach, the prover needs to send the entire circuit $C$ directly to the trusted hardware at once. A natural approach to minimizing the requirement of the hardware state is to disassemble the circuit $C$ into gates, and we feed the hardware k gates at a time, where k is a small constant, say $k = 1$ . Furthermore, we let the potentially malicious prover sends the hash of statement $h_{x} \leftarrow hash ({Input}_{pub}), h_{o} \leftarrow hash (OutPub)$ instead of the statement ${Input}_{pub}, Output$ to the hardware $O_{HW}^{Light}$ . Therefore, the input size can be independent to the statement. Meanwhile we re-define the relation $R^{'} : C ({Input}_{pub}, {Input}_{priv}) = Output \land h_{x} = hash ({Input}_{pub}) \land h_{o} = hash (Output)$ . Without loss of generality, for a relation $R^{'}$ , we assume there exists an efficiently computable algorithm $C_{R^{'}}$ such that $C_{R^{'}} ((h_{x}, h_{o}), ({Input}_{pub}, {Input}_{priv}, Output)) = 1$ iff $C ({Input}_{pub}, {Input}_{priv}) = Output \land h_{x} = hash ({Input}_{pub}) \land h_{o} = hash (Output)$ and otherwise $C_{R^{'}} ((h_{x}, h_{o}), ({Input}_{pub}, {Input}_{priv}, Output)) = 0$ . We assume that $C_{R^{'}}$ is made of identity gates (for input only) and NAND gates. For such $C_{R^{'}}$ , it is easy to find a deterministic polynomial-time (DPT) algorithm $Convert$ which takes $C, {Input}_{pub}, Output$ as input and outputs $L : = {L_{i}}_{i = 1}^{n}$ , where L is the description of $C_{R^{'}}$ , n is the number of the gates and we assume that $k | n$ . Then we use hash chains to guarantee the integrity of L. We set $h_{L} : = 0$ at first, and update $h_{L}$ by $h_{L} \leftarrow hash (h_{L}, {L_{k (i - 1) + j}}_{j = 1}^{k}, i)$ for $i \in [\frac{n}{k}]$ . To prevent the malicious prover from changing the assignment of wires, we let $O_{HW}^{Light}$ produce a MAC tag after executing the gate operation, and return the result along with the MAC tag. When the malicious prover sends the input wire value, he/she has to also attach its corresponding MAC tag. When $O_{HW}^{Light}$ computes the last gate operation and checks the validity, it signs $(h_{L}, h_{x}, h_{o}, n)$ which reveals nothing about ${Input}_{priv}$ ; therefore, it preserves the zero-knowledge property.

Although there are a number of works in the literature studying how to speed up secure computing via trusted hardware, such as Intel SGX, we emphasize that this problem has not been solved by previous works. The closest related work is sealed-glass proof introduced by Tramer et al. [53], where the authors try to explore some use cases even if the isolated execution environment has unbounded leakage, i.e., arbitrary side-channels. We note that, their primitive is interactive, thus not scalable; in their protocol, for each verification, the trusted hardware must be interacted with. Our primitive is non-interactive, and in our construction, the verifier can verify the proof without interacting with the trusted hardware. There are also many theoretical differences between interactive ZK and non-interactive ZK, such as the minimum assumptions needed to realize the primitive; therefore, this work is not covered by [53]. Most importantly, ours is the first work to investigate scriptable SNARK, which is developer-friendly.

1.3. Implementation

We implement our scriptable SNARK proof system on two most popular trusted hardware platforms: Intel SGX and Arm TrustZone. The main component is the $Q$ -compliant hardware functionality $O_{HW}^{Q}$ . In terms of Intel SGX, the $O_{HW}^{Q}$ functionality is instantiated by three entities: the (trusted) Intel server, the prover, and the SGX hardware device. In terms of Arm TrustZone, currently only manufacture has the privilege to access TrustZone root keys; nevertheless, our system uses Hikey 960 TrustZone development board. The $O_{HW}^{Q}$ functionality is instantiated by two entities: the (trusted) authority server, and the TrustZone development board.

With regard to scriptability, in practice, it is a challenge for a third party to verify the consistency between an executable binary and its software specification. That is, the binary contains no bug, no trapdoor, and it is not subverted. Even it is possible, it dramatically increases the verifier’s complexity. On the other hand, it is implausible to assume a trusted third party that is available to generate a certified binary for each language instance. To address this issue, we decide to adopt a scripting language, called Lua. Lua is a lightweight script language. We implemented modified Lua script engine for both Intel SGX enclave computation environment and the TrustZone environment. At a high level, we let the Intel server and/or the setup authority server to prepare and sign a Lua engine enclave/binary. The signed Lua engine is published as a common reference string (CRS). In addition, the hardware is initialized with a signing key, and it corresponding public key is also published as a part of the CRS. The modified Lua engine takes input as a script $C$ , a public input ${Input}_{pub}$ , a private input ${Input}_{priv}$ , and a tag $tag$ that can be used to store auxiliary information, such as session id. The Lua engine runs $Output \leftarrow C ({Input}_{pub}, {Input}_{priv})$ and signs $⟨ C, {Input}_{pub}, Output ⟩$ . Therefore, any verifier who has the public key can verify the signature. The predicate $Q$ is restricted by the Lua engine constrain. For instance, there is a fixed heap size, e.g., 32 MB when the Lua engine enclave is built. It limits the maximum script size. Moreover, as security requirement, one may want to introduce a maximum running time to prevent the script from running forever. Such a running time cap would also reflected by $Q$ .

Recall that scriptable SNARK proofs are typically deployed in a one-to-many scenario, where the prover only needs to invoke the trusted hardware once and many verifiers can check the validity of the proof; however, currently, the remote attestation of Intel’s SGX requires the verifier to interact with the Intel Attestation Service (IAS) server. If each verifier needs to query the Intel IAS server to check the proof, the overall performance is limited by the throughput of Intel’s IAS. Moreover, the validity of a NIZK proof should be consistent over time, i.e., if a NIZK proof is verifiable at this moment, the same proof should remain verifiable in the future. Unfortunately, this would not be the case if we invoke the Intel IAS in the verification process; certifying an old quote (say, generated 1 year ago) is never the design goal of Intel’s remote attestation. This is because the quote needs to contain a non-revoked proof for each item on the signature revocation list, and the proof is no longer verifiable once the revocation list is updated at the Intel side. That means a quote is only valid until the next revocation list update. To resolve this issue, in our design, after generating the quote, the prover immediately queries the Intel IAS server for the attestation verification report on behave of a verifier. Since the attestation verification report is signed by Intel, given Intel’s public key, anyone can verify the validity of the attached signature. This tweak also makes the verification process non-interactive.

We also implement our scriptable SNARK proof system based on trusted hardware with limited state. We simulate the hardware functionality $O_{HW}^{Light}$ on Intel SGX. Most of the instantiations are similar to the one described above, except that: (i) it only computes NAND gates; (ii) it uses MACs. (cf. Section 6.2)

Table 1
Asymptotic efficiency comparison of different SNARK proof/argument systems. $| C |$ is the circuit size; $| w |$ is the witness size; $| c |$ is the problem instance size; s is the number of copies of the subcircuits; d is the width of the subcircuits. DL stands for discrete logarithm assumption, CRHF stands for collision-resistant hash functions, SIS stands for shortest integer solution assumption, KE stands for knowledge-of-exponent assumption, HW stands for trusted hardware model, and AGM stands for algebraic group model

Scheme Setup size Proof size Prover’s time Verifier’s time Setup Asm. Comp. Asm.

Ligero [1] 1 $\sqrt{| C |}$ $| C | log | C |$ $s log s + d log d$ RO CRHF

Bootle et al. [10] 1 $\sqrt{| C |}$ $| C |$ $| C |$ RO CRHF

Baum et al. [2] $\sqrt{| C |}$ $\sqrt{| C | log | C |}$ $| C | log | C |$ $| C |$ CRS SIS

zk-STARKs [4] 1 ${log}^{2} | C |$ $| C | polylog (| C |)$ $polylog (| C |)$ RO CRHF

Aurora [6] 1 ${log}^{2} | C |$ $| C | log | C |$ $| C |$ RO CRHF

Bulletproof [12] $| C |$ $log | C |$ $| C |$ $| C | log | C |$ CRS + RO DL

zk-SNARKs [7,23,52] $| C |$ 1 $| C | log | C |$ $| c |$ CRS KE

This work 1 1 $| C |$ 1 HW Signature

Scheme	Setup size	Proof size	Prover’s time	Verifier’s time	Setup Asm.	Comp. Asm.
Ligero [1]	1	$\sqrt{\| C \|}$	$\| C \| log \| C \|$	$s log s + d log d$	RO	CRHF
Bootle et al. [10]	1	$\sqrt{\| C \|}$	$\| C \|$	$\| C \|$	RO	CRHF
Baum et al. [2]	$\sqrt{\| C \|}$	$\sqrt{\| C \| log \| C \|}$	$\| C \| log \| C \|$	$\| C \|$	CRS	SIS
zk-STARKs [4]	1	${log}^{2} \| C \|$	$\| C \| polylog (\| C \|)$	$polylog (\| C \|)$	RO	CRHF
Aurora [6]	1	${log}^{2} \| C \|$	$\| C \| log \| C \|$	$\| C \|$	RO	CRHF
Bulletproof [12]	$\| C \|$	$log \| C \|$	$\| C \|$	$\| C \| log \| C \|$	CRS + RO	DL
zk-SNARKs [7,23,52]	$\| C \|$	1	$\| C \| log \| C \|$	$\| c \|$	CRS	KE
This work	1	1	$\| C \|$	1	HW	Signature

Performance. The performance of our scriptable SNARK system is theoretically and experimentally evaluated and compared with the other NIZK proof systems. Table 1 illustrates the asymptotic efficiency comparison measured by the circuit size. $| C |$ is the circuit size; $| w |$ is the witness size; $| c |$ is the problem instance size; s is the number of copies of the subcircuits; d is the width of the subcircuits. As we can see, our construction can achieve constant CRS size, constant verifier’s complexity, and constant proof size. The prover’s complexity is also minimum, which is $| C |$ . Note that in theory, the verifier’s complexity cannot be sublinear to the statement size $| x |$ , but as a convention, it is ignored in the table.

In terms of the actual experimental performance. The prover’s running time for evaluating a Boolean circuit consisting of $2^{39}$ NAND gates only takes less than 10 mins, which is 900 times faster than the state of the art, zk-STARK, for circuits larger than $2^{35}$ gates. Note that this performance result is tested through Lua script, and native code for circuit evaluation is 10 times faster in our experiment. The verifier’s running time is merely a signature verification, which takes approximately 1.5 ms – better than all the other existing succinct NIZK systems. The proof size is 297 Bytes with current Intel SGX signature, where 256 Bytes are the signature. Hence, we envision it is possible to further reduce the proof size by replacing the signature scheme. The TrustZone based system uses ECDSA on the secp256k1 curve, so the proof size is only 32 Bytes.

1.4. Applications

Finally, we discuss applications of our scriptable SNARK. We note that, many applications have been previously investigated. However, it is very challenging to deploy them in practice due to the performance barrier.

Sound and scalable blockchain. As discussed at the very beginning of the Introduction, lots of heated discussions are taking place in blockchain community, with the goal of improving the performance in a sound manner. This consists of two parts. First, we should address the existing issues, since many blockchain scalability proposals have been implemented even the community is aware of the security concerns. In Section 7, we mention a few examples, and showcase how to address these issues via our SNARK. Again, we note that, these issues were not addressed simply due to the missing of fast and SNARK.

Second, we will enable new design paradigm for the interesting “one-to-many” unbalanced computation scenarios. Using our SNARK, typically, a single node as prover, can generate in very short time a proof that will convince all other nodes to accept the validity of the current state of the ledger, without requiring those nodes to naively re-execute the computation, nor to store the entire blockchain’s state, which would be required for such a naive verification.

Privacy preserving smart contracts. The zero-knowledge properties of ZK proofs has already been intensively used in blockchain projects, with the goal of ensuring the anonymity and protecting financial privacy. Notably, Succinct Non-interactive ARguments of Knowledge (zk-SNARK) has been used in Zcash and Ethereum; Bulletproofs has been used in Monaro. Recently, Ethereum has the plan to explore the feasibility zk-STARK in its future version of their platform. We note that, it is still not clear if zk-STARK can be widely adopted in blockchain platforms given the fact that, the current proof size is $1000 \times$ longer than zk-SNARKs. Fortunately, our SNARK is super succinct, and super fast. In Section 7, we demonstrate concrete examples.

2. Preliminaries

2.1. Trusted execution environment

Trusted execution environment (TEE) refers to a range of technologies that can establish an isolated and trusted environment where security sensitive data can be stored and processed with confidentiality and integrity guarantees. TEE needs to be instantiated on top of a trusted computing base (TCB), which consists of hardware, firmware and/or software. Minimizing the size (attack surface) of TCB with reasonable assumptions is the common goal of this line of research. In practice, TEE can be realized on top of several promising trusted hardware technologies, such as ARM TrustZone and Intel SGX. Although recently a few side-channel attacks, e.g. [42,56], have been explored against those TEE candidates, new designs and fixes are proposed on a monthly basis. Hence, we envision that TEE will be a cheap and acceptable assumption in the near future. In this work, our benchmarks are mainly based on the Intel SGX platform for its readily deployed remote attestation infrastructure; however, our technique can also be implemented on any other TEE solutions.

Intel SGX. Intel Software Guard Extensions (SGX) is a widely used trusted hardware solution to enable TEE. It provides a hardware enforced isolated execution environment against malicious OS kernels and supervisor software. The SGX processor sets aside an exclusive physical memory space, called processor reserved memory (PRM) to ensure the confidentiality and integrity of enclave’s memory. Each SGX hardware holds two root keys: root provisioning key and root seal key. The actual attestation keys are deviated from those root keys via PRF. Intel’s (anonymous) attestation is based on an anonymous group signature scheme called Intel Enhanced Privacy ID (EPID) [11]. In this work, we are particularly interested in SGX’s ability to enable attested computation, i.e. any third party can audit an outcome is computed by a pre-agreed program in a genuine SGX. More specifically, the application enclave first uses $EREPORT$ to generate a report for local attestation (identifying two enclaves are running on the same platform). The report is then sent to a special enclave called Quoting Enclave (QE) to produce a quote by signing the report with the group signature. In theory, given the group public key (and the up-to-date revocation list), any verifier can check the validity of the signed quote non-interactively; however, currently, one must contact the Intel Attestation Service (IAS) for verification. IAS will first verify the group signature and then create the corresponding attestation verification report with its own signature.

In practice, the security guarantee of SGX is evolving alone with the discovered side-channel attacks: cache-timing attacks [18], page-fault attacks [59], branch shadowing [39], synchronization bugs [58], foreshadow [56], and SgxPectre [16], etc. Subsequently, some privacy concerns are raised when SGX is involved in the data process. Hereby, we would like to emphasize that unlike most SGX applications, the security of our construction mainly relies on the computational integrity guaranteed by SGX rather than data confidentiality. Namely, the adversary is allowed to learn the enclave’s internal state during computation. As far as the root keys are not leaked, the soundness of our construction still holds. This relaxed assumption is modelled as transparent enclave in the literature [53].

TrustZone. As one of the most widely deployed security architectures to support TEE, ARM TrustZone separates a processor into two security states, namely the secure world and the normal world. And the resource (e.g., memory, peripherals) belonging to the secure world cannot be accessed by the normal world directly. The processor runs in either the normal world or the secure world at any given time. Switch between the two worlds is triggered by $SMC$ instruction. In this way, ARM TrustZone enables an isolated execution in the secure world. ARM TrustZone can also support attested computation by equipping each TrustZone-enabled device with a device-specific, asymmetric key pair that is signed by the device’s vendor. This has been implemented in real-world products (like Samsung Knox). Then by putting the pre-agreed program into the secure world, the system software of the secure world can leverage the private key of the key pair to sign the outcome from the pre-agreed program together with the identity information of the pre-agreed program. Theoretically, anyone can verify the signature of the signed data (outcome and identity information of the pre-agreed program) as long as he or she has the corresponding public key. But in practice, device vendors (like Samsung) tend to maintain an attestation server for signature verification purpose. After the signature passes the verification, the attestation server can generate the corresponding attestation report to indicate that the signed data is indeed produced by a trusted device source, just like what IAS does.

2.2. NIZK proof/argument systems

Let $R$ be a polynomial time decidable binary relation. We call x the statement and w the witness, if $(x, w) \in R$ . $L : = {x | \exists w : (x, w) \in R}$ is the NP language defined by $R$ . In a zero-knowledge (ZK) proof/argument system, the prover wants to convince one or more verifier(s) $x \in L$ , where $L$ is an arbitrary NP language. The ZK system is called non-interactive (NIZK) [8] if the prover can generate the proof without interacting with a verifier, and any verifier(s) can check the validity of the proof. However, it is not possible to realize a NIZK proof/argument system unless the language is in BPP in the plain model (a.k.a. standard model) [26]. To circumvent this impossibility result, all NIZK proof/argument systems must rely on some trusted setup assumptions, such as the common reference string model, random oracle model, and generic group model, etc. A NIZK system is called succinct if the proof size is asymptotically less than $| w | + | x |$ (cf. Section 3). Note that, a succinct NIZK proof of knowledge is also called a SNARK. Unfortunately, it is also shown in [24] that succinct NIZK proof/argument systems cannot be based on any falsifiable assumptions, i.e. an assumption that can be written as a game. That means one must embrace “strong assumptions” to enjoy the benefit of succinctness. In addition, many NIZK proof/argument systems have a so-called unbalanced property, where the verifier’s complexity is minimized (sometimes maybe at the cost of increasing the prover’s complexity). This property is desirable when the number of verifiers is large, such as the blockchain scenarios.

2.3. Universal composibility

Our model is based on the Universal Composibility (UC) framework [13,14], which lays down a solid foundation for designing and analyzing protocols secure against attacks in an arbitrary network execution environment (therefore it is also known as network aware security model). Roughly speaking, in the UC framework, protocols are carried out over multiple interconnected machines; to capture attacks, a network adversary $A$ is introduced, which is allowed to corrupt some machines (i.e., have the full control of all physical parts of some machines); in addition, $A$ is allowed to partially control the communication tapes of all uncorrupted machines, that is, it sees all the messages sent from and to the uncorrupted machines and controls the sequence in which they are delivered. Then, a protocol Π is a UC-secure implementation of a functionality $F$ , if it satisfies that for every network adversary $A$ attacking an execution of Π, there is another adversary $S$ —known as the simulator—attacking the ideal process that uses $F$ (by corrupting the same set of machines), such that, the executions of Π with $A$ and that of $F$ with $S$ makes no difference to any network execution environment $Z$ .

The ideal world execution. In the ideal world, the set of parties $P : = {P_{1}, \dots, P_{n}}$ only communicate with an ideal functionality $F$ and the simulator $S$ during the execution. In this ideal world, the corrupted parties are controlled by the simulator $S$ . The output of the environment $Z$ in this execution is denoted by $Exe c_{F, S, Z}$ .

The real world execution. In the real world, the set of parties $P : = {P_{1}, \dots, P_{n}}$ communicate with each other and the adversary $A$ to run the protocol Π. In this real world, the corrupted parties are controlled by the adversary $A$ . The output of the environment $Z$ in this execution is denoted by ${Exec}_{Π, A, Z}$ .

Definition 1.
We say protocol Π UC-secure realizes functionality $F$ if for all PPT adversaries $A$ there exists a PPT simulator $S$ such that for all PPT environment $Z$ it holds: $\begin{matrix} {Exec}_{Π, A, Z} \approx Exe c_{F, S, Z} \end{matrix}$

In order to conceptually modularize the design of the protocols, the notion of “hybrid models” is often introduced in the UC framework. A protocol Π is said to be realized “in the $O$ -hybrid model” if Π invokes the ideal functionality $O$ as a subroutine.
Definition 2.
We say protocol Π UC-secure realizes functionality $F$ in the $O$ -hybrid world if for all PPT adversaries $A$ there exists a PPT simulator $S$ such that for all PPT environment $Z$ it holds: $\begin{matrix} {Exec}_{Π, A, Z}^{O} \approx Exe c_{F, S, Z} \end{matrix}$

The UC model provides strong security guarantees (via polynomial-time security reduction). It also has two appealing features: The property that stand-alone security directly implies security under general concurrent composition (thus protocols only need to be analyzed in a stand-alone fashion), and its support for modular analysis of protocols.
2.4. Cryptographic tools

We need the following cryptographic tools to build our protocols.

Digital signature. A digital signature $DS$ is a mathematical scheme for verifying the authenticity of digital messages or documents. Formally, the digital signature scheme $DS$ has the following algorithms:

$(PK, SK) \leftarrow DS . KeyGen (1^{λ})$ . It is the key generation algorithm that takes input as the security parameter λ and outputs a public key $PK$ and a signature key $SK$ .

$σ \leftarrow DS . Sign (SK, m)$ . It is the signature algorithm that takes input as the signature key $SK$ and a message m. It outputs a signature σ.

$b \leftarrow DS . Verify (PK, m, σ)$ . It is the verification algorithm that takes input as the public key $PK$ , a message m and a signature σ. It outputs a bit b indicating accpetance $(b = 1)$ or rejection $(b = 0)$ .

The security notion required for digital signature is existential unforgeability under chosen message attacks, and we capture it by the following definition.

Definition 3.
We say the digital signature $DS$ is EUF-CMA secure if for any PPT adversary $A$ , the probability of winning the following game $\Pr [{Succ}_{A}^{DS}]$ is ngeligible
$A$ interacts with a challenger, denoted as $Ch$ ;

$Ch$ runs $(PK, SK) \leftarrow DS . KeyGen (1^{λ})$ , and hands the public key $PK$ to $A$ ;

For $i \in [n]$ : $A$ sends the message $m_{i}$ to $Ch$ , $Ch$ runs $σ_{i} \leftarrow DS . Sign (SK, m_{i})$ and sends $σ_{i}$ back. Here n is set by $A$ .

$A$ forges a new message/signature pair $(m^{'}, σ^{'})$ and sends it to $Ch$ . Then $Ch$ checks $m^{'} \notin {m_{i}}_{i = 1}^{n}$ and $DS . Verify (PK, m^{'}, σ^{'}) = 1$ . If both checks pass, $A$ wins.
Here we define the advantage of an adversary $A$ as ${Adv}_{A}^{DS} (1^{λ}) = \Pr [{Succ}_{A}^{DS}]$ .

Message authentication code. A message authentication code (MAC) is another cryptographic scheme that used to authenticate the origin and nature of a message. It is similar with digital signature, but uses symmetric encryption. A MAC scheme has the following algorithms:

$K \leftarrow MAC . KeyGen (1^{λ})$ . It is the key generation algorithm that takes input as the security parameter λ and outputs the secret key $K$ .

$t \leftarrow MAC . Sign (K, m)$ . It is the signing algorithm that takes input as the secret key $K$ and a message m. It outputs a MAC tag t.

$b \leftarrow MAC . Verify (K, m, t)$ . It is the verification algorithm that takes input as the secret key $K$ , a message m and a MAC tag t. It outputs a bit b indicating accpetance $(b = 1)$ or rejection $(b = 0)$ .

The security notion required for MAC is the same as digital signature, and we also capture it by the following definition.
Definition 4.
We say the digital signature $MAC$ is EUF-CMA secure if for any PPT adversary $A$ , the probability of winning the following game $\Pr [{Succ}_{A}^{MAC}]$ is ngeligible
$A$ interacts with a challenger, denoted as $Ch$ ;

$Ch$ runs $K \leftarrow MAC . KeyGen (1^{λ})$ ;

For $i \in [n]$ : $A$ sends the message $m_{i}$ to $Ch$ , $Ch$ runs $t_{i} \leftarrow MAC . Sign (K, m_{i})$ and sends $t_{i}$ back. Here n is set by $A$ .

$A$ forges a new message/tag pair $(m^{'}, t^{'})$ and sends it to $Ch$ . Then $Ch$ checks $m^{'} \notin {m_{i}}_{i = 1}^{n}$ and $MAC . Verify (K, m^{'}, t^{'}) = 1$ . If both checks pass, $A$ wins.
Here we define the advantage of an adversary $A$ as ${Adv}_{A}^{MAC} (1^{λ}) = \Pr [{Succ}_{A}^{MAC}]$ .

Collision-resistant hash function. A hash function $hash$ is collision resistant if it is hard to find two preimages that hash to the same image, that is, two preimages $a, b$ such that $hash (a) = hash (b)$ . Formally, we capture the collision resistant property by the following definition. Definition 5.
We say the hash function $hash$ is collision resistant if for any PPT adversary $A$ , the probability of winning the following game $\Pr [{Succ}_{A}^{hash}]$ is ngeligible
$A$ interacts with a challenger, denoted as $Ch$ ;

$A$ finds a preimage pair $(a, b)$ and sends it to $Ch$ . Then $Ch$ checks $a \neq b$ and $hash (a) = hash (b)$ . If both checks pass, $A$ wins.
Here we define the advantage of an adversary $A$ as ${Adv}_{A}^{hash} (1^{λ}) = \Pr [{Succ}_{A}^{hash}]$ .

3. Security definition

In this section, we formally define the scriptable SNARK. Our definition is through an ideal functionality $F_{S SNARK}^{Q}$ . In addition, we present a setup functionality $O_{HW}^{Q}$ . We note that the two functionalities will be realized in Section 4 and instantiated in Section 6, respectively.

Fig. 1.

The scriptable functionality $F_{S SNARK}^{Q}$ .

Scriptable SNARK ideal functionality. The scriptable SNARK ideal functionality $F_{S SNARK}^{Q}$ is depicted in Fig. 1. The functionality is parameterized by a predicate $Q$ . The functionality $F_{S SNARK}^{Q}$ allows the prover to obtain a proof π if $Q (C, {Input}_{pub}, {Input}_{priv}, Output) = 1$ and $C ({Input}_{pub}, {Input}_{priv}) = Output$ , where $Q$ is a predicate. Once a proof π is generated, it will always is verified. Notice that the proof π is generated without the knowledge of the private input ${Input}_{priv}$ ; therefore, the proof generated by $F_{S SNARK}^{Q}$ has the conventional zero-knowledge. Since $F_{S SNARK}^{Q}$ must obtain a private input ${Input}_{priv}$ such that $C ({Input}_{pub}, {Input}_{priv}) = Output$ before recording a proof π. Hence, $F_{S SNARK}^{Q}$ also capture the (knowledge) soundness property. In addition, the scriptable property is reflected by the predicate $Q$ , which restricts the class of functions that $F_{S SNARK}^{Q}$ supports. For instance, $Q$ could be the total execution steps is less than a certain bound.

The functionality $F_{S SNARK}^{Q}$ interacts with a set of players $P : = {P_{1}, \dots, P_{n}}$ as well as ideal adversary $S$ . To generate a proof π, the prover needs to submit the command $(P ROVE, sid, ssid, ⟨ C, {Input}_{pub}, {Input}_{priv}, Output ⟩)$ to $F_{S SNARK}^{Q}$ . After checking the validity, $F_{S SNARK}^{Q}$ will inform the adversary $S$ using command $(P ROVE, sid, ssid, P_{i}, C, {Input}_{pub}, Output)$ . If the adversary $S$ allows, he/she will then send the proof π to $F_{S SNARK}^{Q}$ . $F_{S SNARK}^{Q}$ records the message $⟨ C, {Input}_{pub}, Output, π ⟩$ and returns it to the requestor. To verify a proof π, the functionality $F_{S SNARK}^{Q}$ first checks if the tuple $⟨ C, {Input}_{pub}, Output, π ⟩$ is recorded. If not, which means the proof is not generated by the functionality itself, then $F_{S SNARK}^{Q}$ asks the adversary $S$ for the private input. Once a private input ${Input}_{priv}$ is submitted, $F_{S SNARK}^{Q}$ checks $Q (C, {Input}_{pub}, {Input}_{priv}, Output) = 1$ and $C ({Input}_{pub}, {Input}_{priv}) = Output$ . If it is the case, $F_{S SNARK}^{Q}$ records the tuple $(C, {Input}_{pub}, Output, π)$ , and the proof is accepted.

Remark on succinctness. We say a NIZK proof system is succinct if the size of the proof $| π | = poly (λ) {(| x | + | w |)}^{o (1)}$ .

Fig. 2.

The $Q$ -compliant trusted hardware functionality $O_{HW}^{Q}$

$Q$ -compliant trusted hardware model. Our scheme is built in the $Q$ -compliant trusted hardware model ( $Q$ -HW model), where $Q$ is a predicate that specifies the class of functions that the hardware is allowed to compute. In the $Q$ -HW model, all parties have access to an ideal functionality $O_{HW}^{Q}$ , which on input queries, executes a given $Q$ -compliant function and returns the execution results. The predicate $Q$ depends on the setup, which may vary from protocol to protocol. In this work, we abstract our requirement as the functionality $O_{HW}^{Q}$ (cf. Fig. 2). As will be shown in Section 6 later, it can be instantiated from programmable trusted execution environment (TEE) solutions, e.g., Intel SGX or TrustZone. The $O_{HW}^{Q}$ functionality is parameterized with a predicate $Q$ and a digital signature scheme, denoted $DS : = (KeyGen, Sign, Verify)$ . $O_{HW}^{Q}$ can be initialized once by sending the $(I NIT, sid)$ command to it. It then generates $(PK, SK) \leftarrow DS . KeyGen (1^{λ})$ and record $(sid, PK, SK)$ . After initialization, anyone can query the public key $PK$ using the $G ET PK$ command. Anyone can then send $(C OMPUTE, sid, ssid, C, {Input}_{pub}, {Input}_{priv})$ request to the functionality $O_{HW}^{Q}$ , where $C$ is the polynomial-time algorithm, ${Input}_{pub}$ is the public input, and ${Input}_{priv}$ is the private input. The functionality first computes $C ({Input}_{pub}, {Input}_{priv}) = y$ and then asserts $Q (C, {Input}_{pub}, {Input}_{priv}, y) = 1$ ; it then returns $(y, σ)$ , where the signature $σ \leftarrow DS . Sign (SK, ⟨ ssid, C, {Input}_{pub}, y ⟩)$ . Note that the private input is not signed.

4. Our scriptable SNARK construction

In this section, we present our scriptable SNARK construction in the $O_{HW}$ -hybrid world. Before presenting our intuition and construction, we first set up the context for scriptable SNARK.

Common information. Unlike most existing SNARK proof systems, the script $C$ (or language $L$ to be proven) is not hardcoded in the prover and verifier executable files. Our scriptable SNARK proof system allows the users to configure the language instance. This implicitly assumes that the prover and the verifier(s) have some common information in addition to the statement x before the protocol execution. For instance, they all know the description of the NP language $L$ , which is usually represented by its polynomial decidable binary relation $R$ . Without loss of generality, for a relation $R$ , we assume there exists an efficiently computable algorithm $C_{R}$ such that $C_{R} (x, w) = 1$ if $(x, w) \in R$ and otherwise $C_{R} (x, w) = 0$ . $C_{R}$ is the common public input to both the prover and the verifier. Depending on the concrete implementation, different SNARK proof systems use different $C_{R}$ representation; most popular SNARK proof systems use arithmetic circuit representation, while some, e.g. [5], allows more developer-friendly representations, e.g., in C programming language. Although, in principle, one can convert any RAM model program into a circuit representation, this transform imposes $O (log n)$ overhead.

Intuition. Trusted hardware offers two important features: (i) data confidentiality and (ii) computation integrity. Most existing trusted hardware (TEE) based applications, e.g., [22] mainly explore the data confidentiality aspect; whereas, in this project, we emphasize the computation integrity aspect. Recall that in a NIZK proof, the prover and the verifier have common input $(C_{R}, {Input}_{pub} : = x)$ . The potentially malicious prover wants to convince the verifiers that he/she knows a witness ${Input}_{priv} : = w$ such that $C_{R} ({Input}_{pub}, {Input}_{priv}) = 1$ . Since the trusted hardware can guarantee computation integrity even when the host is malicious, we can let $O_{HW}^{Q}$ to execute the relationship decision algorithm $b \leftarrow C_{R} (x, w)$ and sign the output b. To bind the decision algorithm and statement, we let $O_{HW}^{Q}$ signs $(C_{R}, x, b)$ without revealing the witness w. Therefore, by checking the signature, the verifier is convinced that the prover must know a witness w such that $C_{R} (x, w) = 1$ if $(C_{R}, x, 1)$ is signed by $O_{HW}^{Q}$ . Similarly, for general computation, the private input ${Input}_{priv}$ is not signed; therefore, zero-knowledge property is preserved even if the signature leaks the signed message.

What is the difference between the above SNARK construction and trusted computation in the $O_{HW}^{Q}$ functionality setting? Recall that SNARK proofs are typically deployed in a one-to-many scenario, so the prover only needs to invoke the $O_{HW}^{Q}$ once and many verifiers can check the validity of the proof; on the contrary, the other existing TEE based trusted computation applications mostly focus on one-to-one setting. Our $crs$ is just the public key of $O_{HW}^{Q}$ .

Construction. Our scriptable SNARK construction utilizes the $Q$ -compliant hardware functionality $O_{HW}^{Q}$ as defined in Fig. 2.

Fig. 3.

The scriptable SNARK protocol $Π_{S SNARK}^{Q}$ in the $O_{HW}^{Q}$ -hybrid model.

We aim to achieve constant verification time; light-weight device can perform the verification. In addition, the verifier is only required to query the $O_{HW}^{Q}$ functionality once to obtain the public key $PK$ ; when $PK$ has already been fetched, the verification can be executed offline. As depicted in Fig. 3, our scriptable SNARK proof protocol $Π_{S SNARK}^{Q}$ uses a digital signature scheme $DS : = (KeyGen, Sign, Verify)$ as its building block. At the beginning of the protocol, the hardware functionality needs to be initialized. In Fig. 3, this step is performed by the prover (marked in grey) if it is not done yet. The prover then asserts $Q (C, {Input}_{pub}, {Input}_{priv}, Output) = 1$ and $C ({Input}_{pub}, {Input}_{priv}) = Output$ ; it sends $(C OMPUTE, sid, ssid, C, {Input}_{pub}, {Input}_{priv})$ to $O_{HW}^{Q}$ and obtains $(C OMPUTE, sid, ssid, ⟨ Output, σ ⟩)$ from $O_{HW}^{Q}$ . σ is the proof.

To verify a proof π, the verifier needs to know the public key $PK$ . This step can be performed by a trusted setup, and $PK$ is published as the common reference string. Otherwise, the verifier can query $O_{HW}^{Q}$ to fetch it (marked in grey). In the verification phase, the verifier $V$ accepts the proof if $DS . Verify (PK, ⟨ ssid, C, {Input}_{pub}, Output ⟩, σ) = 1$ .

Security. We show the security of our succinct scriptable SNARK construction via Thm. 1, below.

Theorem 1.

Assume signature scheme $DS : = (KeyGen, Sign, Verify)$ is EUF-CMA secure with adversarial advantage ${Adv}_{A}^{DS} (1^{λ})$ . The scriptable NIZK protocol $Π_{S SNARK}^{Q}$ described in Fig. 3 , UC-realizes the $F_{S SNARK}^{Q}$ functionality depicted in Fig. 1 in the $O_{HW}^{Q}$ -hybrid world against static malicious corruption with adversarial advantage ${Adv}_{A}^{DS} (1^{λ})$ .

Proof.

To prove the theorem, we construct a simulator $S$ such that no non-uniform $PPT$ environment $Z$ can distinguish between (i) the real execution ${Exec}_{Π_{S SNARK}^{Q}, A, Z}^{O_{HW}^{Q}}$ where the parties $P : = {P_{1}, \dots, P_{n}}$ run protocol $Π_{S SNARK}^{Q}$ in the $O_{HW}^{Q}$ -hybrid world and the corrupted parties are controlled by a dummy adversary $A$ who simply forwards messages from/to $Z$ , and (ii) the ideal execution ${Exec}_{F_{S SNARK}^{Q}, S, Z}$ where the parties interact with functionality $F_{S SNARK}^{Q}$ and corrupted parties are controlled by the simulator $S$ . We consider following cases.

Case 1: The prover $P_{i}$ is corrupted.

Simulator. The simulator $S$ internally runs $A$ , forwarding messages to/from the environment $Z$ . The simulator $S$ simulates honest verifier $P_{j}$ and the functionality $O_{HW}^{Q}$ . In addition, the simulator $S$ simulates the following interactions with $A$ .

∘ When the simulated $O_{HW}^{Q}$ receives the incoming message $(C OMPUTE, sid, ssid, ⟨ C, {Input}_{pub}, {Input}_{priv} ⟩)$ from $P_{i}$ , $S$ computes $C ({Input}_{pub}, {Input}_{priv}) = Output$ and checks if $Q (C, {Input}_{pub}, {Input}_{priv}, Output) = 1$ . If it is the case, $S$ acts as $P_{i}$ to send $(P ROVE, sid, ssid, ⟨ C, {Input}_{pub}, {Input}_{priv}, Output ⟩)$ to $F_{S SNARK}^{Q}$ . Upon receiving $(P ROVE, sid, ssid, ⟨ P_{i}, C, {Input}_{pub}, Output ⟩)$ from $F_{S SNARK}^{Q}$ , $S$ replies $(P ROVE, sid, ssid, σ)$ to $F_{S SNARK}^{Q}$ , where $σ \leftarrow DS . Sign (SK, ⟨ ssid, C, {Input}_{pub}, Output ⟩)$ is the signature generated by the simulated $O_{HW}^{Q}$ functionality.

∘ Upon receiving $(V ERIFY, sid, ssid, ⟨ P_{j}, C, {Input}_{pub}, Output, π ⟩)$ from functionality $F_{S SNARK}^{Q}$ , the simulator $S$ checks the internal state (the view) of the simulated $O_{HW}^{Q}$ , if the command $(C OMPUTE, sid, ssid, ⟨ C, {Input}_{pub}, {Input}_{priv} ⟩)$ has been queried to $O_{HW}^{Q}$ before, it checks if the generated signature $σ \leftarrow DS . Sign (SK, ⟨ ssid, C, {Input}_{pub}, Output ⟩)$ is the same as π. If not, aborts. Otherwise, $S$ returns ${Input}_{priv}$ to $F_{S SNARK}^{Q}$ .

Indistinguishability. The indistinguishability is proven through a series of hybrid worlds $H_{1}, H_{2}$ .

Hybrid $H_{1}$ : It is the real protocol execution ${Exec}_{Π_{S SNARK}^{Q}, A, Z}^{O_{HW}^{Q}}$ .

Hybrid $H_{2}$ : $H_{2}$ is the same as $H_{1}$ except that in $H_{2}$ , if the proof π is not the same as the simulated signature σ, $S$ aborts. Lemma 1.

If $DS$ is a EUF-CMA secure digital signature scheme with adversarial advantage ${Adv}_{A}^{DS} (1^{λ})$ , then $H_{4}$ and $H_{3}$ are indistinguishable with advantage $ϵ = {Adv}_{A}^{DS} (1^{λ})$ .

Proof.

The simulator $S$ aborts when the prover can generate an accepting proof without querying the functionality $O_{HW}^{Q}$ . If there exists an adversary $A$ who can generate an accepting proof without querying $O_{HW}^{Q}$ , then we can construct an adversary $B$ who can break the EUF-CMA security game of the underlying digital signature scheme $DS$ . Indeed, since $O_{HW}^{Q}$ is always trusted, the only way an adversary $A$ can produce an accepting proof is to forge a signature. During the reduction, $B$ simulates the $O_{HW}^{Q}$ as follows. Up on receiving query $(C OMPUTE, sid, ssid, C, {Input}_{pub}, {Input}_{priv})$ , $B$ computes $C ({Input}_{pub}, {Input}_{priv}) = Output$ and checks if $Q (C, {Input}_{pub}, {Input}_{priv}, Output) = 1$ . It then queries the EUF-CMA game challenger to sign $⟨ ssid, C, {Input}_{pub}, Output ⟩$ . After receiving the signature σ from the challenger, $B$ forwards it to $A$ . When $A$ outputs $(V ERIFY, sid, ssid, ⟨ C^{*}, {Input}_{pub}^{*}, {Output}^{*}, π^{*} ⟩)$ such that the verification passes. $B$ outputs $(m^{*} : = ⟨ ssid, C^{*}, {Input}_{pub}^{*}, {Output}^{*} ⟩, σ^{*} : = π^{*})$ as the forged message signature pair. Clearly, $B$ wins whenever $A$ wins.

Therefore, the overall advantage is ${Adv}_{A}^{DS} (1^{λ})$ . □

The adversary’s view of $H_{2}$ is identical to the ideal execution ${Exec}_{F_{S SNARK}^{Q}, S, Z}$ . Therefore, the overall distinguishing advantage is ${Adv}_{A}^{DS} (1^{λ})$ .

Case 2: The verifier $P_{j}$ is corrupted.

Simulator. Similar to Case 1, the simulator $S$ internally runs $A$ , forwarding messages to/from the environment $Z$ . The simulator $S$ simulates honest prover $P_{i}$ and the functionality $O_{HW}^{Q}$ . In addition, the simulator $S$ simulates the following interactions with $A$ .

∘ When the simulated $O_{HW}^{Q}$ receives $(C OMPUTE, sid, ssid, ⟨ C, {Input}_{pub}, {Input}_{priv} ⟩)$ from $P_{i}$ , the simulator $S$ acts as $O_{HW}^{Q}$ to generate the corresponding signature $σ \leftarrow DS . Sign (SK, ⟨ ssid, C, {Input}_{pub}, Output ⟩)$ and return $(C OMPUTE, sid, ssid, ⟨ Output, σ ⟩)$ to $P_{i}$ .

Indistinguishability. The indistinguishability is straightforward. The proof π generated by the simulator $S$ has identical distribution to the proof in the real protocol execution ${Exec}_{Π_{S SNARK}^{Q}, A, Z}^{O_{HW}^{Q}}$ . This is because both proofs are the signatures generated as $DS . Sign (SK, ⟨ ssid, C, {Input}_{pub}, Output ⟩)$ , and the private input is not needed to generate a signature. Moreover, the honest prover first checks the validity of the predicate $Q (C, {Input}_{pub}, {Input}_{priv}, Output) = 1$ and the correctness of the computation output $C ({Input}_{pub}, {Input}_{priv}) = Output$ before querying $O_{HW}^{Q}$ ; therefore, the $Q$ -compliance is guaranteed, despite the fact that $O_{HW}^{Q}$ does not know ${Input}_{priv}$ .

Case 3: Both the prover $P_{i}$ and the verifier $P_{j}$ are corrupted.

Simulator. Trivial case. There is nothing needs to extract, as the trustees do not have input. The simulator $S$ just run trustee according to protocol $Π_{S SNARK}^{Q}$ .

Indistinguishability. The view of $Z$ in the ideal execution ${Exec}_{F_{S SNARK}^{Q}, S, Z}$ has identical distribution to the view of $Z$ in the real execution ${Exec}_{Π_{S SNARK}^{Q}, A, Z}^{O_{HW}^{Q}}$ .

This concludes the proof. □

5. A lightweight SNARK scheme for trusted hardware with limited state

The hardware functionality $O_{HW}^{Q}$ as described in Fig. 2 requires the trusted hardware to have large enough state that linearly depends in the size of the statement $| x |$ and/or the size of the witness $| w |$ ; moreover, typically, we want to hardware to be programable. Unfortunately, there are very few products that can fulfill this requirement, which limits the realization choices of our scheme. In this section, we propose another scheme that can work with trusted hardware with $(Θ (λ))$ -size state.

Intuition. Our previous approach is to send the entire circuit $C$ directly to the trusted hardware. A natural approach to minimizing the hardware state requirement is to disassemble the circuit $C$ into gates, and we feed the hardware k gates at a time, where k is a small constant. However, this would lead to new problems: (i) the trusted hardware with limited state is still not able to load the entire statement x at once; (ii) how to prevent a malicious prover from changing the structure of $C$ and/or wire assignments.

Our solution is to utilize a collision-resistant hash function $hash$ and the message authentication code (MAC) scheme $MAC : = (KeyGen, Sign, Verify)$ . To address the first problem, we send the hash of the statement $h_{x} \leftarrow hash ({Input}_{pub}), h_{o} \leftarrow hash (Output)$ instead of the statement ${Input}_{pub}, Output$ itself. In this way, we reduce the size of the input. Meanwhile we re-define the relation $R^{'} : C ({Input}_{pub}, {Input}_{priv}) = Output \land h_{x} = hash (x); \land h_{o} = hash (Output)$ . Without loss of generality, for a relation $R^{'}$ , we assume there exists an efficiently computable algorithm $C_{R^{'}}$ such that $C_{R^{'}} ((h_{x}, h_{o}), ({Input}_{pub}, {Input}_{priv}, Output)) = 1$ if $C ({Input}_{pub}, {Input}_{priv}) = Output \land h_{x} = hash (x); \land h_{o} = hash (Output)$ and otherwise $C_{R^{'}} ((h_{x}, h_{o}), ({Input}_{pub}, {Input}_{priv}, Output)) = 0$ . We assume that $C_{R^{'}}$ is made of identity gates (for input only) and NAND gates. For such $C_{R^{'}}$ , we assume it is easy to find a DPT algorithm $Convert$ which takes $C, {Input}_{pub}, Output$ as input and outputs $L : = {L_{i}}_{i = 1}^{n}$ , where L is the description of $C_{R^{'}}$ , n is the number of the gates and we assume that $k | n$ . To be specific, the first $n_{1}$ items of L are used to describe the identity gates, that is ${ID α_{i}, γ_{i}}$ , where $α_{i}$ is the input wire of i-th indentity gate while $γ_{i}$ is the output wire and we assume that $k | n_{1}$ . The rest $n - n_{1}$ items are used to describe the NAND gates, that is ${NAND α_{i}, β_{i}, γ_{i}}$ , where $α_{i}, β_{i}$ are the input wires of i-th NAND gate while $γ_{i}$ is the output wire. To address the second problem, we use hash chains to guarantee the integrity of L. We set $h_{L} : = 0$ at first, and update $h_{L}$ by $h_{L} \leftarrow hash (h_{L}, {L_{k (i - 1) + j}}_{j = 1}^{k}, i)$ for $i \in [\frac{n}{k}]$ . And the prover should send $⟨ h_{x}, h_{o}, h_{L}, n ⟩$ at the very beginning.

To prevent the malicious prover from changing the assignment of wires, take NAND gates as an example, the prover has to send the description of the NAND gate $(α_{i}, β_{i}, γ_{i})$ , the assignment of input wires $x_{α_{i}}, x_{β_{i}}$ along with their MACs $t_{α_{i}}, t_{β_{i}}$ . The trusted hardware needs to check $MAC . Verify (K, ⟨ α_{i}, x_{α_{i}} ⟩, t_{α_{i}}) = 1$ and $MAC . Verify (K, ⟨ β_{i}, x_{β_{i}} ⟩, t_{β_{i}}) = 1$ first, where $K \leftarrow MAC . KeyGen (1^{λ})$ . After executing NAND operation $x_{γ_{i}} \leftarrow NAND (x_{α_{i}}, x_{β_{i}})$ , the trusted hardware computes $t_{γ_{i}} \leftarrow MAC . Sign (K, ⟨ γ_{i}, x_{γ_{i}} ⟩)$ , and return $(x_{γ_{i}}, t_{γ_{i}})$ .

The lightweight trusted hardware model. Now we provide our new functionality $O_{HW}^{Light}$ in Fig. 4. It is parameterized with a digital signature scheme $DS : = (KeyGen, Sign, Verify)$ , a MAC scheme $MAC : = (KeyGen, Sign, Verify)$ , and a hash function $hash$ . It maintains a temporary variable $temp$ and a counter $ctr$ which are both initialized as 0.

$O_{HW}^{Light}$ can be initialized once by sending the $(I NIT, sid)$ command to it. It then generates $(PK, SK) \leftarrow DS . KeyGen (1^{λ})$ , $K \leftarrow MAC . KeyGen (1^{λ})$ and record $(sid, PK, SK, K)$ . After initialization, anyone can query the public key $PK$ using the $G ET PK$ command. Anyone, we suppose it is $P_{i}$ , can then send $(C OMPUTE, sid, ⟨ h_{x}, h_{o}, h_{L}, n ⟩)$ request to the functionality $O_{HW}^{Light}$ , where $h_{x} \leftarrow hash ({Input}_{pub}), h_{o} \leftarrow hash (Output)$ , $h_{L}$ is the final output of the hash chain $h_{L} \leftarrow hash (h_{L}, L_{i}, i)$ for $i \in [n]$ , and n is the number of gates. $O_{HW}^{Light}$ records the tuple $⟨ sid, ssid, P_{i}, h_{x}, h_{o}, h_{L}, n ⟩$ for later use. Then $P_{i}$ can send $(I D, sid, ssid, {⟨ α_{k u + j}, γ_{k u + j} ⟩, x_{α_{k u + j}}}_{j = 1}^{k})$ and $(N AND, sid, ssid, {⟨ α_{k u + j}, β_{k u + j}, γ_{k u + j} ⟩, ⟨ x_{α_{k u + j}}, t_{α_{k u + j}}, x_{β_{k u + j}}, t_{β_{k u + j}} ⟩}_{j = 1}^{k})$ to $O_{HW}^{Light}$ . For $I D$ command, $O_{HW}^{Light}$ simply sets $x_{γ_{k u + j}} \leftarrow x_{α_{k u + j}}$ , signs $t_{γ_{k u + j}} \leftarrow MAC . Sign (K, ⟨ ssid, γ_{k u + j}, x_{γ_{k u + j}} ⟩)$ , and returns ${⟨ x_{γ_{k u + j}}, t_{γ_{k u + j}} ⟩}_{j = 1}^{k}$ . For $N AND$ command, $O_{HW}^{Light}$ checks $MAC . Verify (K, ⟨ ssid, α_{k u + j}, x_{α_{k u + j}} ⟩, t_{α_{k u + j}}) = 1$ and $MAC . Verify (K, ⟨ ssid, β_{k u + j}, x_{β_{k u + j}} ⟩, t_{β_{k u + j}}) = 1$ . Then it computes $x_{γ_{k u + j}} \leftarrow NAND (x_{α_{k u + j}}, x_{β_{k u + j}})$ , signs $x_{γ_{k u + j}} \leftarrow NAND (x_{α_{k u + j}}, x_{β_{k u + j}})$ , and returns ${⟨ x_{γ_{k u + j}}, t_{γ_{k u + j}} ⟩}_{j = 1}^{k}$ . For both commands, $O_{HW}^{Light}$ updates $h_{L} \leftarrow hash (h_{L}, {L_{k (i - 1) + j}}_{j = 1}^{k}, i)$ and increases $ctr \leftarrow ctr + 1$ . If $temp = h_{L}$ , $ctr = \frac{n}{k}$ and $x_{γ_{n}} = 1$ hold, it means $O_{HW}^{Light}$ has already verified the whole cirucit. $O_{HW}^{Light}$ then returns σ, where $σ \leftarrow DS . Sign (SK, ⟨ ssid, h_{x}, h_{o}, h_{L}, n ⟩)$ . Note that the private input is not signed.

Fig. 4.

The lightweight trusted hardware functionality $O_{HW}^{Light}$ .

The lightweight scriptable SNARKs construction. Our lightweight scriptable SNARKs construction utilizes the lightweight hardware functionality $O_{HW}^{Light}$ as defined in Fig. 4.

As depicted in Fig. 5, our lightweight scriptable SNARK protocol $Π_{S SNARK}^{Q, Light}$ uses a digital signature scheme $DS : = (KeyGen, Sign, Verify)$ and hash function $hash$ as its main building block. At the beginning of the protocol, the hardware functionality needs to be initialized, and this step is performed by the prover (marked in grey) if it is not done yet. The prover asserts $C ({Input}_{pub}, {Input}_{priv}) = Output$ and $Q (C, {Input}_{pub}, {Input}_{priv}, Output) = 1$ . Note that, the predicate $Q$ here restricts the class of the relation $R^{'} : C ({Input}_{pub}, {Input}_{priv}) = Output \land h_{x} = hash (x); \land h_{o} = hash (Output)$ , that is, $R^{'}$ should be able to be converted to a circuit of polynomial gates. Then the prover computes $h_{x} \leftarrow hash ({Input}_{pub}), h_{o} \leftarrow hash (Output)$ and generates $L \leftarrow Convert (C, {Input}_{pub})$ , where $L : = {L_{j}}_{j = 1}^{n}$ . After that, the prover sets $h_{L} : = 0$ , and updates $h_{L} \leftarrow hash (h_{L}, {L_{k (i - 1) + j}}_{j = 1}^{k}, i)$ for $i \in [\frac{n}{k}]$ . The prover sends $(C OMPUTE, sid, ssid, ⟨ h_{x}, h_{o}, h_{L}, n ⟩)$ to $O_{HW}^{Light}$ , and then sends $(I D, sid, ssid, {⟨ α_{k u + j}, γ_{k u + j} ⟩, x_{α_{k u + j}}}_{j = 1}^{k})$ for identity gates and $(N AND, sid, ssid, {⟨ α_{k u + j}, β_{k u + j}, γ_{k u + j} ⟩, ⟨ x_{α_{k u + j}}, t_{α_{k u + j}}, x_{β_{k u + j}}, t_{β_{k u + j}} ⟩}_{j = 1}^{k})$ for NAND gates. Finally, the prover obtains $(F INISH, sid, ssid, σ)$ from $O_{HW}^{Light}$ , where σ is the proof.

To verify a proof π, the verifier needs to know the public key $PK$ . This step can be performed by a trusted setup, and $PK$ is published as the common reference string. Otherwise, the verifier can query $O_{HW}^{Light}$ to fetch it (marked in grey). In the verification phase, the verifier should computes $h_{x}, h_{o}$ and $h_{L}$ as the prover does, and then accepts the proof if $DS . Verify (PK, ⟨ ssid, h_{x}, h_{o}, h_{L}, n ⟩, σ) = 1$ .

Fig. 5.

A Lightweight Scriptable SNARK Protocol $Π_{S SNARK}^{Q, Light}$ in the $O_{HW}^{Light}$ -hybrid model.

Security. We show the security of our lightweight scriptable SNARK construction via Thm. 2, below.

Theorem 2.

Assume the signature scheme $DS : = (KeyGen, Sign, Verify)$ and the MAC scheme $MAC : = (KeyGen, Sign, Verify)$ are EUF-CMA secure with adversarial advantage ${Adv}_{A}^{DS} (1^{λ})$ and ${Adv}_{A}^{MAC} (1^{λ})$ respectively, and the hash function $hash$ is collision resistant with adversarial advantage ${Adv}_{A}^{hash} (1^{λ})$ . The scriptable SNARK protocol $Π_{S SNARK}^{Q, Light}$ described in Fig. 5 , UC-realizes the $F_{S SNARK}^{Q}$ functionality depicted in Fig. 1 in the $O_{HW}^{Light}$ -hybrid world against static malicious corruption with adversarial advantage $\begin{matrix} {Adv}_{A}^{MAC} (1^{λ}) + {Adv}_{A}^{hash} (1^{λ}) + {Adv}_{A}^{DS} (1^{λ}) . \end{matrix}$

Proof.

To prove the theorem, we construct a simulator $S$ such that no non-uniform $PPT$ environment $Z$ can distinguish between (i) the real execution ${Exec}_{Π_{S SNARK}^{Q, Light}, A, Z}^{O_{HW}^{Light}}$ where the parties $P : = {P_{1}, \dots, P_{n}}$ run protocol $Π_{S SNARK}^{Q, Light}$ in the $O_{HW}^{Light}$ -hybrid world and the corrupted parties are controlled by a dummy adversary $A$ who simply forwards messages from/to $Z$ , and (ii) the ideal execution ${Exec}_{F_{S SNARK}^{Q}, S, Z}$ where the parties interact with functionality $F_{S SNARK}^{Q}$ and corrupted parties are controlled by the simulator $S$ . We consider following cases.

Case 1: The prover $P_{i}$ is corrupted.

Simulator. The simulator $S$ internally runs $A$ , forwarding messages to/from the environment $Z$ . The simulator $S$ simulates honest verifier $P_{j}$ and the functionality $O_{HW}^{Light}$ . In addition, the simulator $S$ simulates the following interactions with $A$ .

∘ The simulated $O_{HW}^{Light}$ receives the incoming message $(C OMPUTE, sid, ssid, ⟨ h_{x}, h_{o}, h_{L}, n ⟩)$ from $P_{i}$ at the beginning. Then the simulated $O_{HW}^{Light}$ will receive $\frac{n}{k}$ messages which are either in form of $(I D, sid, ssid, {⟨ α_{k u + j}, γ_{k u + j} ⟩, x_{α_{k u + j}}}_{j = 1}^{k})$ or $(N AND, sid, ssid, {⟨ α_{k u + j}, β_{k u + j}, γ_{k u + j} ⟩, ⟨ x_{α_{k u + j}}, t_{α_{k u + j}}, x_{β_{k u + j}}, t_{β_{k u + j}} ⟩}_{j = 1}^{k})$ . $S$ performs the operation according to the protocol of $O_{HW}^{Light}$ , and finally gets $x_{γ_{n}}$ and $temp$ . During the simulation of $O_{HW}^{Light}$ , $S$ records the view of the simulated $O_{HW}^{Light}$ . If the prover sends $(ssid, α, x_{α}, t_{α})$ which is inconsistent with $(ssid, α, x_{α}^{*}, t_{α}^{*})$ yet $MAC . Verify (K, ⟨ ssid, α, x_{α}^{*} ⟩, t_{α}^{*}) = 1$ , $S$ aborts. In addition, $S$ can extract $C$ , ${Input}_{pub}$ , ${Input}_{priv}$ and $Output$ from the internal state of the simulated $O_{HW}^{Light}$ . $S$ checks if $x_{γ_{n}} = 1$ , $temp = h_{L}$ and $h_{x} = hash ({Input}_{pub}), h_{o} = hash (Output)$ . If it is the case, $S$ acts as $P_{i}$ to send $(P ROVE, sid, ssid, ⟨ C, {Input}_{pub}, {Input}_{priv}, Output ⟩)$ to functionality $F_{S SNARK}^{Q}$ . Upon receiving $(P ROVE, sid, ssid, ⟨ P_{i}, C, {Input}_{pub}, Output ⟩)$ from $F_{S SNARK}^{Q}$ , $S$ replies $(P ROVE, sid, ssid, σ)$ to $F_{S SNARK}^{Q}$ , where $σ \leftarrow DS . Sign (SK, ⟨ ssid, h_{x}, h_{o}, h_{L}, n ⟩)$ is the signature generated by the simulated $O_{HW}^{Light}$ functionality. Then $S$ records the tuple $⟨ ssid, h_{x}, h_{o}, h_{L}, C, {Input}_{pub}, {Input}_{priv}, Output, σ ⟩$ .

∘ Upon receiving $(V ERIFY, sid, ssid, ⟨ P_{j}, C^{*}, {Input}_{pub}^{*}, {Output}^{*}, π ⟩)$ from functionality $F_{S SNARK}^{Light}$ , the simulator $S$ checks if a tuple $⟨ ssid, h_{x}, h_{o}, h_{L}, C, {Input}_{pub}, {Input}_{priv}, Output, σ ⟩$ is recorded. $S$ computes $h_{L}^{*}, h_{x}^{*}, h_{o}^{*}$ using $C^{*}, {Input}_{pub}^{*}, {Output}^{*}$ . If $(C \neq C^{*} \land h_{L} = h_{L}^{*}) \lor ({Input}_{pub} \neq {Input}_{pub}^{*} \land h_{x} = h_{x}^{*}) \lor (Output \neq {Output}^{*} \land h_{o} = h_{o}^{*})$ , $S$ aborts. If $(h_{L}^{*} \neq h_{L} \lor h_{x}^{*} \neq h_{x} \lor h_{o}^{*} \neq h_{o}) \land DS . Verify (PK, ⟨ ssid, h_{x}^{*}, h_{o}^{*}, h_{L}^{*}, n ⟩, π) = 1$ , $S$ aborts. $S$ then returns ${Input}_{priv}$ to $F_{S SNARK}^{Q}$ .

Indistinguishability. The indistinguishability is proven through a series of hybrid worlds $H_{1}, \dots, H_{4}$ .

Hybrid $H_{1}$ : It is the real protocol execution ${Exec}_{Π_{S SNARK}^{Q, Light}, A, Z}^{O_{HW}^{Light}}$ .

Hybrid $H_{2}$ : $H_{2}$ is the same as $H_{1}$ except that in $H_{2}$ , during the simulation of $O_{HW}^{Light}$ , $S$ records the view of the simulated $O_{HW}^{Light}$ . If the malicious prover sends $(ssid, α, x_{α}, t_{α})$ which is inconsistent with $(ssid, α, x_{α}^{*}, t_{α}^{*})$ yet $MAC . Verify (K, ⟨ ssid, α, x_{α}^{*} ⟩, t_{α}^{*}) = 1$ , $S$ aborts. Lemma 2.

If $MAC$ is a EUF-CMA secure MAC scheme with adversarial advantage ${Adv}_{A}^{MAC} (1^{λ})$ , then $H_{2}$ and $H_{1}$ are indistinguishable with advantage $ϵ_{1} = {Adv}_{A}^{MAC} (1^{λ})$ .

Proof.

The simulator $S$ aborts when the prover has forged a MAC tag. If there exists an adversary $A$ who queries the functionality $O_{HW}^{Light}$ and is able to forge a MAC tag, then we can construct an adversary $B$ who can break the EUF-CMA security game of the underlying digital signature scheme $MAC$ . During the reduction, $B$ simulates the $O_{HW}^{Light}$ as follows. Whenever $B$ receives $I D$ commands for some $ssid$ and the input wire value $x_{α}$ , $B$ sets $x_{γ} \leftarrow x_{α}$ and sends $⟨ ssid, γ, x_{γ} ⟩$ to EUF-CMA game challenger to sign $⟨ ssid, γ, x_{γ} ⟩$ . After receiving $t_{γ}$ from the challenger, $B$ forwards it to $A$ . $B$ does the similar things when receives $N AND$ commands. Whenever $A$ outputs $⟨ {ssid}^{*}, γ^{*}, x_{γ^{*}}, t_{γ^{*}} ⟩$ . $B$ simply forwards $(m * : = ⟨ {ssid}^{*}, γ^{*}, x_{γ^{*}} ⟩, t^{*} : = t_{γ^{*}})$ to the challenger and wins the game. Clearly, $B$ wins whenever $A$ wins.

Therefore, the overall advantage is ${Adv}_{A}^{MAC} (1^{λ})$ . □

Hybrid $H_{3}$ : $H_{3}$ is the same as $H_{2}$ except that in $H_{3}$ , $S$ receives $(V ERIFY, sid, ssid, ⟨ P_{j}, C^{*}, {Input}_{pub}^{*}, {Output}^{*}, π ⟩)$ from functionality $F_{S SNARK}^{Light}$ , $S$ founds a recorded tuple $⟨ ssid, C, {Input}_{pub}, {Input}_{priv}, Output, σ ⟩$ and computes $h_{L}^{*}, h_{x}^{*}, h_{o}^{*}$ using $C^{*}, {Input}_{pub}^{*}, {Output}^{*}$ . If $(C \neq C^{*} \land h_{L} = h_{L}^{*}) \lor ({Input}_{pub} \neq {Input}_{pub}^{*} \land h_{x} = h_{x}^{*}) \lor (Output \neq {Output}^{*} \land h_{o} = h_{o}^{*})$ , $S$ aborts. Lemma 3.

If $hash$ is a collision resistant hash function with adversarial advantage ${Adv}_{A}^{hash} (1^{λ})$ , then $H_{3}$ and $H_{2}$ are indistinguishable with advantage $ϵ_{2} = {Adv}_{A}^{hash} (1^{λ})$ .

Proof.

The simulator $S$ aborts when the prover has found a collision for the hash value. If there exists an adversary $A$ who queries the functionality $O_{HW}^{Light}$ and finds a collision of $h_{x}$ , $h_{o}$ or $h_{L}$ , then we can construct an adversary $B$ who can break the collision resistant game of uderlying hash function $hash$ . During the reduction, $B$ simulates the $O_{HW}^{Light}$ as follows. Up on receiving query $(C OMPUTE, sid, ssid, ⟨ h_{x}, h_{o}, h_{L}, n ⟩)$ , $B$ performs the operation according to the protocol of $O_{HW}^{Light}$ , and finally gets $x_{γ_{n}}$ and $temp$ and the whole collection of ${L_{i}}_{i = 1}^{n}$ . First of all, consider the case for $h_{L}$ . $B$ forwards $h_{L}$ to $A$ . $A$ outputs $L^{*} : = {L_{i}^{*}}_{i = 1}^{n^{*}}$ . $B$ creates two set ${h_{i}}_{i = 1}^{n}$ and ${h_{i}^{*}}_{i = 1}^{n^{*}}$ , and computes $h_{i} \leftarrow hash (h_{i - 1}, {L_{k (i - 1) + j}}_{j = 1}^{k}, i)$ and $h_{i}^{*} \leftarrow hash (h_{i - 1}^{*}, {L_{k (i - 1) + j}^{*}}_{j = 1}^{k}, i)$ , where $h_{0} = h_{0}^{*} = 0$ . Whenever $B$ finds $i, j$ such that $h_{i} = h_{j}^{*}$ , $B$ submits $(⟨ h_{i - 1}, {L_{k (i - 1) + j}}_{j = 1}^{k}, i ⟩, ⟨ h_{j - 1}^{*}, {L_{k (i - 1) + j}^{*}}_{j = 1}^{k}, j ⟩)$ to the collision resistant game challenger and wins the game. As for $h_{x}$ and $h_{o}$ , similiar approach will be taken. Clearly, $B$ wins whenever $A$ wins.

Therefore, the overall advantage is ${Adv}_{A}^{hash} (1^{λ})$ . □

Hybrid $H_{4}$ : $H_{4}$ is the same as $H_{3}$ except that in $H_{4}$ , If $(h_{L}^{*} \neq h_{L} \lor h_{x}^{*} \neq h_{x} \lor h_{o}^{*} \neq h_{o}) \land DS . Verify (PK, ⟨ ssid, h_{x}^{*}, h_{o}^{*}, h_{L}^{*}, n ⟩, π) = 1$ , $S$ aborts. Lemma 4.

Proof.

The simulator $S$ aborts when the prover can generate an accepting proof without querying the functionality $O_{HW}^{Light}$ . If there exists an adversary $A$ who can generate an accepting proof without querying $O_{HW}^{Light}$ , then we can construct an adversary $B$ who can break the EUF-CMA security game of the underlying digital signature scheme $DS$ with the same advantage. Indeed, since $O_{HW}^{Light}$ is always trusted, the only way an adversary $A$ can produce an accepting proof is to forge a signature. During the reduction, $B$ simulates the $O_{HW}^{Light}$ as follows. Up on receiving query $(C OMPUTE, sid, ssid, ⟨ h_{x}, h_{o}, h_{L}, n ⟩)$ , $B$ performs the operation according to the protocol of $O_{HW}^{Light}$ , and finally gets $x_{γ_{n}}$ and $temp$ . $B$ checks if $x_{γ_{n}} = 1$ and $temp = h_{L}$ . It then queries the EUF-CMA game challenger to sign $⟨ ssid, h_{x}, h_{o}, h_{L}, n ⟩$ . After receiving the signature σ from the challenger, $B$ forwards it to $A$ . When $A$ outputs $(V ERIFY, sid, ssid, ⟨ C^{*}, {Input}_{pub}^{*}, π^{*} ⟩)$ such that the verification passes. $B$ computes $h_{x}^{*} \leftarrow hash ({Input}_{pub}^{*}), h_{o}^{*} \leftarrow hash ({Output}^{*})$ and generates $L^{*} \leftarrow Convert (C^{*}, {Input}_{pub}^{*}, {Output}^{*})$ , where $L^{*} : = {L_{i}^{*}}_{i = 1}^{n^{*}}$ . $B$ then sets $h_{L}^{*} : = 0$ , and updates $h_{L}^{*} \leftarrow hash (h_{L}^{*}, {L_{k (i - 1) + j}^{*}}_{j = 1}^{k}, i)$ for $i \in [\frac{n^{*}}{k}]$ . $B$ outputs $(m^{*} : = ⟨ ssid, h_{x}^{*}, h_{o}^{*}, h_{L}^{*}, n^{*} ⟩, σ^{*} : = π^{*})$ as the forged message signature pair. Clearly, $B$ wins whenever $A$ wins.

Therefore, the overall advantage is ${Adv}_{A}^{DS} (1^{λ})$ . □

The adversary’s view of $H_{4}$ is identical to the ideal execution ${Exec}_{F_{S SNARK}^{Q}, S, Z}$ . Therefore, the overall distinguishing advantage is $\begin{matrix} {Adv}_{A}^{MAC} (1^{λ}) + {Adv}_{A}^{hash} (1^{λ}) + {Adv}_{A}^{DS} (1^{λ}) . \end{matrix}$

Case 2: The verifier $P_{j}$ is corrupted.

Simulator. Similar to Case 1, the simulator $S$ internally runs $A$ , forwarding messages to/from the environment $Z$ . The simulator $S$ simulates honest prover $P_{i}$ and the functionality $O_{HW}^{Light}$ . In addition, the simulator $S$ simulates the following interactions with $A$ .

Case 3: Both the prover $P_{i}$ and the verifier $P_{j}$ are corrupted.

Simulator. Trivial case. There is nothing needs to extract, as the trustees do not have input. The simulator $S$ just run trustee according to protocol $Π_{S SNARK}^{Light}$ .

This concludes the proof. □

6. Implementation

6.1. $O_{HW}^{Q}$ implementation

In this section, we realize the $Q$ -compliant trusted hardware functionality $O_{HW}^{Q}$ via Intel SGX and Arm TrustZone.

Fig. 6.

The script engine enclave $SE$ .

Challenges. In both platforms, there are a number of challenges need to be resolved. In terms of SGX, as mentioned in Section 2.1, the remote attestation of Intel SGX currently requires the verifier to contact the Intel IAS server. On the other hand, in a typical SNARK proof system usage case, the prover aims to prove the truth of the statement to a great number of verifiers. If each verifier needs to query the Intel IAS server to check the proof, the overall performance is limited by Intel’s throughput. Moreover, the validity of a SNARK proof should be consistent over time, i.e., if a SNARK proof is verifiable at this moment, the same proof should remain verifiable in the future. Unfortunately, this would not be the case if we invoke the Intel IAS in the verification process; certifying an old quote (say, generated 1 year ago) is never the design goal of Intel’s remote attestation. This is because the quote needs to contain an non-revoked proof for each item on the signature revocation list, and the proof is no longer verifiable once the revocation list is updated at the Intel side. That means a quote is only valid until the next revocation list update. To resolve this issue, in our design, after generating the quote, the prover immediately queries the Intel IAS server for the attestation verification report on behave of a verifier. Since the attestation verification report is signed by Intel, given Intel’s public key, anyone can verify the validity of the attached signature. This tweak also makes the verification process non-interactive.

Secondly, the existing SGX-based proof system, e.g., [53], requires the prover and the verifiers agree on the executable binary (enclave) for the language to be proven. It would make it impossible to build a universal NIZK system in practice. Note that SGX only signs the measure of the enclave, which cannot be directly compared with the corresponding algorithm. Imaging a verifier who is checking a SNARK proof generated some time ago, how would the verifier know the executable binary (enclave) is faithfully compiled? Therefore, SNARK systems, like [53], would need a trusted party to generate an executable binary (enclave) for a given problem instance, and the binary is served as the concrete CRS for the given instance.

In terms of TrustZone, unlike the ecosystem of SGX that is controlled by Intel, the fragmentation of the ARM TrustZone ecosystem may make it hard to have a unique setup standard. To resolve this issue, we need to introduce a trusted setup authority to serve as an attestation server.

Fig. 7.

Protocol $Π_{SGX}^{Q}$ realizing $O_{HW}^{Q}$ via Intel SGX.

SGX-based system overview. In our system, the protocol $Π_{SGX}^{Q}$ involves three entities: the (trusted) Intel server, denoted as $IS$ , the prover $P$ , and the SGX hardware, denoted as ${HW}_{SGX}$ . In practice, it is still a challenge for a third party to verify the consistency between an executable binary and its software specification. That is, the binary contains no bug, no trapdoor, and it is not subverted. Even it is possible, it dramatically increases the verifier’s complexity. On the other hand, it is implausible to assume a trusted third party that is available to generate a certified binary for each problem instance. To address this issue, we decide to adopt a scripting language, called Lua. Lua is a lightweight script language, which is ideal for the SGX enclave computation environment. We let a trusted party, i.e., the (trusted) Intel server $IS$ , to produce a Lua script engine enclave $SE$ . $IS$ then signs $SE$ so that no one can tamper with its functionality. As depicted in Fig. 6, $SE$ has one main function called $VerifySign$ .2

The enclave also has a GetQEInfo function to receive the target information of QE. It is omitted for simplicity.

It takes three arguments: (i) a script

C

, (ii) a public input

{Input}_{pub}

(iii) a tag,

tag

, that can be used to specify the proof context, such as

ssid

, etc. The

VerifySign

function first loads the private input

{Input}_{priv}

from the prover; it then executes the script

y \leftarrow C ({Input}_{pub}, {Input}_{priv})

using the script interpreter. Abort if

y = ⊥

, which means the execution error happened; that is considered as

Q (C, {Input}_{pub}, {Input}_{priv}, y) = 0

. Otherwise, it sets

h : = hash (C, {Input}_{pub}, y)

and

ReportData : = (tag, h)

; it then invokes

EREPORT

to create a report r for QE to sign. Finally, it returns

(y, r)

Fig. 8.

SGX based trusted hardware instantiation.

Remark.

Technically, the private input ${Input}_{priv}$ can be input to the $VerifySign$ function together with the script $C$ and the public input ${Input}_{pub}$ as another argument. We choose to load ${Input}_{priv}$ separately during the enclave execution for the sake of uniformity: (i) for some applications, we could choose to hard code $C$ and ${Input}_{pub}$ for efficiency; and (ii) in case that the prover needs to use an SGX enabled server from a third party, it is possible to load ${Input}_{priv}$ in to the enclave via secure channels to ensure privacy.

The hardware functionality $O_{HW}^{Q}$ is instantiated by the protocol $Π_{SGX}^{Q}$ shown in Fig. 7. The $I NIT$ functionality is realized by the Intel server $IS$ and the hardware ${HW}_{SGX}$ . Upon receiving $(I NIT, s i d)$ , $IS$ invokes the EPID provisioning key procedure [34] with ${HW}_{SGX}$ . The root seal key of ${HW}_{SGX}$ was generated during the processor manufacturing, and Intel claims that they are oblivious to it; the root provisioning key is set up by a special purpose offline key generation facility. The actual procedure is complicated; ${HW}_{SGX}$ is registered to the Intel server $IS$ via a blind joining protocol. We refer interested reader to [34] for details. Hereby, we simplify the description – at the end, ${HW}_{SGX}$ stores a group signature secret key $GSK$ , and the Intel server $IS$ stores the corresponding group signature public key $GPK$ that allows it to verify the signatures generated by ${HW}_{SGX}$ . Note that the group signature is only used to authenticate ${HW}_{SGX}$ to the Intel, rather than to the public. Therefore, it is possible to replace the group signature scheme with some symmetric key cryptographic primitive, e.g., MAC. In addition, $IS$ also generates $(\tilde{PK}, \tilde{SK}) \leftarrow DS . KeyGen (1^{λ})$ . It then creates the script engine enclave $SE$ as depicted in Fig. 6 and signs it $\tilde{σ} \leftarrow DS . Sign (\tilde{SK}, SE)$ . The public key is defined as ${PK}^{*} : = (\tilde{PK}, SE, \tilde{σ})$ . Anyone can query $(G ET PK, s i d)$ to the Intel server $IS$ to fetch the public key ${PK}^{*}$ . The $C OMPUTE$ command is realized by all three parties. Upon receiving $(C OMPUTE, s i d, s s i d, ⟨ C, {Input}_{pub}, {Input}_{priv} ⟩)$ , the prover $P_{i}$ creates an enclave instance of $SE$ to ${HW}_{SGX}$ ; it then invokes $VerifySign (C, {Input}_{pub}, tag)$ (supplying ${Input}_{priv}$ during the execution). ${HW}_{SGX}$ executes the script $y \leftarrow C ({Input}_{pub}, {Input}_{priv})$ ; Abort, if $y = ⊥$ , which is considered as $Q (C, {Input}_{pub}, {Input}_{priv}, y) = 0$ . Otherwise, it outputs a report $r (C, {Input}_{pub}, y, tag)$ for local attestation. The prover $P_{i}$ sends the report $r (C, {Input}_{pub}, y, tag)$ to the QE of ${HW}_{SGX}$ to produce a quote $q (C ({Input}_{pub}, {Input}_{priv}))$ ; the prover $P_{i}$ sends the quote $q (C, {Input}_{pub}, y, tag)$ to the Intel server $IS$ to verify. The above steps are simplified in Fig. 7. The Intel server $IS$ checks the validity of the quote, i.e., checking the group signature and that the SGX platform generating the quote is not revoked; it then signs and returns $σ \leftarrow DS . Sign (SK, ⟨ C, {Input}_{pub}, y, tag ⟩)$ ; The prover $P_{i}$ outputs $(y, σ)$ ; Figure 8 summaries the basic flow for the $I NIT$ , $G ET PK$ , and $C OMPUTE$ protocols.

TrustZone-based system overview. ARM TrustZone is another popular trusted hardware platform that can also be leveraged (as long as a device-unique, asymmetric key pair signed by the device’s vendor exists). ARM TrustZone provides isolated execution by separating the CPU into two different worlds, i.e., normal world and secure world. The code running inside the normal world cannot directly access the resource inside the secure world. Also only the application inside the secure world can access the protected resource.

Specifically, the device-unique key pair can be used to sign the attention blob that indicates the attestation data originates from the secure world. The attestation data in this case contains $⟨ C, {Input}_{pub}, y, tag ⟩$ . The signed data will be passed to the attestation server of device vendor (like Intel IAS). If the signature verification passes on the device vendor’s attestation server, the prover generates proof.

The Lua script engine design and system architecture is similar to the SGX-based solution. However, it is more efficient, as the attestation data can be verified without interacting with the attestation server if the verifier already fetched the public key $PK$ from it.

Evaluations. Our SGX-based prototype is implemented in C++ using the Intel(R) SGX SDK v2.5 for Linux. Our implementation is built on top of [49], and we added OpenSSL lib functions for common cryptographic primitives, such as SHA256, ECDSA, etc. Since system call is not allowed in enclave, we also simulated a simple file system to support the Lua interpreter. The size of the compiled enclave binary is approximately 3.2 MB.

Up on execution, the prover first creates an instance of the Lua script engine enclave in the SGX and transfers the target information of QE into the Lua script engine enclave, which will be used later to generate the report for QE. The prover then produces his proof by calling specific function interface of the enclave, $VerifySign$ , taking the script $C$ and the public input ${Input}_{pub}$ as the arguments of the function. In our prototype, the script $C$ and statement ${Input}_{pub}$ are pre-loaded into the simulated filesystem. After loading ${Input}_{priv}$ from the prover and putting it into the simulated filesystem, the enclave invokes the Lua interpreter to process the script $y \leftarrow C ({Input}_{pub}, {Input}_{priv})$ , where the script can access the statement and witness through Lua file operations. Note that Lua heap size need to be predefined while compiling the Lua script engine enclave, such as 32 MB, which restrict the class of script it can support.

After the script execution, the enclave hashes $h : = hash (C, {Input}_{pub}, {Input}_{priv})$ and then put $(tag, h)$ in to the $REPORTDATA$ field of the report structure, and generate the report $r (tag, h)$ for QE to sign. The prover will then fetch the report $r (tag, h)$ and send it together with signature revocation list (which can be obtained from the Intel IAS and SPID (which is assigned by the Intel IAS when user registers to the Intel IAS) to the QE. The QE will verify the report using its report key and compute an non-revoked proof for the signature revocation list, generating a quote consisting of the $ReportBody$ field of the report, the non-revoke proof and some other necessary information. The prover then will send the quote to the Intel IAS server for attestation verification report.

Table 2

QuoteBody structure

uint16_t	version;
uint16_t	sign_type;
sgx_epid_id_t	epid_group_id;
sgx_isv_svn_t	qe_svn;
sgx_isv_svn_t	pce_svn;
uint32_t	xeid;
sgx_basename_t	basename;
sgx_cpu_svn_t	cpu_svn;
sgx_mise_select_t	misc_select;
uint8_t	reserved1[28];
sgx_attributes_t	attributes;
sgx_measurement_t	mr_enclave;
uint8_t	reserved2[32];
sgx_measurement_t	mr_signer;
uint8_t	reserved3[96];
sgx_prod_id_t	isv_prod_id;
sgx_isv_svn_t	isv_svn;
uint8_t	reserved4[60];
sgx_report_data_t	report_data;

Reducing proof size. Naively, the prover can send the entire signed attestation verification report as the NIZK proof. The proof size is 731 Bytes (IAS report size) + 256 Bytes (the signature size).

To reduce proof size, we observe that Intel’s signature is signed on top of the hash of the attestation verification report, so the prover does not need to give the entire report as a part of the proof as far as the verifier can reproduce the hash of the report. However, the verifier is interested in some field of in the $isvEnclaveQuoteBody$ , such as $REPORTDATA$ . Notice that SHA256 uses Merkle-Damgård structure, i.e., the final hash digest is calculated by iteratively calling a compression function over trunks of the signing document. Therefore, the prover can give the partial hash digest of the first part of the signing report, including ID, timestamp, version, $isvEnclaveQuoteStatus$ . The $isvEnclaveQuoteBody$ structure is shown in Table 2. The verifier is only interested in the five fields marked in grey background, and they can be reconstructed from the public input of the verifier. Moreover, currently, all the reserved fields must be 0. Moreover, the verifier also wants to check $isvEnclaveQuoteStatus = OK$ ; nevertheless, we observe that the attestation verification report whose $isvEnclaveQuoteStatus = OK$ has a fixed length n. Otherwise, the length of the attestation verification report is different from n. Based on that observation, we can regard the length n as another public input of the verifier. Then when the verifier receives a proof, he/she can check whether the $isvEnclaveQuoteStatus$ field of the associated attestation verification report is $OK$ by putting the length n into the end of the report as the total hashed length. then if the $isvEnclaveQuoteStatus$ field is not $OK$ , the report hash is not aligned probably, resulting a wrong hash digest.

We let the prover give the partial hash digest until $misc_select$ field. Denote the partial hash digest of the report as $p h$ . The prover needs to provide the $attributes$ field, denoted as $attr$ , which is 16 Bytes.3

In fact, there are 56 bits reserved area, whose default value is 0 in the attributes field. Hence, the size can be further reduced by 56 bits.

The proof is

(p h, attr, σ)

. The verifier can use reconstruct the hash of the report and then check the validity of the signature. The proof size is now reduced to 41 Bytes + 256 Bytes ( the signature size), which is 297 Bytes.

Fig. 9.

Performance comparison of different SNARK proof systems in terms of prover’s running time, verifier’s running time, and proof size. The complexity is measured by the number of multiplication gates. Our work and BCCGP are 128 bit security; libSNARK and SCI are 80-bit security; ligero and zk-STARK are 60-bit security. Our system is tested on a SGX-equipped processor (I7-8700 @ 3.2GHz and 16 GB RAM, single thread) and hikey 960 TrustZone development board. All the other systems were tested on a server with 32 AMD cores @ 3.2GHz and 512 GB RAM, and the data was reported by [4]. For libSNARK, the hollow marks (libSNARK*) in verifier time and proof size measure only count the post processing phase; while solid marks also count CRS generation time. For our SGX based scheme, the prover’s running time includes network time for intel IAS verification; SGX-a (TZ-a) stands for arithmetic circuit over ring $Z_{2^{64}}$ , and SGX-b (TZ-b) stands for Boolean circuit (NAND gates) w.R.t. SGX and TrustZone platforms.

Our TrustZone-based prototype is developed on the Hikey 960 development board, which is powered by Huawei Kirin 960 SoC with 4 ARM Cortex-A73 cores and 4 1.8 GHz ARM Cortex-A53 cores. There are 4 GB DDR4 memory and 32 GB UFS flash on our board. In our experiment, we choose OPTEE(v3.6) as the OS in the secure world, which is open source and well maintained. For the normal world OS, we use a Linux distribution, which is developed by Linaro Security Working Group based on Linux kernel v5.1 and able to corporate with OPTEE. Then, we implement a Trusted App(TA) for the secure world, which will be managed by OPTEE. The Client Application(CA) in the normal world can invoke the TA through specific interface. Lua Intrepreter(v5.3.2) is adopted and modified. The default secure memory size supported by OPTEE is 16 MB, which restricts the script size. A signing key is stored in the TrustZone for the experiment. The enclave structure and system design is similar to the SGX-based solution, except we adopt ECDSA signature over the secp256k1 curve. Therefore, the signature/proof size is only 32 Bytes.

Figure 9 shows the performance comparison of different SNARK proof systems w.r.t. prover’s running time, verifier’s running time, and proof size. Although our SNARK proof system support RAM model computer program, we implemented circuit evaluation as Lua script to facilitate comparison. We emphasize that the reported time is tested using Lua scripts. If the circuit is written in native C, the performance is approximate 10 times better on both SGX and TrustZone platforms. The complexity is measured by the number of multiplication gates. We provide ‘SGX-A’ and ‘TZ-A’ as the benchmark for arithmetic circuit over ring $Z_{2^{64}}$ for SGX and TrustZone, respectively; ‘SGX-B’ and ‘TZ-B’ as the benchmark for Boolean circuit, using SIMD to implement NAND gates. The measure of the enclave is assumed to be pre-computed and announce by Intel, so it is not counted into the verifier’s running time; moreover, the problem instance consists of the Lua script and its hash; otherwise, the verifier can also compute the hash at a small cost. As shown in [20], SHA256 can be performed at 2.1-3.5GB/s on most platforms.

6.2.

O_{HW}^{Light}

implementation

In this section, we simulate the lightweight trusted hardware functionality $O_{HW}^{Light}$ via Intel SGX. Because most of the instantiations are similiar to Section 6.1, except that: (i) it only computes NAND gates; (ii) it also uses MACs, we focus on the differences here.

Fig. 10.

The enclave $E^{Light}$ .

Enclave. Unlike the script engine enclave depicted in Fig. 6, the enclave $E^{Light}$ we create for $O_{HW}^{Light}$ has three main functions: $Init, VerifyID, VerifyNAND$ , and it is presented in Fig. 10. The $Init$ function takes (i) the description of the circuit $C$ and ${Input}_{pub}, Output$ , that is, $h_{x}, h_{o}, h_{L}, n$ ; (ii) a tag, $tag$ , that can be used to specify the proof context, such as $ssid$ , etc. The $Init$ function maintains a variable $temp$ and a counter $ctr$ which are both initialized as 0, and records the tuple $⟨ h_{x}, h_{o}, h_{L}, n, tag ⟩$ . The $VerifyID$ function takes (i) the description of the k identity gates, that is ${⟨ α_{k u + j}, γ_{k u + j} ⟩}_{j = 1}^{k}$ and (ii) a tag $tag$ . The $VerifySign$ function first loads ${x_{α_{k u + j}}}_{j = 1}^{k}$ from the prover; it then executes $x_{γ_{k u + j}} \leftarrow x_{α_{k u + j}}$ and signs $t_{γ_{k u + j}} \leftarrow MAC . Sign (K, ⟨ tag, γ_{k u + j}, x_{γ_{k u + j}} ⟩)$ . Then it updates $ctr \leftarrow ctr + 1$ and $temp \leftarrow hash (temp, {(α_{k u + j}, γ_{k u + j})}_{j = 1}^{k}, ctr)$ , and returns ${x_{γ_{k u + j}}, t_{γ_{k u + j}}}_{j = 1}^{k}$ . The $VerifyNAND$ function does the similar things as $VerifyID$ , except that (i) it checks $MAC . Verify (K, ⟨ tag, α_{k u + j}, x_{α_{k u + j}} ⟩, t_{α_{k u + j}}) = 1$ and $MAC . Verify (K, ⟨ tag, β_{k u + j}, x_{β_{k u + j}} ⟩, t_{β_{k u + j}}) = 1$ ; (ii) when $ctr = \frac{n}{k}, x_{γ_{n}} = 1$ and $temp = h_{L}$ , it sets $ReportData = (tag, h_{x}, h_{o}, h_{L}, n)$ and invokes $EREPORT$ to create a report r for QE to sign.

Fig. 11.

Protocol $Π_{SGX}^{Light}$ realizing $O_{HW}^{Light}$ via Intel SGX.

The lightweight SNARK system overview. Here, the protocol $Π_{SGX}^{Light}$ involves three entities: the (trusted) Intel server, denoted as $IS$ , the prover $P$ , and the SGX hardware, denoted as ${HW}_{SGX}$ . We let a trusted party, i.e., the (trusted) Intel server $IS$ , to produce a enclave $E^{Light}$ . $IS$ then signs $E^{Light}$ so that no one can tamper with its functionality.

The hardware functionality $O_{HW}^{Light}$ is instantiated by the protocol $Π_{SGX}^{Light}$ shown in Fig. 11. The $I NIT$ functionality and the $G ET PK$ functionality are similiar with protocol $Π_{SGX}^{Q}$ in Section 6.1, thus we will not go into details here. Upon receiving $(C OMPUTE, sid, ssid, ⟨ h_{x}, h_{o}, h_{L}, n ⟩)$ , the prover $P_{i}$ creates an enclave instance of $E^{Light}$ to ${HW}_{SGX}$ ; it then invokes $Init (h_{x}, h_{o}, h_{L}, n, tag : = (sid, ssid))$ . The ${HW}_{SGX}$ sets $temp = ctr = 0$ and records $⟨ h_{x}, h_{o}, h_{L}, n, tag ⟩$ . Upon receiving $(I D, sid, ssid, {⟨ α_{k u + j}, γ_{k u + j} ⟩, x_{α_{k u + j}}}_{j = 1}^{k})$ , the prover $P_{i}$ creates an enclave instance of $E$ to ${HW}_{SGX}$ ; it then invokes $VerifyID ({⟨ α_{k u + j}, γ_{k u + j} ⟩}_{j = 1}^{k}, tag)$ (supply ${x_{α_{k u + j}}}_{j = 1}^{k}$ during the execution). And the ${HW}_{SGX}$ executes the protocol depicted in Fig. 10 and outputs ${x_{γ_{k u + j}}, t_{γ_{k u + j}}}_{j = 1}^{k}$ . The $N AND$ command is similar with the $I D$ command, except when the ${HW}_{SGX}$ outputs a report $r (tag, h_{x}, h_{o}, h_{L}, n)$ for local attestation, the Intel server $IS$ is involved. The prover $P_{i}$ sends the report $r (tag, h_{x}, h_{o}, h_{L}, n)$ to the QE of ${HW}_{SGX}$ to produce a quote $q (tag, h_{x}, h_{o}, h_{L}, n)$ ; the prover $P_{i}$ sends the quote $q (tag, h_{x}, h_{o}, h_{L}, n)$ to the Intel server $IS$ to verify. The above steps are simplified in Fig. 11. The Intel server $IS$ checks the validity of the quote, i.e., checking the group signature and that the SGX platform generating the quote is not revoked; it then signs and returns $σ \leftarrow DS . Sign (SK, ⟨ tag, h_{x}, h_{o}, h_{L}, n ⟩)$ . The prover $P_{i}$ outputs σ finally.

Evaluations. Our SGX-based prototype is implemented in C++ using the Intel(R) SGX SDK v2.11 for Linux. we added OpenSSL lib functions for common cryptographic primitives, such as SHA256, ECDSA, etc. We instantiate $MAC$ with HMAC using SHA256 and $DS$ with ECDSA. We expect to achieve two objectives through experiments: (i) try to determine the optimal value of k; (ii) demonstrate the effectiveness of our proposal.

Fig. 12.

Performance comparison of different k choices in terms of prover’s running time and verifier’s running time. The complexity is measured by the number of multiplication gates. Our system is tested on a SGX-equipped processor (I7-8700 @ 3.2 GHz and 16 GB RAM, single thread).

Figure 12 shows the performance of our proposal w.r.t. prover’s running time and verifier’s running time. The complexity is measured by the number of multiplication gates. From the Fig. 12(a), we conclude that increasing the value of k at the beginning can significantly improve the prover time, because the initial performance bottleneck lies in the overhead of calling the enclave, and increasing the value of k can reduce the number of calls. As k increases, the curve in Fig. 12(a) flattens out, which means that the performance bottleneck at this time lies in the computational overhead (e.g. MAC operations) inside the enclave. We also conclude that the performance of our proposal is competitive. When set $n = 2^{25}$ , the prover time is less than 25 s, and it is much faster than libSNARK, Ligero etc. Note that, no matter which k and n we choose, the proof size is always a small constant (i.e. 297 bytes), thus the verifier time is generally around 1 ms.

7. Blockchain applications

Resolving verifier’s dilemma. The term verifier’s dilemma in the blockchain context was first proposed in [43]. In this section, we first briefly explain what the problem is and then present a solution using our succinct NIZK proof system.

Verifier’s dilemma. In a blockchain system, when a new block is produced, it will be propagated to all the other nodes through the P2P network. In principle, each node needs to independently verify the validity of the block, i.e. in terms of Bitcoin, all the transaction inputs are never spent (e.g., in the UTXO) and the signatures attached to all the transactions are valid. However, in practice, a miner may decide to skip the verification process, for instance, to gain advantages in the proof of work over the other miners – honest miners need to first verify the block, accept it, and then start the proof of work for the next block; whereas, dishonest miners assume that the block is valid, skip the expensive verification, and immediately start to mine the next block.

To resolve the problem, we can let the miner to attach a proof showing the validity of the block. It only takes 1 ms to check the proof; therefore, the disadvantage of honest miners are merely 1 ms, which is negligible compared with the network delay. In our prototype, the statement consists of the root of the Merkle tree commitment (64 levels) of the latest UTXO, denoted as r and the hash of the block, denoted as h. The prover wants to convince the verifiers the followings are true:

The content of the block that can hash to h;

For each transaction input, there exist a path of length 64 can be hashed (SHA256) to r;

The ECDSA signature of each transaction is valid w.r.t. the corresponding public key.

Performance. Table 3 shows the prover’s running time to prove the validity of a Bitcoin block with 3700 transactions. For SGX platform, It takes 91 ms to create the enclave, and the VerifySign function running time is 2.2 s. It then takes 32 ms for the QE to sign a quote; it takes approximately 675 ms4

⁴
The connection time with IAS varies, depending on the region and country. The experiment is tested on a Linode cloud server at Fremont, California, US.

to contact the IAS and receives the verification report from it. The total time for the prover to generate a proof is about 3 s. Then the verifiers take 1.4 ms to verify the proof. For TrustZone platform, It takes 93 ms to open session with TA in the OPTEE, and invoking VerifySign function takes 4.241 s. It then takes 14 ms to close the session. The total time for the prover to generate a proof is about 4.348 s. Note, in our experiment for TrustZone platform, we omit the interaction time with the remote attestation server because of the lack of the attestation server.

Table 3

Proving validity of a Bitcoin block (3700 Txs)

Prover time(SGX)	3 s	create enclave	91 ms
		VerifySign	2.2 s
		get QE quote	32 ms
		get IAS report	675 ms
Prover time(TrustZone)	4.348 s	open session	93 ms
		VerifySign	4.241 s
		close session	14 ms
Verifier time(SGX)	1.4 ms

Fast NIPoPoW. Proof-of-Work (PoW) is one of the most popular consensus mechanism to realize an open permissionless blockchain, e.g., Bitcoin and Ethereum. To determine “longest” chain, the nodes need to verify the entire linearly-growing chain of PoWs. Therefore, verify the amount of computation involved in a chain could be an expensive task for a long chain (e.g., the blockchain of Bitcoin consists of 575000 blocks,) if the nodes only store the genesis block. In practice, checkpoints are used to mitigate this issue.

Non-Interactive Proofs of Proof-of-Work (NIPoPoWs) is a primitive introduced by [36]. It is a short proof that contains the following information,

the total difficulty of all blocks in a chain,

if a given block is on that chain.

The verifiers can check the validity of the proof without downloading all the block headers.

NIPoPoWs enables lightweight wallets with simplified payment verification (SPV). The SPV clients can request multiple NIPoPoWs from the full nodes (i.e., the nodes store the whole blockchain). As long as one of those full nodes is honest, the SPV clients can know if a given block is on the longest chain.

NIPoPoWs also can be used to build a cross-chain solution. Because the miners that run a blockchain do not monitor other blockchain networks, this can be done with short proofs. If a blockchain supports smart contracts, e.g., Ethereum, a contract can be written to validate a NIPoPoW to check that something happened on another blockchain and react to it. For instance, a payment made on a blockchain system, that supports NIPoPows, could cause a payment to be released by an Ethereum smart contract.

In the protocol in [36], the miners run an $O (| C | log (| C |))$ (where $| C |$ is the length of the blockchain) algorithm to generate a proof of size $O (m log (| C |))$ where m is a security parameter. After receiving the proof from the miners, the SPV clients can verify the proof with the probability of $1 - negl (m)$ (where $negl (m)$ is negligible function of m). The parameter m is a trade-off parameter between security and performance. Increasing m makes the protocol more secure (reduce the probability of false verification), but it also harms the performance (increase the size of the proof and the verification time).

In our SNARK proof system, the miner generate a proof by parsing the blockchain to SGX. The algorithm to generate the proof take $O (| C |)$ complexity. The size of the proof is $O (1)$ . The time for the SPV clients to verify the proof is also $O (1)$ . Our NIZK proof system is more efficient in terms of proof generation/ verification time and proof size. Furthermore, our verification algorithm always returns the correct value as long as the digital signature scheme is secured. As shown in Table 4, the prover needs about 3.84 seconds to create such a proof (of size 300 bytes) for a chain of 575000 blocks. The verifiers take 1.5 ms to verify the proof.

Table 4

Proving chain difficulty for 575000 bitcoin blocks

Prover time	3.84 s	create enclave	220 ms
		VerifySign	2.89 s
		get QE quote	32 ms
		get IAS report	694 ms
Verifier time	1.5 ms

Privacy preserving smart contract. The smart contract systems over decentralized cryptocurrencies allow making safe transactions between distrustful parties without trusted third parties. However, most of the existing systems lack transaction privacy. All the information of the smart contracts are exposed on the blockchain.

Privacy preserving smart contract is introduced in [35,38]. Cryptographic primitives, e.g., zero-knowledge proofs, have been used to preserve the privacy of smart contracts. A privacy preserving smart contract consist of two parts

A private portion which takes in clients’ input data (e.g., in two-party coin tossing) as well as currency units (e.g., in an auction). The private portion is executed to determine the payout distribution amongst the clients.

A public portion (e.g., the smart contract’s program) that does not touch private data or money.

After the smart contracts are executed, everyone can verify the execution of the smart contract without knowing any the private portion.

Privacy preserving smart contract can be used for several real-life application, such as insurance, auctions, digital identity and records management. For example, in a unique bid auction smart contract, the clients bid some money to win a prize. The winner is the client with the lowest unique bid. In this case, privacy preserving smart contract is needed so that all the bidding information cannot be revealed.

Nevertheless, the smart contracts in [35,38] is not effective enough. It takes a few minutes to run the cryptographic computation. Later, there are several papers provide different methods to improve the performance of privacy preserving smart contract. In [17,61] a trusted execution environment/hardware is combined with a blockchain to address the performance issues. Here, the time to verify an execution of a smart contract can be hundreds of milliseconds.

Our SNARK proof system can also be combined with a blockchain to improve the performance of privacy preserving smart contract. When clients wants to execute a smart contract, they parse the public and private portion to the SGX to generate an execution proof. Then, the miners can verify the proof without knowing the private portion. We expect the miners can verify the proof within 1.5 ms.

8. Related work

Universal SNARK. Now we briefly describe several different practical approaches for universal SNARK (i.e., can be applied to general computations and languages in NP). We note that our description here are based on a large body of existing results, and unfortunately we cannot cover the entire body research in this line. We mainly compare the performance related properties, including prover scalability, verifier scalability, setup/initialization scalability, and communication scalability. Additionally, we also compare the underlying setup assumptions and computational assumptions. We note that, in the existing approaches, each setup only support one language instance. Meanwhile, our scriptable SNARK can support multiple language instances in a single setup.

There are multiple approaches to scalable SNARK. The first approach is based on homomorphic public-key cryptography, by Ishai et al. [32] and Groth [28]. Then Gennaro et. al [23] introduced an extremely efficient instantiation, based on Quadratic Span Programs, which later been implemented in Pinocchio [48]; see also [5,7,19,52]. Note that, this technique has been used in Zcash.

We note that, the homomorphic public-key cryptography based approach can be combined with other techniques to improve the performance. For example, Valiant, [55] suggested to reduce prover space consumption via knowledge extraction assumptions; This combined method can inherit most of the properties from the underlying proof system. We note that our scriptable SNARK system is more efficient.

The second approach is based on the hardness of the DLP, originally proposed by Groth [29] and then implemented in [9,12]. Note that, the communication complexity in the DLP approach is logarithmic. However, the verifier complexity in this approach is not scalable.

The third approach is based on efficient Interactive Proofs (IP) [27,50].

The line of realizations can be found in [62] and [57].

Note that, the verifier in this approach is not scalable.

The fourth approach is via the so-called “MPC in the head”, originally suggested by Ishai et al. [33] and then implemented in ZKBoo [25], and in Ligero [1].

“MPC in the head” based systems have a non-scalable verifier; in addition, communication complexity is non-scalable.

Not all the existing works can be classified like paragraphs above. Bootle et al. propose a scheme that based on ideal linear commitment (ILC) model where a prover can commit to vectors by sending them to a channel, and a verifier can query the channel on linear combinations of the committed vectors [10]. Baum et al. introduce the first lattice based protocol with sublinear communication costs [2]. A recent proposal called STARK [4], attempts to simultaneously minimize proof size and verifier computation. However, their proof sizes are not small. In [30,44], an updatable and universal reference string is used. The main goals of this approach is to address risks surrounding setups and many other security challenges in practice. It does not improve the efficiency.

Another method to achieve universal setup is using universal circuit [40,41]. In [5,7], a TinyRAM architecture is used to describe universal computations as simple programs. A universal circuit is built based on a specific universal language (i.e., a set of tuples, where each tuple consists of a TinyRAM program, an input string, and a time-bound to run the program). Unfortunately, this approach incur a large overhead on the prover computation.

NIZK in the UC framework. Groth et al. proposed the first UC-secure NIZK argument for any NP language in the presence of an adaptive adversary [31]. In [31], the simulator is allowed to generate the encryption key/decryption key pair, and encrypts message that relates to the witness. Thus the simulator has the chance of extracting the witness. Since then, a lot of research work has been done to construct the UC-secure NIZK protocol, such as [15]. Kosba et al. has even made an attempt on building a framework for UC-secure NIZK proofs [37]. However, to the best of our knowledge, all of these protocols do not achieve succinctness.

Trusted hardware. Many previous works have proposed using trusted hardware to build cryptographic algorithms and systems, including protection of cryptographic keys [45], functional encryption [22], digital rights management [21], map-reduce jobs [46,54], machine learning [47], data analysis [51], and protecting unmodified Windows applications [3]. Of course, people have used trusted hardware to build NIZK proof system. More precisely, Tramer et al. introduced sealed-glass proof in [53], where the authors try to explore some use cases even if the isolated execution environment has unbounded leakage, i.e., arbitrary side-channels. We note that there are two main difference between their work and ours: interactiveness and scriptability. In particular, their primitive is interactive, thus not scalable; in their protocol, for each verification, the trusted hardware must be interacted with. Our primitive is non-interactive, and in our construction, the verifier can verify the proof without interacting with the trusted hardware. Most importantly, ours is the first work to investigate scriptable SNARK, which is developer-friendly.

9. Conclusion

In this work, we introduce a new notion called scriptable SNARK proof system. We formally model this notion in the UC framework. We then propose a generic scriptable SNARK solution based on trusted hardware. We also instantiated our scheme in both Intel SGX and Arm TrustZone. To the best of our knowledge, the proposed scriptable SNARK is better than all the existing succinct SNARK proof systems w.r.t. the prover running time (1000 times faster for Lua script, 10000 times faster for Native C), the verifier’s running time (10 times faster), and the proof size (10 times smaller). In addition, we also propose a scriptable SNARK solution based on lightweight trusted hardware. Most importantly, our SNARK proof system can be readily deployed and used by any developers without the need of cryptographic background.

References

Ames,

Hazay,

Ishai and

Venkitasubramaniam, Ligero: Lightweight sublinear arguments without a trusted setup, in: ACM CCS 2017,

B.M.

Thuraisingham,

Evans,

Malkin and

Xu, eds, ACM Press, 2017, pp. 2087–2104.

Baum,

Bootle,

Cerulli,

Del Pino,

Groth and

Lyubashevsky, Sub-linear lattice-based zero-knowledge arguments for arithmetic circuits, in: Annual International Cryptology Conference, Springer, 2018, pp. 669–699.

Baumann,

Peinado and

Hunt, Shielding applications from an untrusted cloud with haven, ACM Transactions on Computer Systems (TOCS)33(3) (2015), 8. doi:10.1145/2799647.

Ben-Sasson,

Bentov,

Horesh and

Riabzev, Scalable, transparent, and post-quantum secure computational integrity, Cryptology ePrint Archive, Report 2018/046, 2018.

Ben-Sasson,

Chiesa,

Genkin,

Tromer and

Virza, SNARKs for C: Verifying program executions succinctly and in zero knowledge, in: CRYPTO 2013, Part II,

Canetti and

J.A.

Garay, eds, LNCS, Vol. 8043, Springer, Heidelberg, 2013, pp. 90–108. doi:10.1007/978-3-642-40084-1_6.

Ben-Sasson,

Chiesa,

Riabzev,

Spooner,

Virza and

N.P.W.

Aurora, Transparent succinct arguments for r1cs, in: Annual International Conference on the Theory and Applications of Cryptographic Techniques, Springer, 2019, pp. 103–128.

Ben-Sasson,

Chiesa,

Tromer and

Virza, Succinct non-interactive zero knowledge for a von Neumann architecture, in: USENIX Security 2014,

Fu and

Jung, eds, USENIX Association, 2014, pp. 781–796.

Blum,

Feldman and

Micali, Non-interactive zero-knowledge and its applications (extended abstract), in: 20th ACM STOC, ACM Press, 1988, pp. 103–112.

Bootle,

Cerulli,

Chaidos,

Groth and

Petit, Efficient zero-knowledge arguments for arithmetic circuits in the discrete log setting, in: EUROCRYPT 2016, Part II,

Fischlin and

J.-S.

Coron, eds, LNCS, Vol. 9666, Springer, Heidelberg, 2016, pp. 327–357. doi:10.1007/978-3-662-49896-5_12.

10.

Bootle,

Cerulli,

Ghadafi,

Groth,

Hajiabadi and

S.K.

Jakobsen, Linear-time zero-knowledge proofs for arithmetic circuit satisfiability, in: International Conference on the Theory and Application of Cryptology and Information Security, Springer, 2017, pp. 336–365.

11.

Brickell and

Li, Enhanced privacy id from bilinear pairing for hardware authentication and attestation, in: 2010 IEEE Second International Conference on Social Computing, 2010, pp. 768–775. doi:10.1109/SocialCom.2010.118.

12.

Bünz,

Bootle,

Boneh,

Poelstra,

Wuille and

Maxwell, Bulletproofs: Short proofs for confidential transactions and more, in: 2018 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2018, pp. 315–334. doi:10.1109/SP.2018.00020.

13.

Canetti, Universally composable security: A new paradigm for cryptographic protocols, Cryptology ePrint Archive, Report 2000/067, 2000.

14.

Canetti, Universally composable security: A new paradigm for cryptographic protocols, in: 42nd FOCS, IEEE Computer Society Press, 2001, pp. 136–145.

15.

Canetti,

Sarkar and

Wang, Triply adaptive uc nizk, IACR Cryptol. ePrint Arch.2020 (2020), 1212.

16.

Chen,

Xiao,

Zhang,

Lin and

Ten Lai, Sgxpectre attacks: Stealing intel secrets from sgx enclaves via speculative execution, 2018.

17.

Cheng,

Zhang,

Kos,

He,

Hynes,

Johnson,

Juels,

Miller and

Song, Ekiden: A platform for confidentiality-preserving, trustworthy, and performant smart contracts.

18.

Costan and

Devadas, Intel sgx explained, Cryptology ePrint Archive, Report 2016/086, 2016.

19.

Danezis,

Fournet,

Groth and

Kohlweiss, Square span programs with applications to succinct NIZK arguments, in: ASIACRYPT 2014, Part I,

Sarkar and

Iwata, eds, LNCS, Vol. 8873, Springer, Heidelberg, 2014, pp. 532–550.

20.

ECRYPT. ebacs: Ecrypt benchmarking of cryptographic systems. https://bench.cr.yp.to/results-hash.html, 2018. Last accessed: 2019-05-11.

21.

Edward Suh,

Clarke,

Gassend,

Van Dijk and

Devadas, Aegis: Architecture for tamper-evident and tamper-resistant processing, in: ACM International Conference on Supercomputing 25th Anniversary Volume, ACM, 2014, pp. 357–368.

22.

Fisch,

Vinayagamurthy,

Boneh and

Gorbunov, IRON: Functional encryption using intel SGX, in: ACM CCS 2017,

B.M.

Thuraisingham,

Evans,

Malkin and

Xu, eds, ACM Press, 2017, pp. 765–782.

23.

Gennaro,

Gentry,

Parno and

Raykova, Quadratic span programs and succinct NIZKs without PCPs, in: EUROCRYPT 2013,

Johansson and

P.Q.

Nguyen, eds, LNCS, Vol. 7881, Springer, Heidelberg, 2013, pp. 626–645. doi:10.1007/978-3-642-38348-9_37.

24.

Gentry and

Wichs, Separating succinct non-interactive arguments from all falsifiable assumptions, in: 43rd ACM STOC,

Fortnow

S.P.

Vadhan, ed., ACM Press, 2011, pp. 99–108.

25.

Giacomelli,

Madsen and

Orlandi, ZKBoo: Faster zero-knowledge for boolean circuits, Cryptology ePrint Archive, Report 2016/163, 2016.

26.

Goldreich and

Oren, Definitions and properties of zero-knowledge proof systems, Journal of Cryptology7(1) (1994), 1–32. doi:10.1007/BF00195207.

27.

Goldwasser,

Tauman Kalai and

G.N.

Rothblum, Delegating computation: Interactive proofs for muggles, in: 40th ACM STOC,

R.E.

Ladner and

Dwork, eds, ACM Press, 2008, pp. 113–122.

28.

Groth, Fully anonymous group signatures without random oracles, in: ASIACRYPT 2007,

Kurosawa, ed., LNCS, Vol. 4833, Springer, Heidelberg, 2007, pp. 164–180. doi:10.1007/978-3-540-76900-2_10.

29.

Groth, Efficient zero-knowledge arguments from two-tiered homomorphic commitments, in: ASIACRYPT 2011,

Hoon Lee and

Wang, eds, LNCS, Vol. 7073, Springer, Heidelberg, 2011, pp. 431–448. doi:10.1007/978-3-642-25385-0_23.

30.

Groth,

Kohlweiss,

Maller,

Meiklejohn and

Miers, Updatable and universal common reference strings with applications to zk-SNARKs, in: CRYPTO 2018, Part III,

Shacham and

Boldyreva, eds, LNCS, Vol. 10993, Springer, Heidelberg, 2018, pp. 698–728. doi:10.1007/978-3-319-96878-0_24.

31.

Groth,

Ostrovsky and

Sahai, Perfect non-interactive zero knowledge for np, in: Annual International Conference on the Theory and Applications of Cryptographic Techniques, Springer, 2006, pp. 339–358.

32.

Ishai,

Kushilevitz and

Ostrovsky, Efficient arguments without short pcps, in: Twenty-Second Annual IEEE Conference on Computational Complexity (CCC’07), 2007, pp. 278–291. doi:10.1109/CCC.2007.10.

33.

Ishai,

Kushilevitz,

Ostrovsky and

Sahai, Zero-knowledge from secure multiparty computation, in: 39th ACM STOC,

D.S.

Johnson and

Feige, eds, ACM Press, 2007, pp. 21–30.

34.

S.P.

Johnson,

V.R.

Scarlata,

C.V.

Rozas,

Brickell and

McKeen, Intel sgx: Epid provisioning and attestation services, Intel (2016).

35.

Juels,

A.E.

Kosba and

Shi, The ring of Gyges: Investigating the future of criminal smart contracts, in: ACM CCS 2016,

E.R.

Weippl,

Katzenbeisser,

Kruegel,

A.C.

Myers and

Halevi, eds, ACM Press, 2016, pp. 283–295.

36.

Kiayias,

Miller and

Zindros, Non-interactive proofs of proof-of-work, Cryptology ePrint Archive, Report 2017/963, 2017.

37.

Kosba,

Zhao,

Miller,

Qian,

Chan,

Papamanthou,

Pass,

Shelat and

Shi, C∅c∅: A framework for building composable zero-knowledge proofs, Cryptology ePrint Archive, Report 2015/1093, 2015.

38.

A.E.

Kosba,

Miller,

Shi,

Wen and

C.P.

Hawk, The blockchain model of cryptography and privacy-preserving smart contracts, in: 2016 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2016, pp. 839–858. doi:10.1109/SP.2016.55.

39.

Lee,

M.-W.

Shih,

Gera,

Kim,

Kim and

Peinado, Inferring fine-grained control flow inside sgx enclaves with branch shadowing, in: USENIX Security, USENIX Association, 2017.

40.

G.V.

Leslie, Universal circuits (preliminary report), in: Proceedings of the Eighth Annual ACM Symposium on Theory of Computing, STOC ’76, ACM, New York, NY, USA, 1976, pp. 196–203.

41.

Lipmaa,

Mohassel and

Sadeghian, Valiant’s universal circuit: Improvements, implementation, and applications, Cryptology ePrint Archive, Report 2016/017, 2016.

42.

Lipp,

Gruss,

Spreitzer,

Maurice and

Mangard, ARMageddon: Cache attacks on mobile devices, in: USENIX Security 2016,

Holz and

Savage, eds, USENIX Association, 2016, pp. 549–564.

43.

Luu,

Teutsch,

Kulkarni and

Saxena, Demystifying incentives in the consensus computer, in: ACM CCS 2015,

Ray,

Li and

Kruegel, eds, ACM Press, 2015, pp. 706–719.

44.

Maller,

Bowe,

Kohlweiss and

Meiklejohn, Sonic: Zero-knowledge snarks from linear-size universal and updateable structured reference strings, IACR Cryptology ePrint Archive2019 (2019), 99.

45.

J.M.

McCune,

B.J.

Parno,

Perrig,

M.K.

Reiter and

Isozaki, Flicker: An execution infrastructure for tcb minimization, in: ACM SIGOPS Operating Systems Review, Vol. 42, ACM, 2008, pp. 315–328.

46.

Ohrimenko,

Costa,

Fournet,

Gkantsidis,

Kohlweiss and

Sharma, Observing and preventing leakage in MapReduce, in: ACM CCS 2015,

Ray,

Li and

Kruegel, eds, ACM Press, 2015, pp. 1570–1581.

47.

Ohrimenko,

Schuster,

Fournet,

Mehta,

Nowozin,

Vaswani and

Costa, Oblivious multi-party machine learning on trusted processors, in: USENIX Security 2016,

Holz and

Savage, eds, USENIX Association, 2016, pp. 619–636.

48.

Parno,

Howell,

Gentry and

Raykova, Pinocchio: Nearly practical verifiable computation, in: 2013 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2013, pp. 238–252. doi:10.1109/SP.2013.47.

49.

Pires,

Gavril,

Felber,

Onica and

Pasin, A lightweight mapreduce framework for secure processing with sgx, in: Proceedings of the 17th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing, CCGrid ’17, IEEE Press, Piscataway, NJ, USA, 2017, pp. 1100–1107.

50.

Reingold,

G.N.

Rothblum and

R.D.

Rothblum, Constant-round interactive proofs for delegating computation, in: 48th ACM STOC,

Wichs and

Mansour, eds, ACM Press, 2016, pp. 49–62.

51.

Schuster,

Costa,

Fournet,

Gkantsidis,

Peinado,

Mainar-Ruiz and

Russinovich, VC3: Trustworthy data analytics in the cloud using SGX, in: 2015 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2015, pp. 38–54. doi:10.1109/SP.2015.10.

52.

SCIPR Lab, 2019, libsnark: A c++ library for zksnark proofs.

53.

Tramer,

Zhang,

Lin,

Hubaux,

Juels and

Shi, Sealed-glass proofs: Using transparent enclaves to prove and sell knowledge, in: Euro S&P 2017, 2017, pp. 19–34.

54.

Tuan,

Dinh,

Saxena,

E.-C.

Chang,

Chin Ooi and

Zhang, M2R: Enabling stronger privacy in MapReduce computation, in: USENIX Security 2015,

Jung and

Holz, eds, USENIX Association, 2015, pp. 447–462.

55.

Valiant, Incrementally verifiable computation or proofs of knowledge imply time/space efficiency, in: TCC 2008,

Canetti, ed., LNCS, Vol. 4948, Springer, Heidelberg, 2008, pp. 1–18.

56.

Van Bulck,

Minkin,

Weisse,

Genkin,

Kasikci,

Piessens,

Silberstein,

T.F.

Wenisch,

Yarom and

Strackx, Foreshadow: Extracting the keys to the intel sgx kingdom with transient out-of-order execution, in: USENIX Security Symposium, 2018.

57.

R.S.

Wahby,

Tzialla,

Shelat,

Thaler and

Walfish, Doubly-efficient zkSNARKs without trusted setup, in: 2018 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2018, pp. 926–943. doi:10.1109/SP.2018.00060.

58.

Weichbrodt,

Kurmus,

P.R.

Pietzuch and

Kapitza, Asyncshock: Exploiting synchronisation bugs in intel SGX enclaves, in: ESORICS 2016, 2016, pp. 440–457.

59.

Xu,

Cui and

Peinado, Controlled-channel attacks: Deterministic side channels for untrusted operating systems, in: Proceedings of the 2015 IEEE Symposium on Security and Privacy, SP ’15, IEEE Computer Society, 2015, pp. 640–656. doi:10.1109/SP.2015.45.

60.

Zhang,

Chen,

Li,

Zhou,

Thai,

H.-S.

Zhou and

Ren, Succinct scriptable nizk via trusted hardware, in: European Symposium on Research in Computer Security, Springer, 2021, pp. 430–451.

61.

Zhang,

Cecchetti,

Croman,

Juels and

Shi, Town crier: An authenticated data feed for smart contracts, in: ACM CCS 2016,

E.R.

Weippl,

Katzenbeisser,

Kruegel,

A.C.

Myers and

Halevi, eds, ACM Press, 2016, pp. 270–282.

62.

Zhang,

Genkin and

Katz,

Papadopoulos,

Papamanthou, vSQL: Verifying arbitrary SQL queries over dynamic outsourced databases, in: 2017 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 2017, pp. 863–880. doi:10.1109/SP.2017.43.

Scriptable and composable SNARKs in the trusted hardware model 1

Abstract

Keywords

1. Introduction

1.1. Our design goals

1.2. Our approach

1.3. Implementation

2. Preliminaries

2.1. Trusted execution environment

2.2. NIZK proof/argument systems

2.3. Universal composibility

6.1. O HW Q implementation

4 The connection time with IAS varies, depending on the region and country. The experiment is tested on a Linode cloud server at Fremont, California, US.

9. Conclusion

References

6.1. $O_{HW}^{Q}$ implementation

⁴
The connection time with IAS varies, depending on the region and country. The experiment is tested on a Linode cloud server at Fremont, California, US.