Aurélien Havet

Rafael Pires

Pascal Felber

Marcelo Pasin

Romain Rouvoy

Valerio Schiavoni

SecureStreams: A Reactive Middleware Framework for Secure Data Stream Processing

The growing adoption of distributed data processing frameworks in a wide diversity of application domains challenges end-to-end integration of properties like security, in particular when considering deployments in the context of large-scale clusters or multi-tenant Cloud infrastructures.

This paper therefore introduces SecureStreams, a reactive middleware framework to deploy and process secure streams at scale. Its design combines the highlevel reactive dataflow programming paradigm with In-tel®'s low-level software guard extensions (SGX) in order to guarantee privacy and integrity of the processed data. The experimental results of SecureStreams are promising: while offering a fluent scripting language based on Lua, our middleware delivers high processing throughput, thus enabling developers to implement secure processing pipelines in just few lines of code.

Introduction

The data deluge imposed by a world of ever-connected devices, whose most emblematic example is the Internet of Things (IoT), has fostered the emergence of novel data analytics and processing technologies to cope with the ever increasing volume, velocity, and variety of information that characterize the big data era. In particular, to support the continuous flow of information gathered by millions of IoT devices, data streams have emerged as a suitable paradigm to process flows of data at scale. However, as some of these data streams may convey sensitive information, stream processing requires support for end-to-end security guarantees in order to prevent third parties accessing restricted data.

This paper therefore introduces SecureStreams, our initial work on a middleware framework for developing and deploying secure stream processing on untrusted distributed environments. SecureStreams supports the implementation, deployment, and execution of stream processing tasks in distributed settings, from large-scale clusters to multi-tenant Cloud infrastructures. More specifically, SecureStreams adopts a message-oriented [START_REF] Curry | Message-Oriented Middleware[END_REF] middleware, which integrates with the SSL protocol [START_REF] Freier | The secure sockets layer (SSL) protocol version 3[END_REF] for data communication and the current version of Intel®'s software guard extensions (SGX) [START_REF] Costan | Intel® SGX explained[END_REF] to deliver end-to-end security guarantees along data stream processing stages. Se-cureStreams can scale vertically and horizontally by adding or removing processing nodes at any stage of the pipeline, for example to dynamically adjust according to the current workload. The design of the Se-cureStreams system is inspired by the dataflow programming paradigm [START_REF] Uustalu | The Essence of Dataflow Programming[END_REF]: the developer combines together several independent processing components (e.g., mappers, reducers, sinks, shufflers, joiners) to compose specific processing pipes. Regarding packaging and deployment, SecureStreams smoothly integrates with industrial-grade lightweight virtualization technologies like Docker [START_REF] Docker | [END_REF].

In this paper, we propose the following contributions: (i) we describe the design of SecureStreams, (ii) we provide details of our reference implementation, in particular on how to smoothly integrate our runtime inside an SGX enclave, and (iii) we perform an extensive evaluation with micro-benchmarks, as well as with a realworld dataset.

The remainder of the paper is organized as follows. To better understand the design of SecureStreams, Section 2 delivers a brief introduction to today's SGX operating mechanisms. The architecture of Secure-Streams is then introduced in Section 3. Our implementation choices and an example of a Secure-Streams program are reported in Section 4. Section 5 discusses our extensive evaluation, presenting a detailed analysis of micro-benchmark performances, as well as more comprehensive macro-benchmarks with real-world datasets. Some related works to this topic are gathered in Section 6. Finally, Section 7 briefly describes our future work and concludes.

SGX Lightning Tour

The design of SecureStreams revolves around the availability of SGX features in the host machines. It consists in a trusted execution environment (TEE) recently introduced into Intel® SkyLake, similar in spirit to ARM TrustZone [START_REF]Building a Secure System using[END_REF] but much more powerful. Applications create secure enclaves to protect the integrity and the confidentiality of the data and the code being executed.

The SGX mechanism, as depicted in Figure 1, al- lows applications to access confidential data from inside the enclave. The architecture guarantees that an attacker with physical access to a machine will not be able to tamper with the application data without being noticed. The CPU package represents the security boundary. Moreover, data belonging to an enclave is automatically encrypted and authenticated when stored in main memory. A memory dump on a victim's machine will produce encrypted data. A remote attestation protocol allows one to verify that an enclave runs on a genuine Intel® processor with SGX. An application using enclaves must ship a signed (not encrypted) shared library (a shared object file in Linux) that can possibly be inspected by malicious attackers.

In the current version of SGX, the enclave page cache (EPC) is a 128 MB area of memory 1 predefined at boot to store enclaved code and data. At most around 90 MB can be used by application's memory pages, while the remaining area is used to maintain SGX metadata. Any access to an enclave page that does not reside in the EPC triggers a page fault. The SGX driver interacts with the CPU to choose which pages to evict. The traffic between the CPU and the system memory is kept confidential by the memory encryption engine (MEE) [START_REF] Gueron | A Memory Encryption Engine Suitable for General Purpose Processors[END_REF], also in charge of tamper resistance and replay protection. If a cache miss hits a protected region, the MEE encrypts or decrypts data before sending to, respectively fetching from, the system memory and performs integrity checks. Data can also be persisted on stable storage protected by a seal key. This allows the storage of certificates, waiving the need of a new remote attestation every time an enclave application restarts.

The execution flow of a program using SGX enclaves is like the following. First, an enclave is created (see Figure 1-). As soon as a program needs to execute a trusted function (), it executes SGX's primitive ecall (). The call goes through the SGX call gate to bring the execution flow inside the enclave (). Once the trusted function is executed by one of the enclave's threads (), its result is encrypted and sent back () before giving back the control to the main processing thread ().

1 Future releases of SGX might relax this limitation [START_REF] Mckeen | Intel® software guard extensions (intel® sgx) support for dynamic memory management inside an enclave[END_REF].

Architecture

The architecture of SecureStreams comprises a combination of two different types of base components: worker and router. A worker component continuously listens for incoming data by means of non-blocking I/O. As soon as data flows in, an application-dependent business logic is applied. A typical use-case is the deployment of a classic filter/map/reduce pattern from the functional programming paradigm [START_REF] Bird | Introduction to Functional Programming[END_REF]. In such a case, worker nodes execute only one function, namely map, filter, or reduce. A router component acts as a message broker between workers in the pipeline and transfers data between them according to a given dispatching policy. SecureStreams is designed to support the processing of sensitive data inside SGX enclaves. As explained in the previous section, the enclave page cache (EPC) is currently limited to 128 MB . To overcome this limitation, we settled on a lightweight yet efficient embeddable runtime, based on the Lua virtual machine (LuaVM) [START_REF] Ierusalimschy | Lua-An Extensible Extension Language[END_REF] and the corresponding multi-paradigm scripting language [START_REF] Lua | [END_REF]. The Lua runtime requires only few kilobytes of memory, it is designed to be embeddable, and as such it represents an ideal candidate to execute in the limited space allowed by the EPC. Moreover, the application-specific functions can be quickly prototyped in Lua, and even complex algorithms can be implemented with an almost 1:1 mapping from pseudocode [START_REF] Leonini | Splay: Distributed systems evaluation made simple (or how to turn ideas into live systems in a breeze)[END_REF]. We provide further implementation details of the embedding of the LuaVM inside an SGX enclave in Section 4.

Each component is wrapped inside a lightweight Linux container (in our case, the de facto industrial standard Docker [START_REF] Docker | [END_REF]). Each container embeds all the required dependencies, while guaranteeing the correctness of their configuration, within an isolated and reproducible execution environment. By doing so, a Secure-Streams processing pipeline can be easily deployed without changing the source code on different public or private infrastructures. For instance, this will allow developers to deploy SecureStreams to Amazon EC2 container service [START_REF]Amazon EC2 Container Service[END_REF], where SkyLake-enabled instances will soon be made available [START_REF]Amazon EC2 and SkyLake CPUs[END_REF], or similarly to Google compute engine [START_REF]Google Compute Engine and SkyLake CPUs[END_REF]. The deployment of the containers can be transparently executed on a single machine or a cluster, using a Docker network and the Docker Swarm scheduler [START_REF] Swarm | [END_REF].

The communication between workers and routers leverages ZeroMQ, a high-performance asynchronous messaging library [START_REF]ZeroMQ[END_REF]. Each router component hosts inbound and outbound queues. In particular, the routers use the ZeroMQ's pipeline pattern [START_REF]ZeroMQ Pipeline[END_REF] with the Push-Pull socket types.

The inbound queue is a Pull socket. The messages are streamed from a set of anonymous2 Push peers (e.g., the upstream workers in the pipeline). The inbound queue uses a fair-queuing scheduling to deliver the message to the upper layer. Conversely, the outbound queue is a Push socket, sending messages using a round-robin algorithm to a set of anonymous Pull peers-e.g., the downstream workers. This design allows us to dynamically scale up and down each stage of the pipeline in order to adapt it to application's needs or the workload. Finally, ZeroMQ guarantees that the messages are delivered across each stage via reliable TCP channels.

We define the processing pipeline components and their chaining by means of Docker's Compose [START_REF] Comopse | [END_REF] description language. Listing 1 reports on a snippet of the description used to deploy the architecture in Figure 2. Once the processing pipeline is defined, the containers must be deployed on the computing infrastructure. We exploit the constraint placement mechanisms to enforce the Docker Swarm's scheduler in order to deploy workers requiring SGX capabilities into appropriate hosts. In the example, an sgx mapper nodes is deployed on an SGX host by specifying "constraint:type==sgx" in the Compose description.

1 sgx_mapper :

2 image : " $ { IMAGE_SGX } "

Implementation Details

