Mathieu Cunche

Mohamed Ali Kaafar

Roksana Boreli

Asynchronous Covert Communication Using BitTorrent Trackers

Keywords: Covert Channel, BitTorrent, Tracker Canaux de Communication Cachés Canaux Cachés, BitTorrent, Tracker

Covert channels enable communicating parties to exchange messages without being detected by an external observer. In this paper we propose a novel covert channel mechanism based on BitTorrent trackers. The proposed mechanism uses common HTTP commands, thus having the appearance of genuine web traffic and consists of communications that are both indirect and asynchronous: no messages are directly exchanged between the sender and the receiver (of covert communications) and there is a potentially considerable delay between the sender's message to the relaying party and the receiver collecting this message. We present details of the proposed scheme in which a centralized BitTorrent tracker is used for storing covert messages and evaluate its performance based on the implemented prototype. We analyze the detectability of covert communications by an adversary and show that, while the common nature of the BitTorrent traffic and the large number of clients make the detection unlikely, the low temporal correlation between the writer and the reader (the two communicating parties) further increases the detection difficulty. Finally we discuss a variant of our scheme that uses a decentralized tracker (based on distributed hash tables), increasing the scalability and enabling a larger number of parallel covert communication channels.

Introduction

While the purpose of encryption is to protect the content of any communication from being revealed to unauthorized parties, covert channels aim to hide the existence of the communication itself. Covert channels were first described in the context of Multi-Level Security (MLS) systems [3], as a way to communicate information from high security to low security processes. They have been subsequently extended to the case of network communications, with their application ranging from military and national security, where they are used to hide potential communications between parties, to botnets and use by cyber criminals, that look to control remote systems while circumventing traffic filtering.

The model of covert channels has been initially introduced by Simmons in [START_REF] Simmons | The prisoners' problem and the subliminal channel[END_REF] with the Prisoners' problem and the subliminal channel. Two prisoners, who communicate while being observed by a warden, exchange seemingly harmless messages, which however contain useful information enabling them to agree on an escape plan.

We define as indirect network covert channel (I-NCC) a covert channel in which the information is being sent to a host that is distinct from the participant end systems, while in a direct network covert channel (D-NCC) the information is stored in the data packets exchanged between the participants. A large number of dynamic D-NCCs have been proposed in the past (e.g. [START_REF] Wolf | Covert channels in lan protocols[END_REF][START_REF] Lucena | Covert channels in ipv6[END_REF]). In those systems, the transmitted information is embedded within various fields of network packet headers, or inside the data used for padding. On the other hand a fewer number of A-NCCs have been proposed. The utilized techniques include e.g. [START_REF] Luo | Crafting web counters into covert channels[END_REF] where the counters available on various websites are leveraged to store information.

The huge amount of data exchanged through Peer-to-Peer (P2P) networks and the globalscale of P2P infrastructure creates an environment where communication has a potential to be hidden among the mass of regular users and corresponding host message exchanges. We propose to use the BitTorrent tracking infrastructure, as the most widely used P2P file-sharing system with tens of millions of worldwide users, to build a novel asynchronous (network storage) covert channel.

The choice of the BitTorrent tracker system as a storage for our covert channel algorithm is motivated by the suitable properties of the tracker system. First, a tracker commonly hosts lists of peers for multiple content files, and many trackers allow users to not only add content to a swarm but also to retrieve the complete list of content "monitored" by a tracker. Second, trackers usually scale to millions of requests from hosts geographically distributed across many countries, which make them good candidates for universally accessible memory.

In this paper we present a novel asynchronous covert channel based on BitTorrent trackers. Our contributions are as follows.

We present a communication scheme that enables two parties to perform a hidden exchange of information through the centralized BitTorrent tracker. Two inherent properties of the scheme are beneficial to covert communications, as they assist with having a low detectability: the scheme is an indirect network covert channel and it is asynchronous, with the sending and retrieving nodes having the flexibility of not needing to access the intermediate node at the same time. The scheme includes error correction and encryption mechanisms, respectively, to mitigate data losses and to provide obfuscation of transmitted data. Our system exploits the basic primitives of the (centralized) BitTorrent tracker protocol, and therefore does not require the cooperation of the tracker.

We implement a prototype and evaluate the performance of the proposed covert channel scheme. The presented results show that our system can transmit data at an average rate of 1.89 bits/second, and that the data losses appearing on the tracker are compensated by the error correction scheme. In addition, once written on the tracker, the data remain available for dozens of minutes, providing a considerable time window in which the receiver may retrieve the data. Overall these results demonstrate that such a communication channel can reliably transmit information at a rate sufficient for the exchange of small pieces of data (such as text messages or botnet commands) without a fine-grained time synchronization between the sender and the receiver.

We analyze the detectability of our scheme, which includes a number of features well suited to covert communications. First, our system is solely based on one of the most commonly used operation on the Internet, i.e. the HTTP/GET request, resulting in communications having the appearance of genuine traffic. Second, it is asymmetric in the sense that read and write operations are not equivalent, resulting in a distinct cost and a detection difficulty for the sender and the receiver.

Finally, we propose an extension of our scheme to include a decentralized tracker, based on distributed hash tables (DHT), a mechanism adopted by multiple BitTorrent clients. We describe the adaptation of our covert communication scheme to the DHTs and discuss it's advantages of increased scalability and limitations of an increased potential for traffic detection, compared to the scheme where centralized trackers are used.

The paper is organized as follows. In Section 2 we briefly overview the BitTorrent system. Section 3 describes the design of our covert channel and Section 4 analyses the characteristics of the centralized tracker based system. In Section 6 we discuss the difficulty of detection. In Section 5 we present results on the system's performance. Modification that includes the use of distributed hash table is presented in Section 7 and Section 8 review the related work. We present conclusions in Section 9.

Centralized BitTorrent Trackers

BitTorrent is a Peer-to-Peer system in which peers share and download content by exchanging content chunks. To establish a connection with other peers, any peer needs to obtain the IP addresses and ports of the peers involved in the swarm (set of peers downloading and/or sharing a given content), which is performed by using a central server tracking the peers involved in a swarm. Each centralized tracker usually stores the list of peers for several contents. For instance, we found several millions of contents registered on the publicbt tracker.

The BitTorrent system uses a content identification system based on hash called infohash obtained by computing the SHA-1 digest of the content meta-information. Therefore an infohash is a 20 bytes long (160 bits) identifier. In order to obtain the list of peers connected to a swarm, a BitTorrent client contacts a centralized tracker using an Announce request. This request can be performed through either UDP or HTTP protocol. In both cases the requested URL contains several parameters, in particular the content's identifier : http://[tracker_url]/announce? info_hash=x.

Upon reception of an announce request, and if the content is already registered on the tracker, the tracker returns a set of peers and adds the requesting peer to the list. If the content is not registered on the tracker, there are two possible cases: either the tracker rejects the request by specifying a request for an unregistered content, or the tracker registers the content and adds the requesting peer to the corresponding peer list. In the later case the tracker is called open, in the sense that any peer can register a new content on the tracker by performing an announce request. Within the BitTorrent ecosystem, both open and non-publicly accessible centralized trackers co-exist.

Additionally, centralized BitTorrent trackers support other requests such as scrape requests, used to retrieve information on a given content such as the number of registered peers. A Inria generalisation of this request is the scrape-all request that provides the same information but for all the contents registered on the tracker. As a side effect, this request also provides the full list of the contents registered on the tracker. A scrape-all request is performed through an HTTP/GET query on the following url : http://[tracker_url]/scrape Since, the scrape-all request can be very costly for the tracker, it is not always supported. In order to remove this burden from the tracker itself, the corresponding information is sometime offered by a web server. For instance, the publicbt tracker provides a compressed scrape file refreshed every 10 minutes at the following address : http://publicbt.com/all.txt.bz2.

Centralized Tracker-Based Covert Channel Design

In this section, we outline the design of the proposed asynchronous cover channel.

Read and Write operations

We first describe how the centralized tracker can be used as a memory and how the read and write operations can be performed. In this memory the information is stored under the form of data block represented by info_hash identifier in the tracker's content table. Since the info_hash used as content identifier is 20 bytes long, the information can be stored on the tracker as chunk of 20 bytes (160 bits).

Fig. 1 depicts the communication between the writer and the tracker on one side, and between the reader and the tracker on the other side. To write on the tracker, we have to add an entry using an announce request. Let x be a 20 bytes length value, then sending the following request to the tracker will add an entry x to the content table: GET http://[tracker_url]/announce?info_hash=x.

It is possible that the entry x already exists in the content table, in which case, the entry will be updated by increasing the number of peers and adding the source IP address of the request to the list of connected peers.