SecureStreams is implemented in Lua (v5.3). The implementation of the middleware itself requires careful engineering, especially with respect to the integration in the SGX enclaves (explained later). However, a Se-cureStreams use-case can be implemented in remarkably few lines of code. For instance, the implementation of the map/filter/reduce accounts for only 120 lines of code (without counting the dependencies). The framework partially extends RxLua [START_REF]Reactive Extensions for Lua[END_REF], a library for reactive programming in Lua. RxLua provides to the developer the required API to design a data stream processing pipeline following a dataflow programming pattern [START_REF] Uustalu | The Essence of Dataflow Programming[END_REF].

Listing 2 provides an example of a RxLua program (and consequently a SecureStreams program) to compute the average age of a population by chaining :map, :filter, and :reduce functions. 3 The :subscribe function performs the subscription of 3 functions to the data stream. Following the observer design pattern [START_REF] Szallies | On using the observer design pattern[END_REF], these functions are observers, while the data stream is an observable. SecureStreams dynamically ships the business logic for each component into a dedicated Docker container and executes it. The communication between the Docker containers (the router and the worker components) happens through ZeroMQ (v4.1.2) and the corresponding Lua bindings [START_REF]Lua binding to ZeroMQ[END_REF]. Basically, Secure-Streams abstracts the underlying network and computing infrastructure from the developer, by relying on ZeroMQ and Docker.

Under the SGX threat model where the system software is completely untrusted, system calls are not allowed inside secure enclaves. As a consequence, porting a legacy application or runtime, such as the Lua interpreter, is challenging. To achieve this task, we traced all system calls made by the interpreter to the standard C library and replaced them by alternative implementations that either mimic the real behavior or discard the call. Our changes to the vanilla Lua source code consist of the addition of about 600 lines of code, or 2.5 % of its total size. By doing so, Lua programs operating on files, network sockets or any other input/output device do not execute as they normally do outside the enclaves. This inherent SGX limitation also reinforces the system security guarantees offered to the application developers. The SecureStreams framework safely ships the data and code to enclaves. Hence, the Lua scripts executed within the SGX enclave do not use (read/write) files or sockets. Wrapper functions are nevertheless installed in the SGX-enabled LuaVM to prevent any of such attempts.

An additional constraint imposed by the secure SGX enclaves is the impossibility of dynamically linking code. The reason is that the assurance that a given code is running inside a SGX-enabled processor is made through the measurement of its content when the enclave is created. More specifically, this measurement is the result of EREPORT instruction, an SGX-specific report that computes a cryptographically secure hash of code, data and a few data structures, which overall builds a snapshot of the state of the enclave (including threads, memory heap size, etc.) and the processor (security version numbers, keys, etc.). Allowing more code to be linked dynamically at runtime would break the assurance given by the attestation mechanism on the integrity of the code being executed, allowing for example an attacker to load a malicious library inside the enclave.

In the case of Lua, a direct consequence is the impossibility of loading Lua extensions using the traditional dynamic linking technique. Every extension has to be statically compiled and packed with the enclave code. To ease the development of SecureStreams applications, we statically compiled json [START_REF]The JavaScript Object Notation (JSON) Data Interchange Format[END_REF], and csv [START_REF] Shafranovich | Common Format and MIME Type for Comma-Separated Values (CSV) Files[END_REF] parsers within our enclaved Lua interpreter. With these libraries, the size of the VM and the complete runtime still remains reasonably small, approximately 220 KB (19 % larger than the original).

While this restricted Lua has been adapted to run inside SGX enclaves, we still had to provide a support for communications and the reactive streams framework itself. To do so, we use an external vanilla Lua interpreter, with a couple adaptations that allowed the interaction with the SGX enclaves and the LuaVM therein. Figure 3 shows the resulting architecture. We extend the Lua interface with 3 functions: sgxprocess, sgxencrypt, and sgxdecrypt. The first one forwards the encrypted code and data to be processed in the enclave, while the remaining two provide cryptographic functionalities. In this work, we assume that attestation and key establishment was previously performed. As a result, keys safely reside within the enclave. We plan to release our implementation as open-source. 4

Evaluation

This section reports on our extensive evaluation of Se-cureStreams. First, we present our evaluation settings. Then, we describe the real-world dataset used in our macro-benchmark experiments. We then dig into a set of micro-benchmarks that evaluate the overhead of running the LuaVM inside the SGX enclaves. Finally, we deploy a full SecureStreams pipeline, scaling the number of workers per stage, to study the limits of the system in terms of throughput and scalability.

Evaluation Settings

We have experimented on machines using a Intel® Core™ i7-6700 processor [START_REF]Intel® Core™ i[END_REF] and 8 GiB RAM. We use a cluster of 2 machines based on Ubuntu 14.04.1 LTS (kernel 4.2.0-42-generic). The choice of the Linux distribution is driven by compatibility reasons with the Intel® SGX SDK (v1.6). The machines run Docker (v1.13.0) and each node joins a Docker Swarm [START_REF] Swarm | [END_REF] (v1.2.5) using the Consul [START_REF] Consul | [END_REF] (v0.5.2) discovery service. The Swarm manager and the discovery service are deployed on a distinct machine. Containers building the pipeline leverage the Docker overlay network to communicate to each other, while machines are physically interconnected using a switched 1 Gbps network.

Input Dataset

In our experiments, we process a real-world dataset released by the American Bureau of Transportation Statistics [START_REF] Bts | [END_REF]. The dataset reports on the flight departures and arrivals of 20 air carriers [START_REF]Data Expo'09 ASA Statistics Computing and Graphics[END_REF]. We implement a benchmark application atop of SecureStreams to compute average delays and the total of delayed flights for each air carrier (cf. Table 1). We design and implement the full processing pipeline, that (i) parses the input datasets (in a comma-separated-value format) to data structure (map), (ii) filters data by relevancy (i.e., if the data concerns a delayed flight), and (iii) finally reduces it to compute the desired information. 5 We use the 4 last years of the available dataset (from 2005 to 2008), for a total of 28 millions of entries to process and 2.73 GB of data.

Micro-Benchmark: Lua in SGX

We begin our evaluation with a set of micro-benchmarks to evaluate performance of the integration of the LuaVM inside the SGX enclaves. First, we estimate the cost of execution for functions inside the enclave. This test averages the execution time of 1 million function calls, without any data transfer. We compare against the same result without SGX. While non-enclaved function calls took 23.6 ns, the performances inside the enclave drop down to on average 2.35 s-i.e., approximately two orders of magnitude worse. We then assess the cost of copying data from the unshielded execution to the enclave and we compare it with the time required to compute the same on the native system. We initialize a buffer of 100 MB with random data and copy its content inside the enclave. The data is split into chunks of increasing sizes. Our test executes one function call to transfer each chunk, until all data is transfered. Each point in the plot corresponds to the average of 20 runs. Correctness of the copies was verified by SHA256 digest comparison between reproduced memory areas.

Figure 4 shows the results for 4 different variants, comparing the native and the SGX version to only copy the data inside the enclave (in) or to copy it inside and copying it back (in/out). When using smaller chunks, the function call overhead plays an important role in the total execution time. Moreover, we notice that the call overhead steadily drops until the chunk size reaches the size of 64 KB (vertical line). We can also notice that copying data back to non-SGX execution imposes an overhead of at most 20 % when compared to the oneway copy. These initial results are used as guidelines to drive the configuration of the streaming pipeline, in particular with respect to the size of the chunks exchanged between the processing stages. The larger the chunks, the smaller the overhead induced by the transfer of data within the SGX enclave.

Once the data and the code are copied inside the enclave, the LuaVM must indeed execute the code before returning the control. Hence, we evaluate here the raw performances of the enclaved SGX LuaVM. We select 6 available benchmarks from a standard suite of tests [START_REF] Friedrich | The impact of meta-tracing on vm design and implementation[END_REF]. We based this choice on their library dependencies (by selecting the most standalone ones) and the number of input/output instructions they execute (selecting those with the fewest I/O). Each benchmark runs 20 times with the same pair of parameters of the original paper, shown in the even and odd lines of Table 2. Figure 5 depicts the total time (average and standard deviation) required to complete the execution of the 6 benchmarks. We use a bar chart plot, where we compare the results of the Native and SGX modes. For each of the 6 benchmarks, we present two bars next to each other (one per executing mode) to indicate the different configuration parameters used. Finally, for the sake of readability, we use a different y-axis scale for the binarytrees case (from 0 to 400 s), on the right-side of the figure.

We note that, in the current version of SGX, it is required to pre-allocate all the memory area to be used by the enclave. The most memory-eager test (binarytrees) used more than 600 MB of memory, hence using the wall clock time comparison would not be fair for smaller tests. In such cases, almost the whole execution time is dedicated to memory allocation. Because of that, we subtracted the allocation time from the measurements of enclave executions, based on the average for the 20 runs. Fluctuations on this measurement produced slight variations in the execution times, sometimes producing the unexpected result of having SGX executions faster than native ones (by at most 3 %). Table 2 lists the parameters along with the maximum amount of memory used and the ratio between runtimes of SGX and Native executions. When the memory usage is low, the ratio between the Native and SGX versions is small-e.g., less than 15 % in our experiments. However, when the amount of memory usage increases, performance drops to almost 5× worse, as reflected in the case of the binarytrees experiment. The smaller the memory usage, the better performance we can obtain from SGX enclaves.

Synthesis.

To conclude this series of microbenchmarks, taming the overhead of secured executions based on SGX requires balancing the size of the chunks transfered to the enclave with the memory usage within this enclave. In the context of stream processing systems, SecureStreams therefore uses reactive programming principles to balance the load within processing stages in order to minimize the execution overhead.

Benchmark: Streaming Throughput

The previous set of experiments allowed us to verify that our design, implementation, and the integration of the LuaVM into the SGX enclaves is sound. Next, we deploy a SecureStreams pipeline which includes mappers, filters and reducers. To measure the achievable throughput of our system, as well the network overhead of our architecture, we deploy the SecureStreams pipeline in 3 different configurations. In each case, the setup of the pipeline architecture, i.e. the creation of the set of containers, has been done in 11 s for the lightest configuration, in 15 s for the heaviest one.