To read a value from the tracker, we have to get the list of the content identifier stored on the tracker. This operations can be done by using the scrape all request on the tracker. As noted in Section 2, some tracker, such as publicbt.com, provide this information under the form of an aggregated file (we used the compressed text file provided by publicbt.com that can be retrieved at http://publicbt.com/all.txt.bz2 ). Some tracker provide this information under the form of an aggregated file. For instance publicbt.com provides a link to a compressed text file that can be retrieved at http://publicbt.com/all.txt.bz2.

Hash-based filtering for packet identifications

The previously described read operation retrieve all the info_hash stored in the content table. This content table contains both genuine entries, i.e. entries corresponding to existing torrent, and hidden entries, i.e. entries added to the tracker by our hidden communications. To distinguish hidden entries from genuine entries, we use a hash-based filtering mechanism. For each piece of information stored on the tracker, the last t bits are a hash value of the 160t first bits, using a hash function, h(.). For the read operation, after the scrape all operation has been performed, the retrieved info_hash are filtered. Specifically, for each info_hash

x, if h(x[0 . . . 160 -t -1]) = x[160 -t . . . 160 -1], then keep x otherwise discard x.
This hash-based filtering approach may however induce false positives, where info_hash may pass the filter while they are genuine and not hidden entries. We discuss this issue in Section 4.1.

Obfuscation through encryption

With the previous hash-based filtering mechanism, the hidden info_hash can be easily detected by someone knowing the algorithm. This issue can be avoided by encrypting the data before it is written on the tracker, for instance with a symetric block-cipher. Indeed, only a person knowing the secret key will be able to decrypt the retrieved info_hash and filter out those that are corresponding to hidden pieces of information. In addition, this encryption provide data confidentiality and in particular prevent an eavesdropper to recognize the hidden data in plain text.

Data indexing

The size of the info_hash limits the amount of data that can be transmitted in one entry of the content table. The quantity of information that can be encoded (written) is even more reduced with the adjunction of the hash of the useful data (as described in Section 3.2). In essence, a total of 160t bits of information can transmitted per entry. In the case where a larger amount of data has to be transmitted, the data can be split and carried by several content identifiers. In order to transmit a message split in several pieces, we need to add an indexing functionality. To this aim we reserve the first s bits of data for indexing. Those s bits simply contain a sequence identifier, and are concatenated to the data before the addition of the hash to allow the indexing of up to 2 s pieces of information.

Data loss and erasure coding

During our experiment, we have observed that the data written on the tracker can be subject to erasure 1 , i.e. loss of information. These data losses are caused by various errors and by the content expiry delay (which is studied in Section 4.2).

Erasure coding provides an elegant and efficient solution to the problem of data losses encountered in storage [START_REF] Plank | A tutorial on Reed-Solomon coding for fault-tolerance in RAID-like systems[END_REF] and computer communications applications [START_REF] Rizzo | Effective erasure codes for reliable computer communication protocols[END_REF]. By adding redundancy to the source data, erasure codes allow to tolerate the loss of data blocks. More formally the encoding process takes as input a set of k data units and produces n encoded data units, where n > k. Perfect codes, allow the source data to be rebuild from any m distinct data units, as long as m ≥ k. Reed-Solomon codes [START_REF] Reed | Polynomial codes over certain finite fields[END_REF] are an example of perfect codes that have been extensively used in the context of data erasure.

After splitting the message into k blocks of 160ts bits, the encoding process is applied and n blocks, also of 160ts bits, are generated as output of the encoder. Thanks to the optimal erasure correction capabilities of the Reed-Solomon codes, the reader can recover the source data as soon as k blocks have been collected. The amount of redundancy represented by 1 Data written on the tracker was not returned in the scrape-all results. Inria the code rate, R = n/k, can be adjusted to meet the channel requirements, i.e. as appropriate to the loss rate.

Summary of the covert channel mechanism

On the writer side, the message is first divided into k blocks of 160ts bits and encoded into n blocks. For each block, an index and a hash are then added and the obtained data is encrypted before being written (through a HTTP Get Request) on the tracker. Figure 3 describes the encoding of a single data block while Figure 2 presents the operations required to encode a message spanning over several data blocks.

To retrieve the message, the reader performs a scrape-all request, then decrypts all the content identifiers and uses the hash-based filter to select the hidden data blocks. If enough blocks have been collected, a decoding process is applied to decode the original message.

System analysis

In the following, we analyze the characteristics of our proposed asynchronous covert communication scheme. First, as previously mentioned, we examine the extent to which the hash-based filtering approach may induce false positives while retrieving the data from the centralized tracker.

Then we analyze the time data blocks remain on the tracker and finally we evaluate the fraction of data block that are lost during the transmission.

False-positive of the hash-based filter

As noted in Section 3.2, identification of the hidden content by a hash function-based filter may induce false positives, when genuine content identifiers successfully pass the hash-based filter. A false positive will result in either a block collision (if the block index already exists in the sequence) or an insertion (if the index does not exist in the sequence). In both cases the false positive will disrupt the communication by corrupting the data. Let (X | Y ) be the content identifier where X represents the 160-t first bits and Y represents the t last bits corresponding to the hash. A false positive is a genuine content identifier (X | Y ) such as h(X) = Y , ie a content identifier for which the last t bits match the hash of the 160t bits. A content identifier being 20 bytes long SHA-1 hash, and assuming that the output of SHA-1 is uniformly distributed, the false-positive probability is : P (h(X) = Y ) = 2 -t . For a table containing n genuine contents, the expected number of false positive is:

N F-P = n 2 -t
The expected number of false positives can therefore be adjusted through the hash size, t. The number of false positives should be kept as small as possible. However, increasing the size of the hash reduces the number of useful bits in the data block. Let's exemplify this by considering the publicbt tracker which is tracking around 3.10 6 content identifiers. With this tracker, a 2-bytes long hash (t = 16) yields to 43.7 false positives, while a 4-bytes long hash (t = 32) yields to 6.67 10 -5 false positives on the average. We then consider the latter as a good compromise between communication overhead induced by the hash size and the expected number of transmission failure caused by false positives.

Entry's lifetime

Entries are not stored indefinitely on the centralized tracker and if an entry is not requested for a given amount of time, it is removed from the tracker. We have measured this expiration delay on the publicbt tracker, adding several content identifiers to the tracker, and then performing a scrape-all every 10 minutes2 .

Fig. 4 presents a cumulative distribution function of the expiry time on the publicbt tracker. We observe that entries remain valid on the tracker for an average period of 2823 seconds (∼47 minutes), with a minimum of 2275 seconds (∼38 minutes). This large delay allows asynchronous communications, since the message will remain available on the tracker for dozens of minutes. fraction

•• • • • •• • • •• • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • •• • • • • • • • • • •• • • • •• • •• • • • • •• • • •

Data loss

As noted in Section 3, some data blocks can be lost in addition to the erasures caused by the previously discussed expiration delay. Indeed, it may happen that a part of the data blocks written on the tracker are never found in the identifier lists returned by the scrape-all. By performing a number of write operation on the tracker while periodically (every 10 minutes) performing scrape-all operations, we have estimated the fraction of blocks lost, observing over the set of 10 experiments, an average loss rate of 44.92%. As stated in Section 3.5, data losses can be tolerated with the aid of an erasure coding scheme, for instance, a Reed-Solomon code.

The amount of redundancy (determined by the code rate R) added by the coding scheme must be chosen according to the loss rate of the channel on which the data is transmitted. In theory, to reliably transmit data over a channel of loss rate p, one need to use a coding scheme configured with a code rate R < 1p. In practice, because the actual loss rate can vary around the computed average, one must take a margin from the theoretical value. In the following, we will consider coding schemes configured with code rates ranging from R = 1/2 (close to the theoretical limit of 1p = 0.5508) to R = 1/5.

Performance Analysis

This section studies the performance of the proposed communication system. In particular, we evaluate the transmission success rate as well as the throughput of write and read operations. We have implemented a prototype comprising a writer and a reader and performed experiments using the centralized tracker publicbt.com. We consider a scenario were a unique sender wants to transmit a message to a unique receiver. The system is configured with a hash-size of t = 32 bits, and an index composed of s = 6 bits, leaving 160 -6 -32 = 122 bits of payload in info_hash. A message is divided into k blocks of 122 bits, that are then encoded by the erasure protection scheme into n block of 122 bits. An index of s = 6 bits along with a hash of t = 32 bits are happened to each of those n blocks, before being encrypted with a key shared by the sender and the receiver. With those parameters, the expected false positive rate of the hashbased identification is 6.67 10 -5 , and the maximum number of data block (including the data produced by the erasure protection scheme) is 2 s = 64.

Transmission success rate

As explained in Section 4, information written on the centralized tracker can be erased. The Reed-Solomon codes [START_REF] Reed | Polynomial codes over certain finite fields[END_REF] are used to provide resilience against erasures. Several configuration with various message sizes and code rates have been considered. We have considered messages fitting in 2, 4, 8, 16 data blocks and code rates varying between 1/5 and 1/2.

For each set of parameters (message size and code rate) we perform the write and read operations and observe the success rate of the transmission of the entire message. For the write operations, the data blocks are distributed amongst 5 threads that performs the write operations in parallel. At the same time, read operation are performed at regular interval (every 10 minutes). We then compute the success rate of a read operation as a function of the time elapsed since the end of the first write operation. A read operation is considered successful if the information contained in the retrieved scrape file is sufficient to decode the message. The experiment is performed 10 times for each set of parameters. Note that the success rate depends on the data retrieved from one scrape operation. Also note that the success rate could be further increased by considering the information retrieved over multiple read operations.

The associated results are presented in Fig. 5. We have limited the results shown to the configurations that have provided the best performances. Focusing on the the selected configurations, there is a time frame during which a read operation is always successful. The length of this time frame depends on the parameters, and ranges as depicted on Fig. 5, from 1700 seconds to 2350 seconds, allowing for asynchronous transmission as the message can be read anytime during a time frame of several tenths of minutes.

Inria

Transmission throughput

The proposed hidden channel will have an associated throughput, i.e. the data rate at which the sender will be able to transmit data to the receiver. As all communications are based on elementary operations, we first measure the time required to perform these in a series of 100 experiments. Fig. 6 shows the resulting cumulative distribution of the time duration for elementary write and read operations. We can observe that the read time can take significantly longer than the write operation, with 50% of read attempts having a duration longer than n 450 seconds. We note that to transmit a message, a number of write operations need to be done (one for each block i.e. elementary message), while only one elementary read operation is required (the scrape-all operation). Consequently, the time to write a message will depend both on the message size (number of blocks) and the elementary write delay, while the read operation will result in a constant delay. Assuming a large number of write operations, the throughput can therefore be approximated by the throughput of the write operation. Table 5.2 presents a summary of the throughput results, for the following parameters: s = 6 and t = 32, with 122 of useful bits per data block that can be used to transmit information. With the elementary read operation resulting in an average delay of 111.289 seconds and the elementary write operation an average delay of 65.475 seconds, the resulting write throughput (and the system throughput) is 1.89 bits per seconds. Note that performing the write operations in parallel has a potential to increase the system throughput.

• • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • • •• • • • • • • • • •••• •• •• • • • • • • • • • ••• • • • • • • •
• • • • • • • •• • • • • • • • • • • • • • • • • • • • • • • • • • •• • • • •• • • •• • •• •• •• • • • •• •

Detectability Analysis

We now discuss the difficulty of detecting our covert-channel based communication. We consider two types of wardens: a weak adversary (monitoring warden) that has no knowledge of the scheme used for communications, and a strong adversary that knows all the parameters of the used scheme, with the exception of the secret key used to encrypt the data, as discussed in section 3.3. The goal of a warden ignoring the proposed protocol is to spot communication corresponding to our scheme. We will now discuss the characteristics of the traffic generated by our scheme, and how they can be used to be classified as suspicious by the warden.

Focusing on the application layer protocol, both communicating parties are only relying on HTTP, and more particularly on the GET request. This request is one of the most common message used on the Internet, as loading a single web page requires several of these requests. Therefore, from a protocol point of view the traffic generated by the communicating parties will look like genuine web traffic to the warden. The warden could use the content (announce and scrape-all requests) to identify the targegeted application, i.e. BitTorrent. The warden could also come to the same conclusion by analysing the destination of the requests that are BitTorrent trackers (lists of BitTorrent trackers are available on-line3 ). While the application targeted by those HTTP requests, i.e. the tracker component of the BitTorrent system, may not be as common as web services, it is still one of the most popular services of the Internet and has been reportedly used by millions of users 4 .

The goal of a warden aware of the protocol could be to detect the communicating parties and the traffic corresponding to our scheme. Also, the warden may already know the identity of one party and could try to identify the other party.

The warden should first focus on the traffic directed to the centralized BitTorrent trackers, and more particularly to trackers providing the functionality required by our scheme (open centralized tracker supporting scrape-all requests). All the BitTorrent clients performing announce requests should be considered as potential writers while all the clients performing scrape-all requests should be considered as readers. As stated before, the second category can be rather small while the first can be very large. Indeed, the number of clients connected to a tracker at the same time can scale up to 100.000's peers [START_REF] Andrade | Influences on cooperation in bittorrent communities[END_REF]. To the best of our knowledge, no information on the number of clients performing scrape-all requests is available. Nevertheless, given the specific nature of this request, we can conjecture that the number of clients will be small. The latter property makes our system asymmetric in terms of detection difficulty: discovering the identity of the writer is much more difficult than discovering that of the reader. This feature suits well the scenario where an insider is attempting to exfiltrate information to the outside.

Announce requests performed by the writer are using content identifier forged for the purpose of the protocol, and are therefore not corresponding to real content shared on the BitTorrent ecosystem. List of contents shared in the BitTorrent ecosystem can be found on websites like The Pirate Bay. The warden could use this information to verify that the identifier corresponds to real content, but in fact there is a significant part of content shared in the BitTorrent ecosystem that is not found on the common torrent databases. Therefore, this technique could be used to narrow down the search, but will not be enough to identify the writer. Finally we want to highlight two features of our scheme that make the detection even more difficult. First, as opposed to many other covert channels, no direct connection is ever established between the communicating parties. This means that the warden may not even suspect that the parties are exchanging information. Second the system is asynchronous, i.e. the read operation can be done several ten's of minutes after the write operation. Thanks to this feature the temporal correlation between the writer and the reader activity can be kept at a low level.

Application to Distributed Hash Table

In BitTorrent, the role of the centralized tracker can be replaced by a decentralised alternative, based on distributed hash table (DHT). Applying our communication schemes to the DHT is an appealing solution, as the distributed nature of the DHT makes it highly resilient and difficult to monitor by a warden. However, tracker and DHT differ in a number of aspects that prevent the direct application of our scheme on a DHT. In this section we describe how our covert channel communication scheme can be adapted to a DHT.

Distributed Hash Tables in BitTorrent

Distributed hash tables, used as decentralized trackers in P2P systems, are used to store a number of (key,value) pairs. In a DHT, each node is in charge of storing a subset of the (key,value) pairs. This distributed data structure implements a push operation to store (key,value) pairs and a get operation to retrieve a value corresponding to a given key.

A number of P2P file sharing system lookup functionalities are provided by a DHT, with several BitTorrent clients supporting the use of a DHT in order to find peers sharing a specific content. For instance, Vuze, a popular BitTorrent client, uses a variant of the highly efficient Kadelmia DHT [START_REF] Maymounkov | Kademlia: A peer-to-peer information system based on the xor metric[END_REF]. This DHT stores pairs of the form (info_hash, peer_info), where peer_info is a tupple {IP_address, port_number}. A client joining a swarm contacts the node in charge of the corresponding key (the info_hash of the content) to get a list of peers and to add itself to this list. This functionality provided by the DHT is identical to what is provided by a centralized tracker.

However the DHT does not support the scrape-all request, that allowed our reader to get the full list of content registered on a centralized tracker. Recall that this feature was essential to our tracker-based system, as the information was hidden in those content identifiers. In fact, the only way to retrieve/store information from/to the DHT is by providing a content identifier.

Since the IP part of the peer_info is set to that of the requesting peer, there is only one piece of data left that can be arbitrarily chosen: the port number. The port number is a 16bits unsigned integer designating the port on which the BitTorrent peer listens to incoming connections.

System description

We propose to use the port number to convey information and to use the content identifier as a key for the communication. The atomic write operation is done by adding a new pair (i, IP : port_number) to the DHT, where i is the content identifier, IP is the IP address of the writer and port_number contains the hidden data. In return, the atomic read operation is performed by retrieving the peer_info associated to the content identifier i. The DHT can then be seen as a memory in which the content identifier i is the memory address, while port_number is the data stored at this address. A get request for the content identifier i would normally return only one value IP:port_number, making the extraction of the data straightforward.

Starting from the atomic read and write operations, a more advanced anonymous communication system can be built. The communicating parties will use an ordered list of k content identifier I = {D i } 1≤i≤k to designate the address at which the data will be stored in the DHT. In addition some of the features of the original system can be reused. First, the Hash-based filtering can be employed to prevent the genuine DHT activity from interfering with our system. Finally, encryption and erasure coding can be directly applied to provide respectively obfuscation and loss resilience. Note that the indexing feature is not required anymore, as the content identifier list I provides an implicit index.

The management of the content identifier list I could hamper the usability of the system, as the length of the communication must be known in advance and the exchange and storage of those identifiers can be costly. Instead we propose to use a list of identifiers generated by Pseudo Random Number Generator (PRNG) initiated by a seed shared by the communicating parties. Thanks to that, content identifier can be generated on the fly, ensuring a potentially infinite stream of messages while keeping to a minimum preliminary communication as well as memory consumption.

Performance and detectability

In the Kademlia DHT implemented by Vuze, a piece of data is erased from the node eight hours after the last access [START_REF] Geambasu | Vanish: Increasing data privacy with self-destructing data[END_REF]. Therefore, once a message was sent to the DHT we can expect that it will remain available to the reader for the same time period (eight hours). We note that the corresponding time window is much larger than for the centralized tracker-based system (where it is at most 3600 seconds) and allows for asynchronous communication in which read and write operations can be performed with a difference of several hours.

DHTs are designed to be highly resilient storage systems. Indeed their distributed nature as well as data replication (each piece of data is replicated over 20 different nodes) make the loss of data an extremely rare event [START_REF] Geambasu | Vanish: Increasing data privacy with self-destructing data[END_REF].

Using the DHT instead of a centralized tracker would increase the scalability of our system. Indeed, in the centralized tracker based system both read and write operations involve the tracker. The write operation is relatively lightweight, but the read operation puts the tracker under a heavy load as it requires the transfer of a several Megabytes file. Whereas in a DHT-based approach, the random distribution of the data over the DHT nodes distribute the load over a large number of hosts, allowing for the use of a larger number of covert communications in parallel.

The detectability of this scheme, due to the nature of the communication used by the DHT, slightly differs from the centralized tracker-based version. In particular, the read and write operations both use Kadelmia RPC commands embedded in UDP packets. These requests are less common than the HTTP/GET requests used by the centralized tracker-based scheme, and therefore potentially easier to detect. One advantage of the DHT approach though is the large scale system in which the communication can be hidden. Indeed, if it is quite challenging for a warden to monitor the communication over potentially millions of DHT nodes.

Inria 8 Related works

Ephpub [START_REF] Castelluccia | Ephpub: Toward robust ephemeral publishing[END_REF] is a DNS-based ephemeral communication scheme which makes use of DNS server caches to store information. Although the main goal of this system is not to provide anonymous communications, and rather provides ephemeral publication of data (i.e. encrypted data with a lifetime of the key to decrypt it), it shares several aspects with the system proposed in this paper. Indeed, both systems employ a common Internet service to store information, and no direct connection between the communicating parties is required.

Another tool aiming to provide ephemeral publication is called Vanish and has been introduced in [START_REF] Geambasu | Vanish: Increasing data privacy with self-destructing data[END_REF]. In Vanish, the key used to encrypt a message between two communicating parties is stored on the DHT, ensuring that the message becomes unreadable once the key disappears because of information erasure (either due to expiration delay or churn) on the DHT. As in the DHT extension described in our work (Section 7) the sender uses the DHT to store pieces of information that will be later retrieved by a receiver informed of their locations. However, Vanish leverages the DHT to only store bits of the crypto-system keys. Vanish makes use of the Shamir secret sharing scheme, and randomly stores bits of the key on different nodes of the DHT (used as an index storage). Our proposed DHT-based asynchronous covert communication scheme exploits the DHT to store the data itself and relies on the tracking capabilities of the DHT, rather than the storage property.

In [START_REF] Starnberger | Overbot -a botnet protocol based on kademlia[END_REF], authors present Overbot, a stealth command and control channel using the Kadelmia distributed hash table. The objective of this system is to allow compromised nodes to declare themselves to the botmaster and then to receive commands. The botmaster deploys a number of sensor nodes in the DHT, that are in charge of receiving command requests from compromised nodes. Those requests are embedded into genuine DHT requests but include an encoded message that can only be recognized by the botmaster. Once a request for command is received, the bostmaster redirects the compromised node to another controlled node of the DHT, an actuator node, that is in charge of delivering the command. Similarly to our system, Overbot hides its communication within legitimate traffic so that those communications appear to be genuine traffic for an external observer. However, in Overbot a direct connection is established between the different entities (sensor/actuator nodes and compromised nodes), while in our scheme, direct communications between the parties never occurs.

Use of the BitTorrent system to provide a covert channel has been previously investigated in [START_REF] Eidenbenz | Hidden communication in P2P networks steganographic handshake and broadcast[END_REF], where authors propose implementation of covert channels using various functionality of the BitTorrent system. One of the covert channels exploits the fact that the order in which the data blocks are exchanged is left unspecified (on purpose). The conspiring nodes can then perform a mutual identification by exchanging a shared secret encoded by the requested block order. As opposed to our system, this work only considers communication through direct exchange of data between the communicating parties. This could be successfully exploited in a de-anonymization process if one of the parties involved into the communication is identified. communication through direct exchange of data A number of P2P systems providing anonymity have been proposed, like GNUnet and Freenet 5 . We note that the purpose of these systems is to provide anonymous communications and not covert communications like our proposal. Indeed, the identity of the communicating parties is hidden, but the data exchange itself is not hidden at all.

Conclusion

We have presented a new covert channel based on a widely used service available on the Internet: centralized BitTorrent trackers. Our system does not require the cooperation of the tracker and allows the sending of data at a moderate rate. We have implemented a prototype that demonstrates the practicality of our proposal and evaluated the performance of our system. By analyzing the scheme under two attacker models, with the monitoring warden being either the strong or the weak adversary, we have shown that the nature of the communications involved in the proposed scheme makes the detection and blocking of the communications difficult. Finally, we have presented an extension of this scheme that relies on the decentralized, DHT based, trackers in the BitTorrent system.

Figure 1 :

 1 Figure 1: Read and write operation on the tracker.

Figure 2 :

 2 Figure 2: Encoding of a message spanning over several blocks.

Figure 3 :

 3 Figure 3: Creation of the forged content identifier.

Figure 4 :

 4 Figure 4: Expiration delay distribution.

Figure 5 :

 5 Figure 5: Success rate as a function of the time elapsed since the end of the first write operation.

Figure 6 :

 6 Figure 6: Cumulative distribution of the time required to complete the elementary operations of read and write.

1 7 4 5 . 1 11 6Analysis 12 7

 17511112 Read and Write operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Hash-based filtering for packet identifications . . . . . . . . . . . . . . . . . . . . 5 3.3 Obfuscation through encryption . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.4 Data indexing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.5 Data loss and erasure coding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.6 Summary of the covert channel mechanism . . . . . . . . . . . . . . . . . . . . . System analysis 7 4.1 False-positive of the hash-based filter . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.2 Entry's lifetime . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 4.3 Data loss . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 5 Performance Analysis 9 Transmission success rate . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 5.2 Transmission throughput . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Detectability Application to Distributed Hash Table 13 7.1 Distributed Hash Tables in BitTorrent . . . . . . . . . . . . . . . . . . . . . . . . 13 7.2 System description . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 7.3 Performance and detectability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 Inovallée 655 avenue de l'Europe Montbonnot 38334 Saint Ismier Cedex Publisher Inria Domaine de Voluceau -Rocquencourt BP 105 -78153 Le Chesnay Cedex inria.fr ISSN 0249-6399

Table 1 :

 1 Summary of the delay introduced by the elementary operations and the resulting throughput.

	Operation	Elementary operation time min / avg / max	Average throughput
	Write	0 / 65.475 / 532 s	1.89 b/s
	Read	86 / 111.289 / 175 s	NA

RR n°8554

This value has been chosen to limit the load on the tracker on the one side, and because the scrape-all file is refreshed every 10 minutes Inria

http://www.torrentking.org/

http://torrentfreak.com/bittorrent-surges-to-150-million-monthly-users-120109/.Inria

Freenet https://freenetproject.org/ and GNUnet https://gnunet.org/ RR n°8554


Gwenaël Delaval
email: gwenael.delaval@inria.fr

Modular Distribution and Application to Discrete Controller Synthesis

Keywords: Discrete controller synthesis, automatic distribution, type systems

This paper shows the application of the automatic distribution of synchronous reactive programs to the specific problem of discrete controller synthesis of complex reactive systems. Discrete controller synthesis is a formal method used to ensure properties on a flexible system which does not a priori verify them. However, this method is efficient only on Boolean programs. More complex embedded systems, comprising complex data types and structures, cannot be addressed without abstraction means. We show how such abstractions can be obtained automatically using a type-directed projection operation. This operation allows then the safe recombination of the result of the synthesis with the original abstracted system, preserving the ensured properties.

Introduction

Reactive embedded systems, due to their strong interaction with their environment, are intrinsically critical. The failure of such systems can involve serious human or ecological damages. For these reasons, there is a strong need of formal methods for the design of such systems, in order to ensure formal properties on them.

We address here the problem of ensuring properties by mean of an automatic method of transformation of the original program. Some of these methods cannot be applied on complex and general programs, unless performing a preliminary separation of the program in two parts, one on which the automatic transformation is performed, and one with the other computations. This separation can be fastidious, and the recombination of the two parts raises safety and modularity issues. The contribution of this paper is to use an automatic type-directed distribution method to obtain on one hand an abstraction on which the transformation will be applied, and on the other hand the complementary of this abstraction, whose recombination with the transformed abstraction is safe and preserves the transformation. This work is based on [START_REF] Delaval | A type system for the automatic distribution of higher-order synchronous dataflow programs[END_REF], where a type-directed projection operation is defined in order to address the modular distribution of reactive programs, and consists of both an adaptation of this method and an illustration of its application towards a specific distribution problem, namely here separate compilation and analysis of centralized systems.

Figure 1 sums up this method: P is the original program distributed into P 1 and P 2 . The transformation is applied on P 2 , giving the program P ′ 2 , then recombined safely with P 1 . We show the application of this method on a specific transformation, the discrete controller synthesis [START_REF] Altisen | Using controller synthesis to build propertyenforcing layers[END_REF], whose goal is to ensure properties on a partial design. This method allows the programming of both parts of a program, for example here the control part and the data part, in the very same language and in an integrated way, thus giving the programmer more control on the semantics of the written programs.

The properties we wish to address here are temporal logic properties like the evolution of values of inputs and outputs of the program during time. An example of such property can be expressed as "the event B will always occur after the event A". These properties are commonly checked by the use of automatic tools (e.g., model-checking tools [START_REF] Halbwachs | Synchronous observers and the verification of reactive systems[END_REF]), on a conservative abstraction of a fully designed system. Another approach lies in discrete controller synthesis (DCS) [START_REF] Ramadge | Supervisory control of a class of discrete event processes[END_REF]: given a partially designed system and temporal properties, this method computes automatically a controller, actuating on the partial system, and ensuring the required properties. This method has shown its interest for embedded systems in [START_REF] Altisen | Using controller synthesis to build propertyenforcing layers[END_REF].

However, this method is efficient only on a Boolean state-based abstraction of the system [START_REF] Marchand | Synthesis of discrete-event controllers based on the signal environment[END_REF]. This abstraction can involve addition of inputs (e.g., Boolean values from comparison of scalar data) and masking of other ones. The use of this method also involves separate compilation of the state-based abstraction of the original system, thus exposing the final system to consistency problems, such as data or control consistency. Moreover, as current DCS algorithms apply only on global programs, the Boolean abstraction needs to be inlined.

We present here an automatic method allowing the generation, from a unique source program, of a Boolean state-based abstraction (named Boolean fragment hereafter, on which we will perform the DCS to ensure the required properties), and a program performing the other data computations (named data fragment). We show how our method allows the correct automatic recombination of the data fragment with the controlled Boolean fragment, once discrete controller synthesis has been performed on it. This separation of the Boolean and the data fragments also allows us to only inline the part on which the DCS is applied, thus keeping the original modularity structure of the initial program in the data part, thus allowing, for example, to use higher-order features in it.

This paper is organized as follows: Section 2 gives an overview of our method.

A C D B C u 1 ∧ ¬u 2 /c u 1 u 1 C D u 2 ¬u 1 ¬u 1 u 2 ∧ c u 1 P ¬c ¬u 1 ¬u 1 ∧ ¬c ¬u 1 ∧ u 2 ∧ c A B u 1 ∧ ¬u 2 ∧ c u 1
Fig. 2. Example of discrete controller synthesis.

Section 3 shows an application example. Section 4 presents the language used, Section 5 the type-directed projection operation, and Section 6 the application of DCS on the two obtained fragments. Finally, Section 7 discusses our method and presents some prospects.

Overview

Discrete controller synthesis operates on Boolean reactive systems, often expressed as automata. Temporal logic properties are then expressed as properties on the set of traces of these automata. Given a partial program P and a property Φ not satisfied a priori by P , the discrete controller synthesis computes a controller C, such that the synchronous composition of P and C is a program which satisfies Φ. The partial nature of a program is expressed by additional inputs named controllable inputs, whose values will be defined by the computed controller. This set of controllable inputs is denoted I c , and therefore the discrete controller synthesis operation will be noted DCS(P, I c , Φ). By opposition, actual inputs coming from the program environment are called hereafter uncontrollable inputs and denoted I u . Sigali [START_REF] Marchand | Synthesis of discrete-event controllers based on the signal environment[END_REF] and Supremica [START_REF] Akesson | Supremica -a tool for verification and synthesis of discrete event supervisors[END_REF] are examples of DCS tools. Figure 2 shows an example of discrete controller synthesis. Synchronous programs are expressed as Mealy machine. The program P , on the left, has two uncontrollable inputs u 1 and u 2 , and a controllable input c (underlined, as every controllable input in the following). This program is partially designed: in state A, with the input u 2 , two possibilities have been specified as correct by the programmer: staying in state A, or going to state C. Let assume now that, for safety reasons, we want to ensure that the state D will never be reached (expressed as the CTL formula Φ = ∀✷¬D). Then, the computation of DCS(P, {c}, Φ) produces the controller shown on the right of Figure 2, which gives, at occurrences of u 2 in state A, the false value for the controllable input c. The result of the synchronous product of P and C is a program where, for any sequence of inputs u 1 and u 2 , the state D is never reached.

Such methods can only be applied on Boolean state-based systems. Moreover, these methods are not very scalable: they cannot handle, without abstraction, more complex systems (e.g., mixing Boolean and numerical values). Two solution exists to alleviate these problems: a Boolean abstraction must either be extracted of the whole system, or it can be designed apart. The first solution can involve arbitrary complex manual work to obtain an abstraction, then the recombination of the controlled abstraction and the original system. This is why the second solution is considered in the framework of the design of embedded systems in computation/control layers [START_REF] Rutten | A framework for using discrete control synthesis in safe robotic programming and teleoperation[END_REF]. This paradigm allows the design of embedded systems in terms of, on one hand, a computational layer, comprising the implementation of complex functional tasks like control law, signal processing; and on the other hand a control layer, purely reactive, allowing the schedule of the functional tasks.

Thus, these two parts can be separately designed and compiled, and specific analysis tools (model-checking or discrete controller synthesis) can be used for the reactive part. Another interest of this separation approach is to design modular reactive patterns, tested and formally checked once, and reusable for several designs. This approach has shown its interest for domain-specific approchs, like Orccad [START_REF] Borrelly | The Orccad architecture[END_REF], where the Robot-tasks are such modular patterns, or the Nemo language [START_REF] Delaval | A domain-specific language for multitask systems, applying discrete controller synthesis[END_REF].

However, this separate design can be problematic for the global simulation and analysis of the system. Furthermore, it yields a lack of modularity and flexibility of the control interface, especially in the case of use of domain-specific patterns, the approach commonly taken being specific code duplication and inlining. Mode automata [START_REF] Maraninchi | Mode-automata: a new domain-specific construct for the development of safe critical systems[END_REF], as well as further work on synchronous languages [START_REF] Colaço | A Conservative Extension of Synchronous Data-flow with State Machines[END_REF], has addressed such problem by adding automata as control structures in the dataflow languages Lustre [START_REF] Halbwachs | The synchronous data-flow programming language Lustre[END_REF] and Lucid Synchrone [START_REF] Caspi | Synchronous Kahn networks[END_REF][START_REF] Pouzet | Lucid synchrone v3, release and reference manual[END_REF]. Figure 3 shows an example of mode automata, with its equivalent specification in Lucid Synchrone. This automaton is composed of two modes or states, one increasing the global variable x (named I), one decreasing it (D). The transition from I to D (resp. D to I) is taken when x ≥ 10 (resp. x ≤ 0), and the controllable input c is true (this allow the controller to inhibit the transition between the two modes).

These two complementary approaches, global simulation and analysis, and separate compilation, can be both applied on the same system, by means of the application on dataflow languages extended with automata of an automatic distribution method, allowing us to obtain several fragments from a whole program, on which separate analysis and compilation can be applied, before safe recombination. Applying this method for discrete controller synthesis, the goal would be to obtain two fragments, a Boolean abstraction on one hand, and the remaining computations on another. Figure 4 shows the application of this method on the automaton of Figure 3. The Boolean fragment is shown on the left, and the remaining computations are performed by the automaton on the right. For the communication of values from one fragment to the other, u 1 and u 2 are added as outputs of the second automaton, and as uncontrollable inputs on the Boolean fragment. c 1 and c 2 are added conversely to communicate the result of Boolean computations. In the following, we will keep the convention of calling u (resp. c) the channel communications from the data fragment to the Boolean fragment (resp. from the Boolean to the data fragment). The synchronous composition of these two automata is semantically equivalent with the automaton of Figure 3.

c 1 c 1 = u 1 ∧ c c 2 I D c 2 = u 2 ∧ c c 1 x = last(x) + 1 x = last(x) -1 c 2 I D u 1 = (x = 10) u 2 = (x = 0)
Figure 5 sums up our method. Once the two fragments P b and P d have been obtained from the original program P , the discrete controller synthesis can be performed on the Boolean fragment P b , and the composition of this Boolean fragment with the computed controller C can then be safely composed with the other computations obtained by the distribution. I db and I bd are respectively the set of communication channels added from P d to P b (so as outputs of P d and uncontrollable inputs of P b ), and the way back. The synchronous composition of the Boolean fragment with its controller is performed by plugging the inputs I u and I db as inputs of the controller, and the output of the controller as controllable inputs of the fragment.

Application

Figure 6 shows as illustrating example the programming of a pattern named task, representing a delayable task. This pattern is a higher-order node: its parameter f is the function to be executed by an instantiation of this task when it is active, req and stop are two Boolean requesting respectively the launch of the task and its end, and x is the input of f. The task is delayable because an input ok can delay it when it is requested. This input will be instantiated with controllable ones. The outputs of this task are the output y of f, and a Boolean act, true when the task is actually active. The main node then contains two instantiations of this pattern. Programs are here written in the simplified syntax used further in Section 4. The concrete syntax of Lucid Synchrone can be seen in [START_REF] Pouzet | Lucid synchrone v3, release and reference manual[END_REF].

Performing a type-directed distribution allows for this distribution to be modular. Thus, one node will result in exactly one node on each fragment. In order to do this modular operation, the typing approach allows us to attach to each node the information about where its inputs and outputs are located (i.e., on which fragment they have been computed), and what fragment and what communication channels y1,act1,c1,c2,c3,c4 = task((), u1, ok1, u2, ()) and y2,act2,c5,c6,c7,c8 = task((), u3, ok2, u4, ()) are involved by this node's computation. The result of the partition of this program is shown in Figures 7 and8. On the Boolean fragment (Fig. 7), the node task has four additional outputs for each transition. Thus, as this node is instantiated twice in the main node, eight outputs c1 to c8 are added. The controller computed on this abstraction can, e.g., ensure that these two tasks will never be active at the same time (∀✷¬(act1 ∧ act2)).

I A W c 2 act = false c 1 c 3 c 4 c 2 = (req ∧ ¬ok) act = false c 1 = (req ∧ ok) c 3 = ok act = true c 4 = stop
The abstraction with other computations is given in Figure 8. The outputs added in the Boolean abstraction are here added as inputs, and new outputs are added, holding the values of comparisons (u1 to u4).

Both fragments comprise an automaton, whose states and transitions match with the original one. The targeted behaviour is a Boolean fragment computing transitions, and a data fragment receiving scheduling instructions under the form of triggered transitions between computing states. Unused values (f and x on the Boolean fragment, req, ok and stop on the data one) are replaced by the special value ().

The language

The language we consider is a dataflow language, extended with automata. It follows the following syntax: A program P is a sequence of node definitions, followed by a set of equations (the "main" of the program). A node definition d takes as input a pattern p, comprising a sequence of uncontrollable inputs (x). Its output is an expression e, evaluated within the scope of a set of equations D.

Definitions D are either an empty definition ǫ, single equations defining patterns of variables (p = e), definitions naming the result of an application (p = x(e)), parallel declarations (D and D), or an automaton, composed of a sequence of states S defined by one handler h (automaton S → h . . . S → h end). An automaton handler is a definition followed by a sequence of transitions.

An expression e may be an immediate value (i), a variable (x), a pair construction (e, e), a binary combinatory operation (op(e, e), where op can be +, -,. . . ), an initialized delay (e fby e). The pair construction is left-associative, and thus we denote by e 1 , . . . , e n the expression (. . . (e 1 , e 2 ), e 3 ), . . .), e n ).

Type-directed projection

The type system is adapted from [START_REF] Delaval | A type system for the automatic distribution of higher-order synchronous dataflow programs[END_REF]. It is extended with automata, and simplified to answer the specific problem of separate compilation of a program in two parts (i.e., two locations). The target architecture here is then composed of two "locations", named A b and A d (A b will be the Boolean fragment and A d the data fragment), which are connected to each other in both directions.

Our type system associates to each expression and definition a spatial type, which expresses on which fragment (Boolean or data) this expression or definition is located or defined. For example, a value of spatial type bool at A d is a Boolean value located (and then, usable) on the data fragment. The spatial type of a node taking as input a Boolean, whose output is a Boolean, and which is only computable on the Boolean fragment without internal communication, will be of spatial type bool at A b -{A b }/∅ → bool at A b . It is a type and effect system [START_REF] Talpin | Polymorphic type, region and effect inference[END_REF], as with its spatial type, we associate to each expression and definition the set of fragments, and the channels involved in its computation. As a more complete example, the type of the node task of Figure 6 will carry the fact that it takes as input a node whose input, output, and computation are on A d (the data fragment), three inputs on A b (the Boolean fragment) and one on A d , that its output is a pair whose first component is on A d and its second one on A b , and that the computation of task involves the two fragments A b and A d and four communication channels from A b to A d :