The first configuration allows the streaming framework to blindly bypass the SGX enclaves. Further, it does not encrypt the input dataset before injecting it into the pipeline. This mode operates as the baseline, yet completely unsafe, processing pipeline. The second mode encrypts the dataset but lets the encrypted packets skip the SGX enclaves. This configuration requires the deployers to trust the infrastructure operator. Finally, we deploy a fully secure pipeline, where the input dataset is encrypted and the data processing is operated inside the enclaves. The data nodes inject the dataset, split into 4 equally-sized parts, as fast as possible. We gather bandwidth measurements by exploiting Docker's internal monitoring and statistical module.

The results of these deployments are presented in Figure 6. For each of the mentioned configurations, we also vary the number of workers per stage, from one (Figure d,g), two (Figure 6-b,e,h), or four (the remaining ones.) We use a representation based on stacked percentiles. The white bar at the bottom represents the minimum value, the pale grey on top the maximal value. Intermediate shades of grey represent the 25th-, 50th-, and 75th-percentiles. For instance, in Figure 6-a (our baseline) the median throughput at 200 s into the experiment almost hits 7.5 MB /s, meaning that 50 % of the nodes in that moment are outputting data at 7.5 MB /s or less. The baseline configuration, with only 1 worker per stage, completes in 420 s, with a peak of 12 MB /s. By doubling the number of workers reduces the processing time down to 250 s (Figure 6-d), a speed-up of 41 %. Scaling up the workers to 4 in the baseline configuration (Figure 6-g) did not produce a similar speed-up.

As we start injecting encrypted datasets (Figure 6-b and follow-up configurations with 2 and 4 workers), the processing time almost doubles (795 s). The processing of the dataset is done after the messages are decrypted. We also pay a penalty in terms of overall throughputi.e., the median value rarely exceeds 5 MB /s. On the other hand, now we observe substantial speed-ups when increasing the workers per stage, down to 430 s and 300 s with 2 and 4 workers, respectively.

The deployment of the most secure set of configurations (right-most column of plots in Figure 6) shows that when using encrypted datasets and executing the stream processing inside SGX enclaves one must expect longer processing times and lower throughputs. This is the (expected) price to pay for higher-security guarantees across the full processing pipeline. Nevertheless, one can observe that the more workers the less penalty is imposed by the end-to-end security guarantees provided by SecureStreams.

Benchmark: Workers' Scalability

To conclude our evaluation, we study SecureStreams in terms of scalability. We consider a pipeline scenario similar to Figure 2 with some variations in the number of workers deployed for each stage. We do so to better understand to what extents the underlying container scheduling system can exploit the hardware resources at its disposal. First, we increase the number of workers for each stage of the pipeline, from 1 to 4. For each of the configurations, the experiment is repeated 5 times. We present average and standard deviation of the total completion time to process the full dataset in Figure 7. As expected, we observe ideal speed-up from a configuration using 1 worker to that using 2 workers. However, in the configuration using 4 workers by stage, we do not reach the same acceleration. We explain this because, in this latter case, the number of deployed containers (which equals the sum of input data streams, workers, and routers, hence 20 containers) is greater than the number of physical cores of the hosts (8 for each of the 2 hosts used in our deployment-i.e., 16 cores on our evaluation cluster).

We also study the total completion time while increasing only the number of mapper workers in the first stage of the pipeline (which we identified as the one consuming most resources) from 1 to 16 and maintaining the numbers of filters and reducers in the following stages constant. As in the previous benchmark, the experiment is repeated 5 times for each configuration and we measure the average and standard deviation of the total completion time. Figure 8 presents the results. Here again, we observe ideal speed-up until the number of deployed containers reaches the number of physical cores. Beyond this number, we do not observe further improvements. These two experiments clearly show that the scalability of SecureStreams according the number of deployed workers across the cluster is primarily limited by the total number of physical cores available.

Apart from this scalability limitation, there are other factors that reduce the observed streaming throughput, with or without involving the SGX enclaves. For instance, our throughout experiments highlight that the system does not manage to saturate the available network bandwidth in all cases. We believe this behaviour can be explained by the lack of optimizations in the application logic as well as possible tuning options of the inner ZeroMQ queues.

As part of our future work, we therefore plan to further investigate these effects and to build on this knowledge to only scale the appropriate workers in order to maximize the overall speed-up of the deployed application. In particular, we intend to leverage the elasticity of workers at runtime in order to cope with the memory constraints imposed by SGX and the configuration of the underlying hardware architecture, for each of the available nodes, in order to offer the best performances for secured execution of data stream processing applications built atop of SecureStreams.

Related Work

Spark [START_REF] Zaharia | Discretized streams: Fault-tolerant streaming computation at scale[END_REF] has recently gained a lot of traction as prominent solution to implement efficient stream processing. It leverages Resilient Distributed Datasets (RDD) to provide a uniform view on the data to process. Despite its popularity, Spark only handles unencrypted data and hence does not offer security guarantees. Recent proposals [START_REF] Shah | Data-atrest security for Spark[END_REF] study possible software solutions to overcome this limitation.

Several big industrial players introduced their own stream processing solutions. These systems are mainly used to ingest massive amounts of data and efficiently perform (real-time) analytics. Twitter's Heron [START_REF] Kulkarni | Twitter Heron: Stream Processing at Scale[END_REF], and Google's Cloud DataFlow [START_REF] Akidau | The Dataflow Model: A Practical Approach to Balancing Correctness, Latency, and Cost in Massivescale, Unbounded, Out-of-order Data Processing[END_REF] are two prominent examples. These systems are typically deployed on the provider's premises and are not offered as a service to end-users.

A few dedicated solutions exist today for distributed stream processing using reactive programming. For instance, Reactive Kafka [START_REF]Reactive Streams for Kafka[END_REF] allows stream processing atop of Apache Kafka [START_REF] Kafka | [END_REF][START_REF] Kreps | A distributed messaging system for log processing[END_REF]. These solutions do not, however, support secure execution in a trusted execution environment.

More recently, some open-source middleware frameworks (e.g., Apache Spark [START_REF]Spark Streaming[END_REF], Apache Storm [START_REF]Apache Storm[END_REF], Infinispan [START_REF]Infinispan[END_REF]) introduced APIs to allow developers to quickly set up and deploy stream processing infrastructures. These systems rely on the Java virtual machine (JVM) [START_REF] Lindholm | The Java Virtual Machine Specification: Java SE 8 Edition[END_REF]. However, SGX currently imposes a hard memory limit of 128 MB to the enclaved code and data, at the cost of expensive encrypted memory paging mechanisms and serious performance overheads [START_REF] Pires | Secure content-based routing using intel® software guard extensions[END_REF][START_REF] Brenner | SecureKeeper: Confidential ZooKeeper Using Intel® SGX[END_REF] when this limit is crossed. Moreover, executing a fullyfunctional JVM inside an SGX enclave would currently involve significant re-engineering efforts.

DEFCon [START_REF] Migliavacca | Defcon: High-performance event processing with information security[END_REF] relies also on the JVM. This event processing system focuses on security by enforcing constraints on event flows between processing units. The event flow control is enforced using application-level virtualisation to separate processing units in a ad-hoc JVM.

A few recent contributions tackle privacy-preserving data processing, particularly in a MapReduce scenario. This is the case of Airavat [START_REF] Roy | Airavat: Security and Privacy for MapReduce[END_REF] and Gupt [START_REF] Mohan | GUPT: Privacy Preserving Data Analysis Made Easy[END_REF]. These systems leverage differential-privacy techniques [START_REF] Dwork | Calibrating noise to sensitivity in private data analysis[END_REF] and can face a different threat model than the one supported by SGX and hence by SecureStreams. In particular, when deploying such systems on a public infrastructure, one needs to trust the cloud provider. Our system greatly reduces the trust boundaries, and only requires trust of Intel® and their SGX implementation. Some authors contest that public clouds may be secure enough some parts of an application. They propose to split the jobs, running only the critical parts in private clouds. A privacy-aware framework on hybrid clouds [START_REF] Xu | A framework for privacy-aware computing on hybrid clouds with mixed-sensitivity data[END_REF] has been proposed to work on tagged data, at different granularity levels. A MapReduce preprocessor splits data into private and public clouds according to their sensitivity. Sedic [START_REF] Zhang | Sedic: privacyaware data intensive computing on hybrid clouds[END_REF] does not offer the same tagging granularity, but proposes to automatically modify reducers to optimize the data transfers in a hybrid cloud. These solutions require splitting application and data in two parts (sensitive and not) and impose higher latencies due to data transfers between two different clouds. Yet, they cannot offer better security guarantees that the software stack itself offers, be it public or private.

MrCrypt [START_REF] Sai | Mrcrypt: Static analysis for secure cloud computations[END_REF] proposes using homomorphic encryption instead of trusted elements. Through static code analysis, it pinpoints different homomorphic encryption schemes for every data column. Still, some of the demonstrated benchmarks are ten times slower than the unecrypted execution. SecureStreams avoids of complex encryption schemes, decrypts data entering enclaves and processes in plaintext.

The Styx [START_REF] James Stephen | STYX: Stream Processing with Trustworthy Cloud-based Execution[END_REF] system uses partial homorphic encryption to allow for efficient stream processing in trusted cloud environments. Interestingly, the authors of that system mention Intel® SGX as possible alternative to deploy stream processing systems on trusted hardware offered by untrusted/malicious cloud environments. Se-cureStreams offers insights on the performances of exactly this approach.

To best of our knowledge, SecureStreams is the first lightweight and low-memory footprint stream processing framework that can fully execute within SGX enclaves.

As we described before, SecureStreams is executing processes taking advantage of SGX enclaves inside Docker containers. SCONE [START_REF] Pietzuch | SCONE: Secure Linux Containers with Intel SGX[END_REF], which is not yet openly available, is a recently introduced system that offers a secure container mechanism for Docker to leverage the SGX trusted execution support. It proposes a generic technology to embed any C program to execute inside an SGX enclave. Rather than generic programs, Se-cureStreams offers support to execute a lightweight LuaVM inside an SGX enclave and securely execute chunks of Lua code inside it. In our experiments, we execute this LuaVM inside Docker containers.