∀α. (α at A d -{A d }/∅ → int at A d ) × bool at A b × bool at A b × bool at A b × α at A d -{A b , A d }/T → (int at A d × bool at A b ) where T = [A b c 1 → A d , A b c 2 → A d , A b c 3 → A d , A b c 4 → A d ]
The syntax of spatial type expressions is:

σ ::= ∀α 1 , . . . , α n .∀δ 1 , . . . , δ p .t t ::= b | α | t at s | t -ℓ/T → t | t × t T ::= [A 1 c 1 → A ′ 1 , . . . , A n cn → A ′ n ] if ∀i = j, c i = c j H ::= [x 1 : σ 1 , . . . , x n : σ n ] if ∀i = j, x i = x j b ::= int | bool | . . . s ::= A b | A d | δ ℓ ::= {s 1 , . . . , s n }
H denotes spatial typing environments. We distinguish spatial type schemes (σ), which can be quantified, from simple spatial types (t). A simple spatial type can be either a stream base type (b, like integers, Booleans, . . . ), a type variable (α), a located type (t at s), a node type (tℓ/T → t), or a pair type (t × t). A location is either one of the two constant location A b (for the Boolean fragment) and A d (for the data fragment), or a location variable δ. ℓ denotes sets of locations (hence limited here to subsets of {A b , A d }, or singleton {δ}).