Conclusion

Secure stream processing is becoming a major concern in the era of the Internet of Things and big data. This paper introduces our design and evaluation of Secure-Streams, an concise and efficient middleware framework to implement, deploy and evaluate secure stream processing pipelines for continuous data streams. The framework is designed to exploit the SGX trusted execution environments readily available in Intel®'s commodity processors, such as the latest SkyLake. We implemented the prototype of SecureStreams in Lua and based its APIs on the reactive programming approach. Our initial evaluation results based on realworld traces are encouraging, and pave the way for deployment of stream processing systems over sensitive data on untrusted public clouds.

We plan in our future work to further extend and thoroughly evaluate SecureStreams against other known approaches on secure stream processing, like Styx [START_REF] James Stephen | STYX: Stream Processing with Trustworthy Cloud-based Execution[END_REF], MrCrypt [START_REF] Sai | Mrcrypt: Static analysis for secure cloud computations[END_REF] or DEFCon [START_REF] Migliavacca | Defcon: High-performance event processing with information security[END_REF]. In particular, we plan to extend SecureStreams with full automation of container deployments, as well as enriching the framework with a library of standard stream processing operators and efficient yet secure native plugins, to ease the development of complex stream processing pipelines.

Figure 1 :

 1 Figure 1: SGX core operating principles.

  Figure 2 depicts a possible implementation of this dataflow pattern using the SecureStreams middleware.

Figure 2 :

 2 Figure 2: Example of SecureStreams pipeline architecture.

3 5 - 6 - 7 - 8 devices : 9 - 26 -

 5678926 entrypoint : . / start . sh sgx -mapper . lua 4 environment : TO = tcp : // router_mapper_filter : 5557 FROM = tcp : // router_data_mapper : 5556 " constraint : type = = sgx " " / dev / isgx " ro ut er _d at a_ mapper : image : " $ { IMAGE } " hostname : router_data_mapper entrypoint : lua router . lua environment : -TO = tcp : // * : 5556 -FROM = tcp : // * : 5555 -" constraint : type = = sgx " data_stream : image : " $ { IMAGE } " entrypoint : lua data -stream . lua environment : -TO = tcp : // router_data_mapper : 5555 -" constraint : type = = sgx " DATA_FILE = the_stream . csv Listing 1: SecureStreams pipeline examples. Some attributes (volume, networks, env file) are omitted.

Listing 2 :

 2 Example of process pipeline with RxLua.

Figure 3 :

 3 Figure 3: Integration between Lua and Intel® SGX.

Figure 4 :

 4 Figure 4: Execution time to copy 100 MB of memory inside an SGX enclave (in) or to copy it back outside in/out.

Figure 5 :

 5 Figure 5: Enclave versus native running times for Lua benchmarks.

  Streaming throughput. Data in clear text, no SGX, 1 worker per stage. Streaming throughput. Data in clear text, no SGX, 2 workers per stage. Streaming throughput. Encrypted data, no SGX, 2 workers per stage. Streaming throughput. Encrypted data, processing SGX, 2 workers per stage. Upload Throughput (MB/sec) Streaming throughput. Data in clear text, no SGX, 4 workers per stage. Upload Throughput (MB/sec) Streaming throughput. Encrypted data, processing SGX, 4 workers per stage.

Figure 6 :

 6 Figure6: Throughput comparison between normal processing (with cleartext data and no encryption), encrypted data but without enclaves, and with encrypted data and SGX processing. We scale the number of worker nodes per stage from 1 (left-most column), 2 (center colum) and 4 (right-most column).

Figure 7 :

 7 Figure7: Scalability: processing time, average and standard deviation. The experiment is repeated 5 times, with a variation on the number of workers for each stage, each worker using SGX.

  mappers Processing time: Average and standard deviation

Figure 8 :

 8 Figure8: Scalability: processing time, average and standard deviation. The experiment is repeated 5 times, with a variation on the number of mappers SGX, other workers-1 filter worker and 1 reduce worker-do not use SGX.

Table 1 :

 1 Benchmark app based on SecureStreams.

	System layer	Size (LoC)
	DelayedFlights app	86
	SecureStreams library	350
	RxLua runtime	1, 481
	Total	1, 917

Table 2 :

 2 Parameters and memory usage for Lua benchmarks.

		configuration memory	ratio
		parameter	peak	SGX/Native
	dhrystone	50 K	275 KB	1.14
		5 M	275 KB	1.04
	fannkuchredux	10	28 KB	0.99
		11	28 KB	1.04
	nbody	2.5 M	38 KB	0.99
		25 M	38 KB	1.00
	richards	10	106 KB	1.02
		100	191 KB	0.97
	spectralnorm	500	52 KB	1.00
		5 K	404 KB	0.99
	binarytrees	14	25 MB	1.18
		19	664 MB	4.76

Anonymous refers to a peer without any identity: the server socket ignores which worker sent the message.

Note that in our evaluation the code executed by each worker is confined into its own Lua file.

Omitted due to DEBS17 double-blind policy.

This experiment is inspired by Kevin Webber's blog entry diving into Akka streams:https://blog.redelastic.com/ diving-into-akka-streams-2770b3aeabb0.

Acknowledgments

The research leading to these results has received funding from the European Commission, Information and Communication Technologies, H2020-ICT-2015 under grant agreement number 690111 (SecureCloud project). Rafael Pires is also sponsored by CNPq, National Counsel of Technological and Scientific Development, Brazil.


Yackolley Amoussou-Guenou

Bruno Biais

Maria Potop-Butucaru

Sara Tucci-Piergiovanni

Rationals vs Byzantines in Consensus-based Blockchains

In this paper we analyze from the game theory point of view Byzantine Fault Tolerant blockchains when processes exhibit rational or Byzantine behavior. Our work is the first to model the Byzantine-consensus based blockchains as a committee coordination game. Our first contribution is to offer a game-theoretical methodology to analyse equilibrium interactions between Byzantine and rational committee members in Byzantine Fault Tolerant blockchains. Byzantine processes seek to inflict maximum damage to the system, while rational processes best-respond to maximise their expected net gains. Our second contribution is to derive conditions under which consensus properties are satisfied or not in equilibrium. When the majority threshold is lower than the proportion of Byzantine processes, invalid blocks are accepted in equilibrium. When the majority threshold is large, equilibrium can involve coordination failures, in which no block is ever accepted. However, when the cost of accepting invalid blocks is large, there exists an equilibrium in which blocks are accepted iff they are valid.

Introduction

Since the publication of Nakamoto's white paper [START_REF] Nakamoto | Bitcoin: A Peer-to-Peer Electronic Cash System[END_REF] proposing the Proof-of-Work protocol, Bitcoin, thousands of blockchains have been created. At the operational level, a blockchain maintains an evolving list of ordered blocks. Each block consists of one or more transactions that have been verified by the system members. POW blockchains, however, consume excessive amounts of energy. This motivated tremendous efforts to propose alternatives protocols.

Byzantine-consensus based blockchains offer an alternative which has the advantage of being economical and offering strong consistency garanties [START_REF] Anceaume | Blockchain Abstract Data Type[END_REF]. In Byzantine-consensus based blockchains such as HoneyBadger, HotStuff or Tendermint [START_REF] Abraham | Solidus: An incentive-compatible cryptocurrency based on permissionless byzantine consensus[END_REF][START_REF] Amoussou-Guenou | Correctness of tendermint-core blockchains[END_REF][START_REF] Decker | Bitcoin Meets Strong Consistency[END_REF][START_REF] Eyal | Bitcoin-NG: A Scalable Blockchain Protocol[END_REF][START_REF] Kokoris-Kogias | Enhancing Bitcoin Security and Performance with Strong Consistency via Collective Signing[END_REF][START_REF] Miller | The honey badger of bft protocols[END_REF][START_REF] Yin | HotStuff: BFT Consensus in the Lens of Blockchain[END_REF] a subset of deterministically selected processes, executes an instance of PBFT-consensus to decide on the next block to append. These protocols strive to satisfy the following properties: Termination: every non-Byzantine process decides on a value (a block); Agreement: if there is a non-Byzantine process that decides a value B, then all the non-byzantine processes decide B; Validity [START_REF] Crain | Leader/Randomization/Signature)-free Byzantine Consensus for Consortium Blockchains[END_REF]: a decided value by any non-Byzantine process is valid, it satisfies the predefined predicate.

While Byzantine consensus [START_REF] Lamport | The byzantine generals problem[END_REF] is one of the best understood and formalized building blocks in distributed computing, blockchains systems revive this line of research in several respects: First, traditional Byzantine consensus has been analyzed only in systems where processes were either correct (verify their specification) or Byzantine (arbitrarily deviate from their specification). Blockchain systems bring on the scene a third type of player: rational players who take actions only if these actions increase their profits. Understanding the performance and limits of Byzantine-consensus based blockchains with rational players is the goal of the current work. Our focus on rational players is in line with analyses of blockchain systems conducted by economists. Economists, however, have not considered Byzantine participants yet. Thus, our work endeavours to combine and unify computer science and economics approaches. Second, traditional Byzantine consensus analyses have not studied the choice and consequences of the way in which participants are rewarded. In this work we address the case of rewarding only the participants to the consensus.

Our contribution. Our contribution is twofold. First, we offer a methodology to analyse Byzantine consensus based blockchain protocols as a game between rational and Byzantine players. Two key aspects of the game, for rational players, are the cost of blocks verification and the cost of networking. Block verification is crucial since appending non verified blocks may have long term costs (e.g. double spending, collapse of the system etc.). Networking (participating to the agreement protocol by voting in favor of correct blocks) also has tremendous impact on system welfare: If participants don't vote, this can block the system or lead to agreement on invalid blocks. Second, we derive conditions (on the majority threshold necessary for block acceptance, ν, and the proportion of Byzantine processes, f ) under which rational players reach an equilibrium where the consensus properties are guaranteed. Our findings are as follows. When f ≥ ν, invalid blocks are accepted, so that validity is not satisfied. When f < ν, while there exists an equilibrium in which validity and termination are satisfied, there also exists an equilibrium in which blocks are never accepted, so that termination is not satisfied. This points to a tension between validity (which requires that the ν threshold be large enough) and termination (which can be threatened when the ν threshold is high.)