A value of spatial type t at s is a value located on s. A value of spatial type t 1ℓ/T → t 2 is a node whose input is of spatial type t 1 , whose output is of spatial type t 2 , and whose computation involves the set of locations ℓ.

So as to allow, e.g., the instantiation of a type scheme of the form ∀α.α at s by the type int at s -{s}/∅ → int at s, we extend the equality relation between types. Thus, the following equalities stand:

(t 1 × t 2 ) at s = (t 1 at s) × (t 2 at s) (t 1 -{s}/∅ → t 2 ) at s = (t 1 at s) -{s}/∅ → (t 2 at s) t at s at s = t at s t 1 = t ′ 1 t 2 = t ′ 2 (t 1 × t 2 ) = (t ′ 1 × t ′ 2 ) t 1 = t ′ 1 t 2 = t ′ 2 t 1 -ℓ/T → t 2 = t ′ 1 -ℓ/T → t ′ 2
The notion of well-formed types is introduced, because one cannot associate a meaning to any type: e.g., the spacial type int at A b at A d cannot appear in the type system. A spatial type t is well-formed iff ∀t ′ , s 1 , s 2 , t = t ′ at s 1 at s 2 ⇒ s 1 = s 2 .

Every type in the type system is assumed to be well-formed, and typing algorithms maintain this invariant during typing. The instantiation mechanism is defined as follows:

t[t 1 /α 1 , . . . , t n /α n , s 1 /δ 1 , . . . , s p /δ p ] ≤ ∀α 1 . . . α n .∀δ 1 . . . δ p .t
The generalization mechanism is restrained for the projection. We allow type schemes to comprise at most one location variable. In that case, the type scheme is of the form ∀α 1 . . . α n .∀δ.t at δ, and the projection consists in placing the value of this type on the two fragments.

We note respectively FLV(t) and FTV(t) the set of free location variables and free type variables of the type t. FLV and FTV are straightforwardly extended to typing environments. The generalization of t in typing environment H is noted gen H (t), defined as: gen H (t) = ∀α 1 , . . . , α n .∀δ 1 , . . . , δ p .t where {α 1 , . . . , α n } = FTV(t) -FTV(H) {δ 1 , . . . , δ p } = FLV(t) -FLV(H) p ≤ 1

The function locations(•) gives the set of locations involved in the spatial type given as argument. It is defined as:

locations(t 1 × t 2 ) = locations(t 1 ) ∪ locations(t 2 ) locations(t 1 -ℓ/T → t 2 ) = ℓ locations(t at s) = {s}
This type system will also infer communication channels needed between the two fragments. A channel will be represented by added common variables between two fragments, i.e., added inputs on one side corresponding to added outputs on the other. Channels are named so as to be able to match these added variables in the two fragments. Formally, a channel is a location pair associated with a name, noted A 1 c → A 2 : c is the name of the channel, A 1 its source location, and A 2 its destination location. c is the common variable representing a communication between the two fragments. The set of channel names is totally ordered, so as to keep consistency of inputs and outputs added, from the node definition to node instances. T denotes channels sequences, in which channel names are disjoints. (T, T ′ ) denotes the concatenation of two channel sequences. dom(T ) is the set of channel names of T . For the sake of multiple instanciation of nodes, it is necessary to be able to rename channels, so as to keep these names disjoints in inferred channel sequences. Given two channel sets T and T ′ , we note T ′ ∼ = T the fact that T ′ is equal to T modulo a renaming of its channels:

T ′ ∼ = T ⇔ T ′ = T [c ′ 1 /c 1 , . . . , c ′ n /c n ]
where dom(T ) = {c 1 , . . . , c n } and dom(T

′ ) = {c ′ 1 , . . . , c ′ n }
Then, from a channel sequence T , we denote by T ↑ s (resp., T ↓ s) the channel sequence extracted from T and which source (resp., destination) is s.

∅ ↑ s = ∅ ([s c → s 2 ], T ) ↑ s = [s c → s 2 ], (T ↑ s) ([s 1 c → s 2 ], T ) ↑ s = (T ↑ s) iff s 1 = s ∅ ↓ s = ∅ ([s 1 c → s], T ) ↓ s = [s 1 c → s], (T ↓ s) ([s 1 c → s 2 ], T ) ↓ s = (T ↓ s) iff s 2 = s
Finally, a program is typed and projected with the initial environment H 0 = H op , H u , H c , where H op contains the types of the initially defined operations (Boolean operations being defined to be computed on A b , and other on A d ), and H u and H c respectively the types of the uncontrollable and controllable inputs.

H op =           • fby • : ∀α.∀δ.α at δ × α at δ -{δ}/∅ → α at δ, fst • : ∀α, β.∀δ 1 , δ 2 .α at δ 1 × β at δ 2 -{δ 1 , δ 2 }/∅ → α at δ 1 , snd • : ∀α, β.∀δ 1 , δ 2 .α at δ 1 × β at δ 2 -{δ 1 , δ 2 }/∅ → β at δ 2 , ( and
) : bool at A b × bool at A b -{A b }/∅ → bool at A b , . . . (+) : int at A d × int at A d -{A d }/∅ → int at A d , . . .           H u = [x u1 : t 1 at s n , . . . , x un : t n at s n ] H c = [x c1 : bool at A b , . . . , x cp : bool at A b ]
We note I u and I c respectively the sets of uncontrollable and controllable inputs:

I u = dom(H u ) and I c = dom(H c ).
The type system defines a judgment H ⊢ D : H ′ /ℓ/T , meaning that in teh typing environment H, the definition D yields the typing environment H ′ , and its computation involves the set of locations ℓ, and the communication channels T . This type system defines a type directed projection operation, performed on a typed program. For the sake of brevity, we will detail here only the rules of this projection operation. The rules defining the type system can be found in appendix.

The projection of a definition D on a location s is noted H ⊢ D : H ′ /ℓ/T s =⇒ D ′ , meaning that in the typing environment H, the definition D defines the environment H ′ , and its projection on s results in the new definition D ′ . ℓ is the set of locations involved, and T is the set of communication channels (i.e., added inputs and outputs) needed for the execution of D. The set of locations involved is used for the suppression of unused definitions and expressions.

This projection operation is straightforwardly extended to programs. Projection of expressions and transitions are noted respectively H ⊢ e : t/ℓ/T s =⇒ e ′ /D and H ⊢ u : ℓ/T s =⇒ u ′ /D, where D is in both cases an additional definition of outputs for communications occurring within e or u.

The type system is given in Figures 9 and10. An immediate value is located on any projected program (rule Imm). A projected variable results in itself iff it is located on the computed fragment (rule Inst).