Related work.

Blockchains can be roughly divided in consensus-less [START_REF] Nakamoto | Bitcoin: A Peer-to-Peer Electronic Cash System[END_REF] and Byzantine consensus-based blockchains [START_REF] Kokoris-Kogias | Enhancing Bitcoin Security and Performance with Strong Consistency via Collective Signing[END_REF][START_REF] Decker | Bitcoin Meets Strong Consistency[END_REF][START_REF] Abraham | Solidus: An incentive-compatible cryptocurrency based on permissionless byzantine consensus[END_REF][START_REF] Eyal | Bitcoin-NG: A Scalable Blockchain Protocol[END_REF][START_REF] Amoussou-Guenou | Correctness of tendermint-core blockchains[END_REF]. Byzantine Consensus-based blockchains have the advantage to guarantee strong consistency by running a Byzantine Fault Tolerant protocol [START_REF] Castro | Practical byzantine fault tolerance[END_REF]. In order to use a BFT protocol in an open setting, recent research has been devoted to either find secure mechanisms to select committees of fixed size over time (e.g. [START_REF] Gilad | Algorand: Scaling byzantine agreements for cryptocurrencies[END_REF], [START_REF] David | Ouroboros praos: An adaptively-secure, semi-synchronous proof-of-stake blockchain[END_REF]) and/or to propose incentives to promote participation [START_REF] Abraham | Solidus: An incentive-compatible cryptocurrency based on permissionless byzantine consensus[END_REF]. Most of the proposals, however, assume participants as either honest or Byzantine, lacking to thoroughly explore the effect of rational participants. In this line of work, Solidus [START_REF] Abraham | Solidus: An incentive-compatible cryptocurrency based on permissionless byzantine consensus[END_REF] is the first to consider rational processes by proposing an incentive-compatible BFT protocol for blockchains. Solidus introduces interesting incentive mechanisms, however, the paper lacks a game theoretic analysis of them.

While addressing a slightly different protocol, [START_REF] Mohammad Hossein Manshaei | A game-theoretic analysis of shard-based permissionless blockchains[END_REF] is the closest work to ours. In this protocol multiple committees run in parallel to validate a non-intersecting set of transactions (a shard). A non-cooperative static game approach for the intra-committee protocol is taken leading to the result that rational agents can free-ride when rewards are equally shared. The main aspect of our analysis that is new and different from [START_REF] Mohammad Hossein Manshaei | A game-theoretic analysis of shard-based permissionless blockchains[END_REF] is the following: we have a dynamic (not static) multi-round analysis, of a problem in which some participants are Byzantine and some blocks can be invalid (and costly for rational if accepted). In that context, there is a situation in which in equilibrium rational agents are pivotal, because if they do not check the block validity this will create the risk of having an invalid block accepted. It is because they are pivotal that they do not free ride. Moreover, we discuss equilibria in relation to formal consensus properties -Termination vs Validity -, which represents a novelty.

In the realm of consensus-less blockchains, as Bitcoin, many works used rational arguments to prove thresholds on the fraction of honest nodes needed to guarantee security properties [START_REF] Eyal | Majority is not enough: bitcoin mining is vulnerable[END_REF][START_REF] Sapirshtein | Optimal selfish mining strategies in bitcoin[END_REF]. These works establish very pessimistic thresholds while in practice Bitcoin works even if the honest majority assumption does not hold [START_REF] Badertscher | But why does it work? A rational protocol design treatment of bitcoin[END_REF]. Following this observation, [START_REF] Badertscher | But why does it work? A rational protocol design treatment of bitcoin[END_REF] proposes a rational analysis of Bitcoin based on the rational design protocol framework [START_REF] Garay | protocol design: Cryptography against incentive-driven adversaries[END_REF]. The proposed game, with respect to ours, is at an upper level of abstraction, proposing a two-player zero-sum game between the protocol designer and the adversary. Our game models instead the behavior of protocol participants, that can be rational, evolving in an environment with Byzantine processes. Moreover, our work targets consensus-based blockchain unlike [START_REF] Badertscher | But why does it work? A rational protocol design treatment of bitcoin[END_REF].

With only rational players, [START_REF] Biais | The blockchain folk theorem[END_REF] models Bitcoin as a coordination game. Similar to the work in [START_REF] Biais | The blockchain folk theorem[END_REF], our analysis shows that the protocol in consensus-based blockchains is a coordination game. Additionally, we consider Byzantine players, and show that Termination can be violated when coordination failures occur. [START_REF] Saleh | Blockchain Without Waste: Proof-of-Stake[END_REF] uses a game theoretic approach to study consensus-less Proof-of-Stake Blockchains, and shows that the Nothing at Stake problem is mitigated because players with large stakes on the main chain prefer not to add blocks on forking branches, lest it should reduce the strength of the main chain, and thus the value of their stakes. The environment considered in [START_REF] Saleh | Blockchain Without Waste: Proof-of-Stake[END_REF] differs from ours, since the study in [START_REF] Saleh | Blockchain Without Waste: Proof-of-Stake[END_REF] does not consider consensus-based blockchains, nor Byzantine players.

Blockchain Consensus with Rational Players

System Model

We consider a system composed of a finite and ordered set Π, called committee, of synchronous sequential processes or players, namely Π = {p 1 , . . . , p n } where process p i is said to have index i.

In the following, we refer to process p i by it index, say process i. Hereafter, the words "player" and "process" are taken to have the same meaning.

Communication. We assume that each process evolves in rounds. A round consists of one or more phases, and each phase is divided into three sequential steps, in order: the send, the delivery and the compute step. We assume that the send step is atomically executed at the beginning of the phase and the compute step is atomically executed at the end of the phase. The phase has a fixed duration that allows collecting all the messages sent by the processes at the beginning of the phase during the delivery step. At the end of a phase a process exit from the current phase and starts the next one. The processes communicate by sending and receiving messages through a broadcast primitive. Messages are created with a digital signature, and we assume that digital signatures cannot be forged. When a process i delivers a message, it knows the process j that created the message. We assume that messages cannot be lost.

Processes Behavior. In this paper we consider a variant of the BAR model [START_REF] Amitanand | BAR fault tolerance for cooperative services[END_REF] where processes are either rational or Byzantine. Rational processes are self-interested and seek to maximize their expected utility. They will deviate from a prescribed (suggested) protocol if and only if doing so increases their expected utility. Their objective function must account for their costs (e.g., sending messages) and benefits (e.g., reward of a block) for participating in a system. In line with [START_REF] Amitanand | BAR fault tolerance for cooperative services[END_REF], the objective of Byzantine processes is prevent the protocol from achieving its goal, and to reduce the rational processes utility, no matter the cost. We denote by f the number of Byzantine processes in the network. We assume symmetric Byzantines, their behaviour is perceived identically by all non Byzantine processes. That is, a message sent by a Byzantine process and received by a non-Byzantine process in a given phase is received by all non-Byzantine processes in the same phase.

Byzantine Consensus based Blockchain

Consensus-based blockchains should satisfy the following consensus properties:

• Termination: every non-Byzantine process decides on a value (a block);

• Agreement: if there is a non-Byzantine process that decides a value B, then all the nonbyzantine processes decide B;

• Validity [START_REF] Crain | Leader/Randomization/Signature)-free Byzantine Consensus for Consortium Blockchains[END_REF]: a decided value by any non-Byzantine process is valid, it satisfies the predefined predicate.

Let us note that the above properties must hold also for systems prone to rational behavior. To implement the above specification in Consensus-based blockchains, for each height h > 0 of the blockchain, a Consensus instance is run inside a committee selected for the given height. In this paper we analyze a very general protocol, inspired by [START_REF] Abraham | Solidus: An incentive-compatible cryptocurrency based on permissionless byzantine consensus[END_REF][START_REF] Amoussou-Guenou | Correctness of tendermint-core blockchains[END_REF][START_REF] Decker | Bitcoin Meets Strong Consistency[END_REF][START_REF] Eyal | Bitcoin-NG: A Scalable Blockchain Protocol[END_REF][START_REF] Kokoris-Kogias | Enhancing Bitcoin Security and Performance with Strong Consistency via Collective Signing[END_REF][START_REF] Miller | The honey badger of bft protocols[END_REF][START_REF] Yin | HotStuff: BFT Consensus in the Lens of Blockchain[END_REF], a variant of PBFT. In this protocol, a proposer proposes a value, i.e. a block, and the other members of the committee will check the validity of the value. If the value is valid, then they will vote for it and will announce their vote through a message to the other members. Votes are collected and if a given threshold is reached, then the value is decided, otherwise a new proposer will propose another block and the procedure restarts.

In this work, we study a protocol (for rational players) which in some equilibria implements the consensus. For the sake of clarity, we first present a prescribed protocol, and then the actions of the rational processes. If a rational player does not deviate from a given prescribed protocol, we can consider it as a correct process.

The prescribed protocol. The protocol proceeds in rounds. For sake of simplicity we consider the height k of the blockchain passed as parameter to the protocol. Algorithm 1 presents the pseudo-code of the protocol.

For each round t a committee member is designated as the proposer for the round in a round robin fashion. The isProposer(t, k) function returns true only if the process is the proposer for the current round (line 7). The function, by taking as parameter the current height, only returns true if the proposer is part of the current committee, deterministically selected on the basis on the information contained in the blockchain up to k (the actual selection mechanism is out of the scope of the paper). Each round is further divided in two phases: the PROPOSE and the VOTE phase.

During the PROPOSE phase, the proposer of the round uses the function createValidValue(k) to generate a block. Because a valid block must include the identifier of the k th block in the blockchain, the height k is passed as parameter (line 8). Once the block is created, a message broadcasting the proposal is sent (line 9). At line 10 the proposal is received through a delivery function. Each process checks if the proposal is a valid value (line 13). If so, the process sets its vote to the value (line 14).

During the VOTE phase, any process that set its vote to the current valid proposal sends a message (of type vote) to the other members of the committee (line 18). During the delivery step, sent messages are collected by any process. During the compute step each process verifies if a quorum of ν votes for the current proposal has been reached. Let us note that ν, the majority threshold is a parameter here, because it is the object of our study to establish the quorum ν in presence of rational and Byzantine processes. If the quorum is reached, if the process voted for the value and did not already decided for the current height, then it decides for the current proposal (line 23) and the protocol ends. If the quorum is not reached, then a new round starts (line 26).

Algorithm 1 Prescribed Protocol for a given height k at any process i

: if | VOTE, k, t, v | ≥ ν ∧ decidedV alue = nil ∧ vote = nil ∧ vote = v then 23:
decidedV alue ← v; exit /* The valid value is decided if the threshold is reached */ 24: else 25:

vote ← nil 26:

t ← t + 1
Let us note that the protocol in an environment assuming only correct (altruistic) and symmetric Byzantine processes trivially implements consensus if f , the number of Byzantine processes, is such that f < ν. If f ≥ ν, on the other hand, the Termination property is not guaranteed. The scenario for that is that Byzantine validators might vote for a different value with respect to the one voted by correct processes or a nil value. In that case the correct process will not decide (line 22) and will move in the next round. The scenario can repeat forever.

In the following we detail the pseudo-code for a rational processes shown in Algorithm 2. The rational process will try to maximize its payoff by choosing to undertake or not the actions defined in its action space. We consider the choice of : (i) proposing or not a valid block, (ii) checking or not the validity of a block and (iii) sending or not the vote for a proposed block. The decision tree for the process i is shown in Figure 1.

Let us consider now rational processes. The rational process will try to maximize its payoff by choosing to undertake or not some actions, defined in Section 2.3. Intuitively, we consider the choice of : (i) proposing or not a valid block, (ii) checking or not the validity of a block and (iii) sending or not the vote for a proposed block. We consider that the actions of checking the validity of the block and the action of sending the message (of type vote) have a cost.

Protocol of the rational processes. Rational processes choices are explicitly represented in the pseudo-code (Algorithm 2) by dedicated variables, namely, action propose , action check , and action send , defined at lines 5 -7. Each action, initialized to nil, can take values from the set {0, 1}. depends on the knowledge the process has about the validity of the proposal. The strategy determines if the process chooses to send its vote for the proposal or not (line 24-30). If the processes chooses to send a message for the proposal it will pay a cost c send .

Let us note that the rational player that did not check the validity of the block could decide an invalid value if more than ν other processes have done the same and the proposed block is invalid.

We now define the game that represent the protocol.

Byzantine-Rational Game

Recall that out of the n players, f ≥ 1 are Byzantine, while nf are rational. Each player i privately observes its own type, θ i , which can be Byzantine (θ i = θ b ) or rational (θ i = θ r ). 1Action space. As proposer, the player decides whether to propose a valid block or to propose an invalid block. Then, at each round t, each player first decides whether to check the block's validity or not (at cost c check ), and second decides whether to send a message (at cost c send ) or not.

Information sets. At the beginning of each round t > 1, the information set of the player, h t i , includes the observation of the round number t, the player's own type θ i , as well as the observation of what happened in previous rounds, namely (i) when the player decided to check validity, the knowledge of whether the block was valid or not, (ii) how many messages were sent, and (iii) whether a block was accepted or not. At round 1, h 1 i only includes the player's private information about its own type, θ i .

Algorithm 2 Pseudo-code for a given height k modelling the rational process i's behavior Then, in each round t > 1, the player decides whether to check the validity of the current block. At this point, denoting by b t the block proposed at round t, when the player does not decide to check validity isValid(b t ) is the null information set, while if the player decides to check, isValid(b t ) is equal to 1 if the block is valid and 0 otherwise. So, at this stage the player's information set becomes

H t i = h t i ∪ isValid(b t ), which is h t
i augmented with the validity information player i has about b t , the proposed block.

Strategies. At each round t ≥ 1, the strategy of player i is a mapping from its information set into its actions. If the agent is selected to propose the block, its choice is given by σ propose i (h t i ). Then, at the point at which the agent can decide to check block's validity, its strategy is given by σ check i (h t i ). Finally, after making that decision, the player must decide whether to send a message or not, and that decision is given by σ send i (H t i ).

Reward and cost from adding blocks. In this paper we study the case in which, when a block is accepted, only the processes which sent a message are rewarded (and receive R). In addition, we assume that when an invalid block is accepted, all rational players incur cost κ.

In this work we make the following assumption. The reward, R, to the players when a block is accepted is larger than the cost of checking validity, c check , which in turn is larger than cost of sending, c send , a message. But the reward obtained when a block is accepted is smaller than the cost of accepting an invalid block, κ. That is, κ > R > c check > c send .

Objective of rational players. Let T be the endogenous round at which the game stops. If a block is accepted at round t ≤ n, then T = t. Otherwise, if no block is accepted, T = n. In the latter case, the termination property is not satisfied.

At the beginning of the first round, the expected gain of rational player i is:

U i = E (R * 1 (σ send i (H T i )=1) * 1 (block accepted at T ) -κ1 (invalid block accepted) ) -T t=1 c check 1 σ check i (h t i )=1) + c send 1 (σ send i (H t i )=1) |h 1 i ,
where 1 (.) denotes the indicator function, taking the value 1 if its argument is true, and 0 if it is false.

Then, at the beginning of round t > 1, if T ≥ t, the continuation payoff of the rational player with information set h t i is

W i,t (h t i ) = E (R * 1 (σ send i (H T i )=1) * 1 (block accepted at T ) -κ1 (invalid block accepted) ) -T s=t c check 1 (σ check i (h s i )=1) + c send 1 (σ send i (H s i )=1) |h t i ,
Objective of Byzantine players. In the current paper we assume the following: Byzantine processes 1) as proposers, propose invalid blocks, and 2) when receiving a proposed block, check the blocks' validity and send a message if and only if the block is invalid.

We conjecture, the above strategies will turn out to be the optimal strategies of the Byzantine players, minimizing W i,t in equilibrium.

Equilibrium concept. Since we consider a dynamic game, with asymmetric information, the relevant equilibrium concept is Perfect Bayesian Equilibrium [START_REF] Fudenberg | Perfect bayesian equilibrium and sequential equilibrium[END_REF], intuitively defined as follows:

A Perfect Bayesian equilibrium is such that all players 1) choose actions maximizing their objective function, 2) rationally anticipate the strategies of the others, and 3) draw rational inferences from what they observe, using their expectations about the strategies of the others and Bayes law, whenever it applies.

A Perfect Bayesian Equilibrium (PBE) is a Nash equilibrium [START_REF] Nash | Non-cooperative games[END_REF], so players best-respond to one another. It imposes additional restrictions, to take into account the fact that the game is dynamic and that players can have private information, and therefore must draw rational inferences, from their observation of actions and outcomes. Rationality of inferences in PBE implies that (i) each player has rational expectations about the strategies of the others, and (ii) each player's beliefs are consistent with Bayes law, when computing probabilities conditional on events that have strictly positive probability on the equilibrium path. Perfection in PBE implies that, at each node starting a subgame the players' strategies form a Nash equilibrium of that subgame. In this context, to show that a strategy is optimal it is sufficient to show that it dominates any one-shot deviation [START_REF] Blackwell | Discounted dynamic programming[END_REF].

Problem Definition In this work, we explore the behavior of rational players that could not validate the block -because checking validity has a cost -and conditions (the majority threshold ν and proportion of Byzantine processes) under which rational players reach an equilibrium where consensus properties (defined in Section 2.2) are guaranteed. To do so, in Section 3, we study the equilibria that arise under different conditions.

3 Equilibria for Rational Players

Equilibrium when f ≥ ν

When the number of Byzantine players is larger than the majority rule, i.e., f ≥ ν, the validity property is not satisfied, since, when the first proposer is Byzantine, it proposes an invalid block, and that block is accepted, as all Byzantine players send messages in its favor. Against that backdrop, we characterize the strategies of the rational players and state the equilibrium outcome when f ≥ ν.

Proposition 1. If nf ≥ ν + 1 and f ≥ ν, there exists a Perfect Bayesian equilibrium in which the strategy of a rational player at any round is the following:

• As proposer, a rational player proposes a valid block.

• When receiving a proposed block, the rational players do not check the block validity but send a message.

The first condition (n-f ≥ ν +1) implies that, when all rational players but one send a message, they meet the majority threshold ν, so the block is accepted. The second condition (f ≥ ν) implies that, when all Byzantine processes send a message, the block is accepted. Under these conditions, each rational player understands it is not pivotal: If the block is invalid, Byzantine players will send messages, so that the block will be accepted irrespective of the rational player's own action. Moreover, if the block is valid, Byzantine players will not send messages, but all the other rational players will, so that the block will be accepted irrespective of the rational player's action.

Thus rational players understand that they are not pivotal, and that whatever they do, given the equilibrium behavior of the other rational agents and of the Byzantine processes; all blocks will be accepted. Consequently, they have no interest in checking the validity of the block. The only relevant comparison for them is between their expected gain when they send a message