The rules Comm-From and Comm-To define a subtyping mechanism for inserting communications between the two fragments. An expression e of type t at s, which is a value entirely located on s, can be communicated to the other fragment s ′ , and thus can be considered as being of type t at s ′ . The rule Comm-From defines a new communication channel as the value of e, and suppresses this expression in the projection. The rule Comm-To replaces this expression by this new communication channel. For example, this rule is applied, on the program of Figure 6, after the computation of (x1>0) on the data fragment. The channel added by this application is

A d u 1 → A b .
The projection of a pair is the projection of its compounds, new definitions of these compounds being put in parallel (rule Pair). The projection of an equation involves computing the projection of the expression, and putting in parallel with the projected equation the set of definitions of the communications channels (rule Def).

The rules Suppr-Expr and Suppr-Def allow the suppression of any expression on the fragment where no part of this expression is involved.

Projection of a node (rule Node) involves projecting its compounds, and then adding the communication channels used in these compounds as inputs and outputs of the resulting node, so as to allow multiple instantiations of this node : for example, c 1 to c 4 are added as outputs of the node task on the Boolean fragment (see Figure 7). The rules App-Keep and App-Suppr state that an application is kept iff the fragment computed appears in the set of fragments involved in the computation of the applied node. If it is kept, then the set of communication channels involved within this node are added as inputs and outputs of the application.

Figure 10 shows the rule for the projection of automata. The rules Trans-D and Trans-B state that an expression triggering a transition, once computed, must be located on the Boolean fragment. A communication channel is then added, from the Boolean fragment to the data one, holding the value of this expression (c 1 to c 4 on Figure 7). The projected transition holds then the expression composed only of the value of this channel. This channel is computed in the state where the transition can be triggered (rule Handler). Then, the projection of an automaton involves the projection of every handler (rule Automaton).

Given two programs P = d 1 ; . . . ;d n ;D and P ′ = d ′ 1 ; . . . ;d ′ p ;D ′ , we note P P ′ the synchronous composition of P and P ′ , defined as:

(d 1 ; . . . ;d n ;D) (d ′ 1 ; . . . ;d ′ p ;D ′ ) = d 1 ; . . . ;d n ;d ′ 1 ; . . . ;d ′ p ;(D and D ′ )
The semantics of a program P is given by a relation noted S i ⊢ P : S o , meaning that, given the sequence of inputs S i = R i 1 .R i 2 . . . ., the execution of the program P results in the sequence of outputs

S o = R o 1 .R o 2 .
. . ., where R denotes a reaction environment, mapping names to instantaneous values. The semantics is taken from [START_REF] Colaço | A Conservative Extension of Synchronous Data-flow with State Machines[END_REF] and not rewritten here. (App-Suppr) The following property is a refinement of the result stated in [START_REF] Delaval | A type system for the automatic distribution of higher-order synchronous dataflow programs[END_REF]. It states that the composition of the two fragments obtained by projection has the same semantics as the original program.

(Imm) H ⊢ i : b at s/{s}/∅ s =⇒ i/ǫ (Inst) t ≤ (H(x)) s ∈ locations(t) H ⊢ x : t/
H ⊢ D 1 : H 1 /ℓ 1 /T 1 s =⇒ D ′ 1 H ⊢ D 2 : H 2 /ℓ 2 /T 2 s =⇒ D ′ 2 H ⊢ D 1 and D 2 : H 1 , H 2 /ℓ 1 ∪ ℓ 2 /T 1 , T 2 s =⇒ D ′ 1 and D ′ 2 (Node) H, x i : t i , H 1 ⊢ D : H 1 /ℓ 1 /T 1 s =⇒ D ′ H, x i : t i , H 1 ⊢ e : t/ℓ 2 /T 2 s =⇒ e ′ /De (T 1 , T 2 ) ↑ s = [s c 1 → s 1 , . . . , s cn → sn] (T 1 , T 2 ) ↓ s = [s ′ 1 c ′ 1 → s, . . . , s ′ p c ′ p → s] H ⊢ node f (x 1 , . . . , xn) = e with D : [gen H ((t 1 × . . . × tn) -ℓ 1 /T 1 , T 2 → t)/f ]/ℓ 1 ∪ ℓ 2 /∅ s =⇒ node f (x 1 , . . . , xn, c ′ 1 , . . . , c ′ p ) = (e ′ , c 1 , . . . , cn) with D ′ and De (App-Keep) H ⊢ f : t -ℓ 1 /T 1 → (t 1 × . . . × tn)/ℓ 2 /T 2 s =⇒ f ′ /D 1 H ⊢ e : t/ℓ 3 /T 3 s =⇒ e ′ /D 2 s ∈ ℓ 1 T ′ 1 ∼ = T 1 T ′ 1 ↑ s = [s c 1 → s 1 , . . . , s cn → sn] T ′ 1 ↓ s = [s ′ 1 c ′ 1 → s, . . . , s ′ p c ′ p → s] H ⊢ x = f (
H ⊢ f : t -ℓ 1 /T 1 → (t 1 × . . . × tn)/ℓ 2 /T 2 s =⇒ f ′ /D 1 H ⊢ e : t/ℓ 3 /T 3 s =⇒ e ′ /D 2 s ∈ ℓ 1 T ′ 1 ∼ = T 1 H ⊢ p = f (e) : [t 2 /x]/ℓ 1 ∪ ℓ 2 ∪ ℓ 3 /T ′ 1 , T 2 , T 3 s =⇒ D 1 and D 2

Application of Discrete Controller Synthesis

The formal properties to be ensured by the final program will be expressed as properties on the sequence of outputs S o . Given a CTL property Φ, we note P |= Φ (Trans-D)

H ⊢ e : t at A b /ℓ 1 /T 1 A d =⇒ e ′ /D 1 H ⊢ u : ℓ 2 /T 2 A d =⇒ u ′ /D 2 H ⊢ until e then S u : ℓ 1 ∪ ℓ 2 /T 1 , T 2 , [A b c → A d ] A d =⇒ until c then S u ′ /D 1 and D 2 (Trans-B) H ⊢ e : t at A b /ℓ 1 /T 1 A b =⇒ e ′ /D 1 H ⊢ u : ℓ 2 /T 2 A b =⇒ u ′ /D 2 H ⊢ until e then S u : ℓ 1 ∪ ℓ 2 /T 1 , T 2 , [A b c → A d ] A b
=⇒ until cn then S u ′ /c = e and D 1 and D 2 (Handler)

H ⊢ D : H ′ /ℓ 1 /T 1 s =⇒ D 1 H ⊢ u : ℓ 2 /T 2 s =⇒ u ′ /D 2 H ⊢ D u : H ′ /ℓ 1 ∪ ℓ 2 /T 1 , T 2 s =⇒ D 1 and D 2 u (Automaton) ∀i ∈ {1, . . . , n}, H ⊢ h i : H i /ℓ i /T i s =⇒ h ′ i ℓ = ℓ 1 ∪ . . . ∪ ℓn T = T 1 , . . . , Tn H ′ = merge(H 1 , . . . , Hn) H ⊢ automaton S 1 → h 1 . . . Sn → hn end : H ′ /ℓ/T s =⇒ automaton S 1 → h ′ 1 . . . Sn → h ′ n end
Fig. 10. Rules for the projection operation (Automata).

the fact that the program P satisfies Φ. We only consider safety properties, i.e., properties of the form Φ = ∀✷ϕ, ϕ being a predicate on reaction environments. For instance, the property of exclusivity of the two tasks in the program of Section 3 can be expressed as ∀✷ϕ, with ϕ(R) = (R(act1) = false ∨ R(act2) = false).

Definition 6.1 (Safety property satisfaction)

• A sequence S = R 1 .R 2 . . . . satisfies a property ✷ϕ (noted S |= ✷ϕ) iff ∀i, ϕ(R i ).

• A program P satisfies a property ∀✷ϕ (noted P |= ∀✷ϕ) iff for all S i , S o such that S i ⊢ P : S o , S o |= ✷ϕ.

The following property states that safety properties are preserved by synchronous composition: given a synchronous program P satisfying a safety property Φ, any synchronous composition P P ′ satisfies Φ. This result has been stated in [START_REF] Halbwachs | Synchronous observers and the verification of reactive systems[END_REF]. The following result is the formalization of the whole method. It states how, from a program P , a set of controllable inputs I c , and a safety property Φ, a semantically compatible program P ′ can be obtained, satisfying Φ. P and P ′ are not strictly semantically equivalent, as I c are inputs of P but local variables (defined by the controller) of P ′ . We will also define a similarity relation ≤ I between programs as follows (where

(R 1 .R 2 . . . .) \ I = (R 1 \ I).(R 2 \ I). . . ., and R \ I = R ′ iff dom(R ′ ) = dom(R) \ I and ∀x ∈ dom(R ′ ), R ′ (x) = R(x)): P ′ ≤ I P iff ∀S i 1 , S o , S i 1 ⊢ P ′ : S o ⇒ ∃S i , S i \ I = S i 1 ∧ S i ⊢ P : S o

Discussion

We have shown an adaption of an automatic distribution method to allow the separate compilation and transformation of a program. This adaptation has been illustrated on the specific program transformation of discrete controller synthesis. From an initial program, we have shown how to extract the Boolean and the data fragments, how to apply DCS on the Boolean fragment to ensure a safety property, and finally how to recombine by synchronous product the controlled Boolean fragment and the data fragment in such a way that the semantics of the resulting program is ensured to be a simulation refinement of the initial one.

Compared with [START_REF] Delaval | A type system for the automatic distribution of higher-order synchronous dataflow programs[END_REF], this article, besides being an application of this method, shows how it can be adapted towards the distribution of programs on an heterogeneous architecture (i.e., whose computing resources does not all provide the same operations), instead of homogeneous ones, as targetted in this previous work. This adaptation consists, for the declaration of the architecture, to attach specific operations to each declared location. More generally, this example illustrates how a tool allowing co-design of different parts of programs, such as Orccad [START_REF] Borrelly | The Orccad architecture[END_REF], Ptolemy [START_REF] Buck | Ptolemy: A framework for simulating and prototyping heterogenous systems[END_REF], can integrate two approaches, the design by a unified language or paradigm allowing more control of the program semantics, and the separate compilation, program transformation or analysis. From this point of view, this work can be related to the different approaches of unification of different paradigms in one language (modes and dataflow in Mode automata [START_REF] Maraninchi | Mode-automata: About modes and states for reactive systems[END_REF], and its generalization in Lucid Synchrone [START_REF] Colaço | A Conservative Extension of Synchronous Data-flow with State Machines[END_REF]). The purpose of this work is to show how such language integrations does not stand as an obstacle for the further application of heterogeneous compilation paradigms. Such comparable distribution method has been applied for the design of multi-tier systems [START_REF] Neubauer | From sequential programs to multi-tier applications by program transformation[END_REF]: the functions are then annotated with the location where it is executed. We show here how these annotations can be integrated in a language, and how a type system can be used to infer the location of every value or expression.

The prospects of this work lies mainly in considering modular program transformations and analysis. From the point of view of the specific problem addressed here, controller synthesis for hierarchical systems has been studied in [START_REF] Marchand | Supervisory control problems of hierarchical finite state machines[END_REF], and the interaction of this method with modular compilation should be studied. The interest of this method for other mixed models shall also be evaluated.

A Type system

Fig. 1 .

 1 Fig. 1. Automatic distribution for application of a transformation on part of a program.

x ≥ 10

 10 ∧ c x = last(x) + 1 x = last(x) -1 x ≤ 0 ∧ c I D automaton | I -> do x = last x + 1 until (x >= 10) & c then D | D -> do x = last x -1 until (x <= 0) & c then I end

Fig. 3 .

 3 Fig. 3. Mode automata example.

Fig. 4 .Fig. 5 .

 45 Fig. 4. Two fragments obtained from the program of Figure 3.

Fig. 6 .

 6 Fig. 6. Example: delayable task pattern.

Fig. 7 .

 7 Fig. 7. Boolean fragment of Figure 6.

2 Fig. 8 .

 28 Fig. 8. Data fragment of Figure 6.

P

  ::= d 1 ; . . . ;d n ;D d ::= node f (p) = e where D p ::= p, p | x D ::= ǫ | p = e | p = x(e) | D and D | automaton S → h . . . S → h end h ::= do D u u ::= until e then S u | ǫ e ::= i | x | (e, e) | op(e, e) | e fby e

3 s

 3 e) : [t 1 /x 1 , . . . , tn/xn]/ℓ 1 ∪ ℓ 2 ∪ ℓ 3 /T ′ 1 , T 2 , T =⇒ (x 1 , . . . , xn, c 1 , . . . , cn) = f ′ (e ′ , c ′ 1 , . . . , c ′ p ) and D 1 and D 2