R -c send - f n κ
and their expected gain when they do not send a message -f n κ. Since, by assumption, R > c send , rational players find it optimal to send a message. Finally note that, in the equilibrium of Proposition 1, a block is decided at round 1, so the termination property is satisfied, but, when the proposer is Byzantine, an invalid block is accepted, so the validity property is not satisfied. Proof If a rational player is selected to be the proposer, he prefers to propose a valid block than to propose an invalid block. Indeed, if he proposes an invalid block, that block will be accepted (since the f ≥ ν Byzantine players, on checking it and discovering it is invalid, will send a message). In that case the gain of the proposer is Rc checkc sendκ. If instead the rational player proposes a valid block, this block will be accepted and his gain will be Rc checkc send . Now, turn to the actions of rational players who are not proposers. The equilibrium gain of these players is

-c send + R - f n κ.
If instead of playing the equilibrium strategy, a rational player does not send a message, its expected gain is -f n κ, which by assumption (R > c send ) is lower than the equilibrium expected gain.

Another deviation is to check the block's validity and send a message only if the block is valid, which brings expected gain equal to

-c check + (1 - f n )(R -c send ) - f n κ.
This is lower than the equilibrium expected gain if

-c send + R - f n κ > -c check + (1 - f n )(R -c send ) - f n κ,
which holds since it is equivalent to

0 > -c check - f n (R -c send ).
The other possible deviations are trivially dominated: Checking the block's validity and sending a message only when the block is invalid, yields expected gain

-c check + f n (R -c send -κ),
which is lower than the equilibrium expected gain. Checking the block's validity and sending a message only when the block is valid yields expected gain

-c check + 1 - f n (R -c send ) - f n κ,
again lower than the equilibrium expected gain. Checks the validity of the block and always sending a message yields

R -c send - f n κ -c check ,
which is again dominated, as is also checking and not sending, which yields -c check -f n κ.

P roposition 1

Equilibria when f < ν

Proposition 2. When f < ν and nf ≥ ν, there exists a Nash equilibrium in which rational players never check blocks' validity nor send messages, so that no block is ever accepted.

Condition f < ν, in Proposition 2 implies that Byzantine players cannot reach the majority threshold on their own. This precludes accepting invalid blocks. So the validity property is satisfied. Unfortunately, the condition also implies there exists an equilibrium in which the termination property also fails to hold. The intuition is the following:

In Proposition 2, each rational player anticipates that no other player will send a message when the block is valid. 2 In this context, each rational player knows that, if it were to send a message in favor of a valid block, it would be the only one to do so. Because the majority threshold ν is strictly larger than 1, the block would not be accepted. Therefore sending a message is a dominated action for the rational player. Thus, the equilibrium in Proposition 2 reflects that rational players' actions are strategic complements and they must coordinate on sending messages in order to have valid blocks accepted. Proposition 2 shows that, in equilibrium, there can be a coordination failure, such that no block is ever accepted. 3Proof Consider a rational player who anticipates that other rational players will not send any message at any round. If it follow the equilibrium strategy and does not send an message, its gain is 0. This must be compared to the gain of the player if he deviates:

• If it sends a message without checking its expected gain is

-c send + Pr(invalid)1 (f =ν-1) (R -κ).
• If it checks the block's validity and sends a message only when the block is valid, its expected gain is -c check -Pr(valid)c send .

• If it checks the block's validity and sends a message only when the block is invalid, its expected gain is

-c check + Pr(invalid)(1 (f =ν-1) (R -κ) -c send ).
• If it checks the validity of the block and always sends a message, its expected gain is

-c send -c check + Pr(invalid)1 (f =ν-1) (R -κ).
• If it checks and does not send a message, its gain is -c check .

Clearly, the player is better off following the equilibrium strategy.

P roposition 2

Note that the conditions of Proposition 2 imply that f < n 2 , i.e, there is a strict majority of rational players. Yet, the proposition shows that such majority is not enough to ensure both termination and validity.

While there exists an equilibrium in which termination does not obtain, this does not necessarily imply there is no equilibrium with termination and validity. To have termination and validity, it must be that, in equilibrium, sufficiently many rational players find it in their own interest to check the validity of the block and to send messages in support of valid blocks. The problem is that some players might be tempted to free-ride, and let the others bear the cost of checking. To avoid this situation, it must be that (at least some) rational players anticipate they are pivotal, i.e., if they fail to check block validity and send messages in support of valid blocks, this may derail the process at their own expense.

To make this point, we look for an equilibrium in which some rational players check the validity of the block and send a message if and only the block is valid, and this results in valid blocks being immediately accepted and invalid blocks being rejected. Before proving that such an equilibrium exists, we characterise the expected continuation payoff to which it would give rise. Lemma 1. Consider a candidate equilibrium in which some rational players check the validity of the block and send a message if and only the block is valid, while the other rational players send messages without checking validity, and this results in valid blocks being immediately accepted and invalid blocks being rejected. In such an equilibrium, if it exists, the expected continuation payoff, at round t, of the rational players who are to check block validity is

π check (t) = R -c send -φ(t)c check ,
while the expected continuation payoff, at round t, of the rational players who are not to check block validity is

π send (t) = R -ψ(t)c send ,
where φ(f ) = 1, ψ(f + 1) = 1 and both φ and ψ satisfy property P defined below.

Definition 1. A function g satisfies property P , if g(t) = 1 + f -t+1 n-t+1 g(t + 1), ∀t < f . In the candidate equilibrium, participants will reach a point at which the block is valid and all rational players send a message so that the block accepted. This gives rise to a payoff Rc send , the first part of π check (t). The second part of π check (t), φ(t)c check , is the expected cost of checking block validity, where φ(t) is the expected number of times the player expects to check validity before a block is accepted. Similarly, in π send (t), ψ(t)c check , is the expected cost of sending messages, where ψ(t) is the expected number of times the player expects to send messages before a block is accepted. Proof We prove this Lemma in 2 parts:

1. Proof of the first part of the proposition, concerning the rational players who are expected to check validity:

At round t = f , players know that all f -1 previous proposers were Byzantine and that there are now nf + 1 potential proposers, out of which only one is Byzantine and nf > ν are rational. The expected gains of the rational players who are supposed to check are

-c check + n -f n -f + 1 (R -c send ) + 1 n -f + 1 (R -c send ),
where the first term is the cost of checking validity, the second term corresponds to the case in which the current proposer is rational and proposes a valid block that is immediately accepted, and the third term corresponds to the case in which the proposer is Byzantine, the block is rejected, and we move to the next round, at which a valid block is finally accepted (without needing any further validity check). This equilibrium payoff simplifies to

R -c send -c check ,
reflecting that eventually a valid block will be accepted, and that from round f on the player will need to check validity only once. This equilibrium payoff implies that

φ(f ) = 1.
Now turn to round t < f . If round t ≤ f is reached, the previous t -1 proposers were Byzantine. There remains n -(t -1) potential proposers. Out of them a fraction

f -(t -1) n -t + 1
is Byzantine, while the complementary fraction nf nt + 1 is rational. This fraction being the probability that the next proposer is rational.

To prove the property stated in the Proposition by backward induction, we now prove that if this property is satisfied at round t + 1, that is if

π check (t + 1) = R -c send -φ(t + 1)c check ,
then it is satisfied at round t.

Suppose the rational player follows the equilibrium strategy of checking and sending iff the block is valid. Its expected gain from round t on is

-c check + n -f n -t + 1 (R -c send ) + f -(t -1) n -t + 1 π(t + 1),
where the first term is the cost of checking the block at round t, the second term is the probability that the block is valid and accepted multiplied by the payoff in that case, and the third term is the probability that the block is invalid and rejected multiplied by the payoff in that case. Substituting the value of π check (t + 1), using that the property is verified at round t + 1, the expected gain writes as

-c check + n -f n -t + 1 (R -c send ) + f -(t -1) n -t + 1 (R -c send -φ(t + 1)c check ).
That is

R -c send -1 + f -(t -1) n -t + 1 φ(t + 1) c check ,
which, using the definition of φ(t), is Rc sendφ(t)c check .

2. Proof of the second part of the proposition, concerning the rational players who are just expected to send messages:

Again, we prove that if the property is satisfied at round t + 1, i.e., π send (t + 1) = Rψ(t + 1)c send , then it is satisfied at round t. Suppose the rational player follows the equilibrium strategy of not checking blocks' validity and always sending a message. Its expected gain from round t on is

c send + n -f n -t + 1 R + f -t + 1 n -t + 1 π send (t + 1),
where the first term is the cost of sending a message at round t, the second term is the probability that the block is valid and accepted multiplied by the payoff in that case, and the third term is the probability that the block is invalid and rejected multiplied by the payoff in that case. Substituting the value of π send (t + 1), the expected gain writes as

-c send + n -f n -t + 1 R + f -t + 1 n -t + 1 (R -ψ(t + 1)c send ).
That is

R -1 + f -t + 1 n -t + 1 ψ(t + 1) c send ,
which, using the definition of ψ(t), is Rψ(t)c send .

Lemma 1

Relying on Lemma 1, we now establish that our candidate equilibrium is indeed an equilibrium. To do so denote the highest index of all Byzantine players by i B . Proposition 3. When f < ν and nf > ν, if the cost κ of accepting an invalid block is large enough, in the sense that κ > α(t)c checkβ(t)c send , ∀t < f, where

α(t) = (n -t + 1)φ(t) -(f -t + 1) Pr(i B ≥ n -ν + f + 2|T ≥ t)φ(t + 1) (f -t + 1) Pr(i B < n -ν + f + 2|T ≥ t)
and

β(t) = Pr(i B ≥ n -ν + f + 2|T ≥ t) Pr(i B < n -ν + f + 2|T ≥ t) ,
and if the reward is large enough relative to the costs in the sense that

R ≥ max n n -f c send , c send + n n -f c check ,
there exists a Perfect Bayesian Nash equilibrium in which the strategy of rational players is the following:

• As proposer, a rational player proposes a valid block.

• At any round t ≤ f , when receiving a proposed block, (i) the rational players with index i ∈ {t, . . . , nν + f + 1} check the block validity and send a message only if the block is valid, while (ii) the rational players with index i ∈ {nν + f + 2, . . . , n} do not check the validity of the block but send a message.