Fig. 9 .

 9 Fig. 9. Rules for the projection operation.

Property 5 . 1 (

 51 Semantical equivalence) For all S i , S o , P , H, H ′ , ℓ and T such that S i ⊢ P : S o , H ⊢ P : H ′ /ℓ/T A =⇒ P A and H ⊢ P : H ′ /ℓ/T B =⇒ P B , then S i ⊢ P A P B : S o .

Property 6 . 2 (

 62 Conservation of safety properties)∀P, Φ, P ′ , P |= Φ ⇒ (P P ′ ) |= Φ. Definition 6.3 (Discrete controller synthesis) DCS is a partial function such that, given a program P , a set of controllable inputs I c of P , and a safety property Φ, then if DCS(P, I c , Φ) is defined, then (P DCS(P, I c , Φ)) |= Φ.

Theorem 6 . 4

 64 For all P, I = I u ⊎ I c , Φ, let P b , P d , H, T, ℓ such that H 0 ⊢ P : H/ℓ/T A b =⇒ P b and H 0 ⊢ P : H/ℓ/T A d =⇒ P d , then if C = DCS(P b , I c , Φ) is defined, then let P ′ = (P d P b C), P ′ ≤ Ic P and P ′ |= Φ. Proof. From property 5.1, P b P d is semantically equivalent with P . Then, for any program C whose output domain is I, (P b P d C) ≤ I P . Then, (P b P d DCS(P b , I c , Φ)) ≤ I P . By definition of DCS, (P b DCS(P b , I c , Φ)) |= Φ. Then from property 6.2, for all P , (P P b DCS(P b , I c , Φ)) |= Φ. Then, (P d P b DCS(P b , I c , Φ)) |= Φ. ✷

  ′ /D H ⊢ e : t at s ′ /ℓ ∪ {s ′ }/T, [s H ⊢ e 1 , e 2 : t 1 × t 2 /ℓ 1 ∪ ℓ 2 /T 1 , T 2

							c → s ′ ]	s =⇒ ()/D and cn = e ′
	(Comm-To)	H ⊢ e : t at s/ℓ/T H ⊢ e : t at s ′ /ℓ ∪ {s ′ }/T, [s s ′ =⇒ e ′ /D c → s ′ ] s ′ =⇒ cn/D
	(Pair)		H ⊢ e 1 : t 1 /ℓ 1 /T 1	s =⇒ e ′ 1 /D 1	H ⊢ e 2 : t 2 /ℓ 2 /T 2 s =⇒ e ′ 1 , e ′ 2 /D 1 and D 2 s =⇒ e ′ 2 /D 2
	(Suppr-Expr)	s ∈ ℓ H ⊢ e : t/ℓ/T	s =⇒ ()/ǫ	(Suppr-Def)	s ∈ ℓ H ⊢ D : H ′ /ℓ/T	s =⇒ ǫ
	(Def)	H ⊢ e : t 1 × . . . × tn/ℓ/T H ⊢ (x 1 , . . . , xn) = e : [t 1 /x 1 , . . . , tn/xn]/ℓ/T s =⇒ e ′ /D s =⇒ x = e ′ and D
	(And)

locations(t)/∅ s =⇒ x/ǫ (Comm-From) H ⊢ e : t at s/ℓ/T s =⇒ e

  (Imm) H ⊢ i : b at s/{s}/∅ ⊢ e : t at s ′ /ℓ ∪ {s ′ }/T, [s(Pair) H ⊢ e 1 : t 1 /ℓ 1 /T 1 H ⊢ e 2 : t 2 /ℓ 2 /T 2 H ⊢ e 1 , e 2 : t 1 × t 2 /ℓ 1 ∪ ℓ 2 /T 1 , T 2 (Def) H ⊢ e : t 1 × . . . × t n /ℓ/T H ⊢ (x 1 , . . . , x n ) = e : [t 1 /x 1 , . . . , t n /x n ]/ℓ/T (And) H ⊢ D 1 : H 1 /ℓ 1 /T 1 H ⊢ D 2 : H 2 /ℓ 2 /T 2 H ⊢ D 1 and D 2 : H 1 , H 2 /ℓ 1 ∪ ℓ 2 /T 1 , T 2 : H i /ℓ i /T i ℓ = ℓ 1 ∪ . . . ∪ ℓ n T = T 1 , . . . , T n H ′ = merge(H 1 , . . . , H n ) H ⊢ automaton S 1 → h 1 . . . S n → h n end : H ′ /ℓ/T

	(Inst)	t ≤ (H(x)) H ⊢ x : t/ locations(t)/∅ s ∈ locations(t)
	(Comm) H (Node)	H ⊢ e : t at s/ℓ/T
	H, x

c → s ′ ] i : t i , H 1 ⊢ D : H 1 /ℓ 1 /T 1 H, x i : t i , H 1 ⊢ e : t/ℓ 2 /T 2 H ⊢ node f (x 1 , . . . , x n ) = e with D : [gen H ((t 1 × . . . × t n )ℓ 1 /T 1 , T 2 → t)/f ]/ℓ 1 ∪ ℓ 2 /∅ (App) H ⊢ f : tℓ 1 /T 1 → (t 1 × . . . × t n )/ℓ 2 /T 2 sf ′ /D 1 H ⊢ e : t/ℓ 3 /T 3 se ′ /D 2 T ′ 1 ∼ = T 1 H ⊢ x = f (e) : [t 1 /x 1 , . . . , t n /x n ]/ℓ 1 ∪ ℓ 2 ∪ ℓ 3 /T ′ 1 , T 2 , T 3 (Trans) H ⊢ e : t at A b /ℓ 1 /T 1 A d =⇒ e ′ /D 1 H ⊢ u : ℓ 2 /T 2 H ⊢ until e then S u : ℓ 1 ∪ ℓ 2 /T 1 , T 2 , [A b c → A d ] (Handler) H ⊢ D : H ′ /ℓ 1 /T 1 H ⊢ u : ℓ 2 /T 2 H ⊢ D u : H ′ /ℓ 1 ∪ ℓ 2 /T 1 , T 2

(Automaton)

i ∈ {1, . . . , n}, H ⊢ h i

Acknowledgement

I would like to gratefully thank Alain Girault and Marc Pouzet for their suggestions and comments about this work. Anonymous reviewers also significantly helped in improving of this paper.