• If round t = f + 1 is reached, rational players send a message without checking if the block is valid. At this point the block is valid and accepted.

Hence, in equilibrium, termination occurs no later than at round f + 1.

On the equilibrium path, invalid blocks (proposed by Byzantine players) are rejected, while valid blocks (proposed by rational players) are accepted. This implies that, if round t = f + 1 is reached, the players know that during all the previous (f ) rounds the proposers were Byzantine (to draw this inference, the rational players use their anticipation that all participants play equilibrium strategies; hence the Perfect Bayesian nature of the equilibrium). Consequently, at round f + 1, the proposer must be rational, and all players anticipate the proposed block is valid. So, no rational player needs to check the validity of the block but all send a message, which brings them expected gain equal to R-c send . This is larger than their gain from deviating (e.g., by not sending a message or by checking the block.)

At previous rounds t ≤ f , players know that all t -1 previous proposers were Byzantine and that there remains ft + 1 Byzantine players with index strictly larger than t -1 (as above, this rational inference is a feature of the Perfect Bayesian equilibrium we characterize). Do the equilibrium strategies of the rational players preclude acceptance of an invalid block by Byzantine processes? To examine this point, consider the maximum possible number of messages that can be sent if the proposer is Byzantine. In equilibrium the νf -1 players with indexes strictly larger than nν + f + 1 are to send a message without checking it. The worse case scenario (maximizing the number of messages sent when the block is invalid) is that none of these players are Byzantine. In that case, in equilibrium, the number of messages sent when the block is invalid is f + (νf -1) = ν -1, so that we narrowly escape validation of the invalid block. In contrast, if one of the rational players deviated from equilibrium and sent a message without checking the block, in the worse case scenario, this would lead to accepting an invalid block. Thus, in that sense, the rational players with index strictly lower than nν + f + 1 are pivotal. Hence they check block validity, because, under the condition stated in the proposition, the cost of accepting an invalid block is so large that rational players do not want to run that risk. Proof For clarity, we decompose the proof in 5 steps.

1. The first step is to note that rational proposers strictly prefer to propose a valid block than an invalid one. This is because, when they follow their equilibrium strategy of proposing a valid block, it is accepted and the proposer gets Rc checkc send , while if they propose an invalid block, it is rejected, and we move to the next round, a which, in equilibrium, the player gets at most Rc checkc send (and possibly less). Indeed, this player incurs the cost of checking validity at the next round, because the rational players who are not expected to check validity have indexes above nν + f + 1, which are above f + 1, so that they do not get to propose blocks.

2. The next step concerns the actions of the rational players when round t = f + 1 is reached. At that round, all players know the proposer must be rational and the proposed block valid.

In equilibrium no rational checks validity but all send a message. Any other action would be dominated.

3. The third step concerns the most relevant deviation, in which a rational player expected to check block validity fails to do so. If at round t a rational player supposed to check, deviates and sends a message without checking block validity, its expected continuation payoff is

1 - f -(t -1) n -t + 1 (R -c send ) + f -(t -1) n -t + 1 Pr(i B < n -ν + f + 1) (R -c send -κ) + f -(t -1) n -t + 1 Pr(i B ≥ n -ν + f + 1) (π(t + 1) -c send ) .
The first term is the payoff obtained by the deviating rational player if the current block is valid, and therefore immediately accepted. The second term is the payoff obtained by the deviating player when he was pivotal and triggered acceptance of an invalid block. To see this, consider the number of messages when the block is invalid, the rational player is deviating and the indexes of all the Byzantine players are strictly lower than nν + f + 2: f messages are sent by the Byzantine processes, 1 message is sent by the deviating rational agent, νf -1 messages are sent by the rational players with index above than or equal to nν + f + 2. The resulting total number of messages is ν and the block is accepted. The last term corresponds to the case in which the deviating rational player is not pivotal, and the invalid block is not accepted, so that we move to the next round.

Substituting the value of π check (t + 1) = Rc sendφ(t + 1)c check from Lemma 1, the expected continuation value of the deviating player is First, the player could do nothing (neither check nor send). Relative to the equilibrium payoff, this deviation economises the cost of checking (c check ). If the current proposer is Byzantine, the player then obtains the same payoff after a one shot deviation as on the equilibrium path (π check (t + 1)). If the current proposer is rational, the block gets accepted, but the player does not earn any reward. So the deviation is dominated if

n -f n -t + 1 (R -c send ) ≥ c check ,
which holds under the condition, stated in the proposition, that R ≥ max n n-f c send , c send + n n-f c check . Second, the player could check the block validity, and then send a message irrespective of whether the block is valid or not. This would generate a lower payoff than the main deviation, shown above (in 3.) to be dominated.

Third, the player could check validity but then send no message. When the current proposer is Byzantine, this one-shot deviation yields the same payoff as the equilibrium strategy. When the current proposer is rational, this deviation yields a payoff of -c check , which is lower than the equilibrium payoff Rc sendc check .

Fourth, the player could check the block's validity and send a message only if the block is invalid, which is trivially dominated. 5. Finally turn to deviations of rational players supposed to send messages without checking blocks' validity.

First, consider the possibility to abstain from sending a message. This economises the costs c send , but, in case the block is valid and accepted, this implies the agent loses the reward R. So, the deviation is dominated if

n -f n -t + 1 R ≥ c send ,
which holds under the condition, stated in the proposition, that R ≥ max n n-f c send , c send + n n-f c check . Second, consider the possibility of checking validity and sending a message only for valid blocks. This deviation would imply the agent would have to incur the cost of checking (c check ), but it would economise the cost of sending a message when the block is invalid. So the deviation is dominated if

c check ≥ f -t + 1 n -t + 1 c send ,
which holds because of our assumption that c check ≥ c send .

Other deviations, such as checking validity but never sending messages, or checking validity and always sending messages, or checking validity and sending only if the block is invalid, are trivially dominated.

P roposition 3

Conclusion and Future Work

In this paper we model PBFT-consensus based blockchains as a coordination game between rational and Byzantine processes. We derive the conditions (on the majority threshold and the proportion of Byzantine processes) under which consensus properties are guaranteed in equilibrium or not. In future work, we will extend the analysis to more general Byzantine strategies and rational agents preferences, costs and rewards.

  Those values are set by calling the functions σ propose

				Send (lines 24 -30)
		Valid
	Checks the			Not Send (line 24)
	validity
	(lines 21-23)			Send (lines 24 -30)
		Not Valid
				Not Send (line 24)
	Does not (line 21) validity check the	(line 6) Information No Validity	Not Send (line 24) Send (lines 24 -30)
	Figure 1: Decision tree of process i
	i	, σ check i	, and σ send i	, respectively, returning the
	strategy for the process i. Strategy σ propose

i determines if the proposer i chooses to produce a valid proposal or an invalid one (lines

[START_REF] Eyal | Bitcoin-NG: A Scalable Blockchain Protocol[END_REF][START_REF] Eyal | Majority is not enough: bitcoin mining is vulnerable[END_REF][START_REF] Fudenberg | Perfect bayesian equilibrium and sequential equilibrium[END_REF][START_REF] Garay | protocol design: Cryptography against incentive-driven adversaries[END_REF][START_REF] Gilad | Algorand: Scaling byzantine agreements for cryptocurrencies[END_REF]

. In both cases the proposal is sent in broadcast (line 17).

Strategy σ check i determines if the receiving process chooses to check the validity of the proposal or not, which is a costly action. If the process chooses to check the validity (line 22), it will also update the knowledge it has about the validity of the proposal and it will pay a cost c check . If otherwise, the process keeps not knowing if the proposal is valid or not (validV alue[t] remains set to ⊥). Note that this value remains set to ⊥ even if the process is the proposer. This is because we assumed, without loss of generality, that checking validity has a cost and that the only way of checking validity is by executing the isValid(v) function.

Note that, as defined in Section 2.3, strategy σ send i

  c send ) -f -(t -1) nt + 1 Pr(i B < nν + f + 2|T ≥ t)κ f -(t -1) nt + 1 Pr(i B ≥ nν + f + 2|T ≥ t) (φ(t + 1)c check + c send ) .The equilibrium condition is that this deviation payoff must be lower than the equilibrium continuation payoff of the playerRc sendφ(t)c check . B < nν + f + 2|T ≥ t)κ > φ(t)c check f -(t -1) nt + 1 Pr(i B ≥ nν + f + 2|T ≥ t) (φ(t + 1)c check + c send ) .

	Or
	(R That is
	f -(t -1) n -t + 1 Pr(i Note that φ(t) ≥ f -(t -1) n -t + 1	Pr(i

1 -f -(t -1) nt + 1 (Rc send ) + f -(t -1) nt + 1 Pr(i B < nν + f + 2|T ≥ t) (Rc sendκ) + f -(t -1) nt + 1 Pr(i B ≥ nν + f + 2|T ≥ t) (Rc sendφ(t + 1)c checkc send ) . B ≥ nν + f + 2|T ≥ t)φ(t + 1),

since by the definition of φ(t) this inequality is equivalent to

1 + f -(t -1) nt + 1 φ(t + 1) ≥ f -(t -1) nt + 1 Pr(i B ≥ nν + f + 2|T ≥ t)φ(t + 1),

which indeed holds. Thus we can write the equilibrium condition as

κ > α(t)c checkβ(t)c send , ∀t < f,

as stated in the proposition.

4. Other possible deviations for rational player supposed to check block's validity are easier to rule out:

If player's type was observable (i.e., if Byzantine processes were detectable in advance) there would be a trivial solution to preclude them from harming the system: forbidding their participation.

Byzantine players send messages but only when the block is invalid.

If f = 0, then, with ν = 1, there exists a unique equilibrium, in which all processes check validity and send a message iff the block is valid. In that equilibrium validity and termination are satisfied. But this obtains only if there are no Byzantine processes. As soon as f ≥ 1, if ν = 1, Proposition 1 applies and validity is not satisfied.