Guillaume Fournier
email: guillaume.fournier@supelec.fr

Pierre Matoussowsky
email: pierre.matoussowsky@supelec.fr

Pascal Cotret
email: pascal.cotret@centralesupelec.fr

Hit the KeyJack: stealing data from your daily wireless devices incognito

Internet of Things (IoT) is one of the most fast-growing field in high technologies nowadays. Therefore, lots of electronic devices include wireless connections with several communication protocols (WiFi, ZigBee, Sigfox, LoRa and so on). Nevertheless, designers of such components do not take care of security features most of the time while focusing on communication reliability (speed, throughput and low power consumption). As a consequence, several wireless IoT devices transmit data in plaintext creating lots of security breaches for both eavesdropping and data injection attacks. This work introduces KeyJack, a preliminary proof-of-concept of a solution aiming to eavesdrop wireless devices and hopefully perform injection attacks afterwards. KeyJack operates on widely-used devices: our keyboards! This solution is based on lowcost embedded electronics and gives an attacker or a white hat hacker the possibility to retrieve data from John Doe's computer. This work also shows that this approach could be used to any wireless device using 2.4GHz radio chips like the NRF24L01 from Nordic Semiconductor. KeyJack node KeyJack node KeyJack node KeyJack server (self-hosted)

Introduction

Nowadays, most of the people have IoT devices at home or even at work: for instance, it could be included in a fridge, a set-top box or computers. IoT is a highly-growing field and it will get even bigger in the next decade (a Verizon report [START_REF]Verizon: State of the market: The internet of things 2016[END_REF] foresees that the IoT market will hit the $1 trillion limit by 2019). In the same document, it can be seen that the IoT market targets several applications such as healthcare and home monitoring. Most of these connected devices were designed to perform tasks fast and in a cheap way (in other words, communication links have to be fast and low-power). Unfortunately, without security, each device is a vector of threats: malevolent people could use breaches in wireless protocols to steal or inject data using man-in-the-middle (MITM) attacks.

In this context, this work focuses on wireless keyboards that are widelyspread components. This work presents KeyJack that is a kind of wireless keylogger implemented in a tiny electronic board aiming to retrieve data from a remote computer. Furthermore, this work gives some clues about using it as a malicious injection device.

Section 2 presents some related works of both classic keyloggers and embedded electronics solutions with similar goals. Section 3 presents KeyJack, its requirements and implementation details. Then, Section 4 presents an eavesdropping scenario where Keyjack is used and gives some hints about the feasability of injection attacks using such hardware components. Finally, Section 5 presents some conclusions and perspectives about this work.

Related works

Keyloggers

When an hacker wants to retrieve data from a user keyboard, keyloggers could be used [START_REF] Sagiroglu | Keyloggers[END_REF][START_REF] Subramayam | Keyloggers: The Overlooked Threat to Computer Security[END_REF][START_REF] Holz | Learning More about the Underground Economy: A Case-Study of Keyloggers and Dropzones[END_REF][START_REF] Dorne | La menace keylogger[END_REF]: these components are usually softwares running in the background of the target computer. In more recent works such as Damopoulos et al. [START_REF] Damopoulos | From keyloggers to touchloggers: Take the rough with the smooth[END_REF], keyloggers are also implemented for touchscreen that are widely-spread interfaces on our smartphones and tablets. Such keyloggers aim to keep a copy of each keyboard hit made by the victim. On the other side, several works such as [START_REF] Herley | How to Login from an Internet Cafe Without Worrying about Keyloggers[END_REF][START_REF] Ortolani | Noisykey: Tolerating keyloggers via keystrokes hiding[END_REF] present countermeasures in order to implement systems resilient to such attacks. Therefore, IoT designers could imagine to create embedded systems immune to standard keylogger implementations.

However, most of software keyloggers are not so easy to use:

-Advanced features are rarely included in free versions. As keyloggers may be used for "bad" purposes, developers keep the most intrusive options for paid licenses. -Basic keyloggers are not 100% discrete as they appear in the task manager.

-For some of them, administrator rights may be required by the operating system (for instance, installing a driver). -Furthermore, results take up space on the target computer and may increase its power consumption.

Other interesting works

In the context of pure keyloggers, there are other interesting alternatives in the hardware community:

-KeyGrabber USB made by KeeLog [START_REF] Usb | Hardware keylogger -keygrabber usb[END_REF].

-USB Rubber Ducky, a USB tool by Hak5 [9]. This USB key includes a 60MHz programmable microcontroller and a µSD slot. It behaves like a keyboard: therefore, nearly anything can be performed (from a Rick Roll hack to keyloggers as well).

Both solutions look like USB flash drives: it can be easily hidden on a computer port. Even if some countermeasures exists (for instance, KeyScrambler[14] encrypts of all keyboard hits in Firefox), it is not 100% satisfying as it still needs some physical access to the target. Furthermore, even if such a tool may be hidden in the task manager, it is assumed that its power consumption may be revealed with physical measurements. KeyJack wants to tackle those problems using an alternative breach: nowadays, most keyboards are wireless and may be affected by eavesdropping and MITM attacks. The next subsection presents some works using wireless connection to reveal security breaches.

Embedded electronics solutions

There are several works aiming to steal information from wireless computer devices. The most "industrial" solution is MouseJack from Bastille Networks 3 . MouseJack is an exploit used in several wireless (non-Bluetooth) keyboards that can be used to perform eavesdropping and relay attacks. However, a laptop is required to run MouseJack in contradiction to KeyJack which aims to be a discrete and standalone solution [START_REF] Higgins | Mousejack attack bites non-bluetooth wireless mice (Feb 2016)[END_REF].

Other people tried to make things smaller. Digital Security (@iotcert) implemented related eavesdropping methods for Bluetooth devices running on a single-board computer such as Raspberry Pi [2,3]: Cauquil et al. implemented a Bluetooth sniffer on a RaspberryPi Zero single-board computer that can be used to track people and steal secrets (as it was shown in their Nuit du Hack'16 talk4 ). Samy Kamkar (@samykamkar) developed Keysweeper [START_REF] Kamkar | Keysweeper[END_REF][START_REF] Goodin | Meet keysweeper, the 10usd usb charger that steals ms keyboard strokes[END_REF], a solution based on a small tiny microcontroller similar to Teensy or Arduino Nano. Even if this solution is the most similar to KeyJack, it does not take into account the feasability of data injection (Kamkar only focused on data listening). Furthermore, KeyJack plans to use a GSM chip to perform multiple eavesdropping with target localization in a use case where several KeyJack devices would be implemented.

KeyJack

Threat model

There are several keyboard manufacturers. This work focuses on the two main ones: Microsoft and Logitech (it is assumed that generic/low-cost keyboards may work as well). Microsoft/Logitech keyboards uses a classic Wifi-based protocol working at 2.4GHz (for European versions at least). When this 2.4GHz link is left unencrypted, a classic MITM scheme could be used as shown in Figure 1. For some recent keyboards, the communication between Alice and Bob is encrypted: even if such schemes may be broken using brute force or other advanced techniques, this work assumes that the link is left in plaintext:

-For basic models, security was not implemented in the wireless protocol.

-For future perspectives, KeyJack could be adapted to other plaintext protocols working at different frequencies (5GHz band, for instance).

Requirements

A KeyJack device must have the following requirements:

-No physical access to the target device/computer. It means there will not be any USB connection or malicious software installed. -Tiny implementation: in other words, KeyJack must be a small-sized board, easily transportable and autonomous in terms of energy. -"Tracking-friendly": KeyJack end-users must be able to get eavesdropping results from a remote device (website, smartphone. . . ). -Injection-enabled: this work aims to propose a solution which enable not only eavesdropping but also data injection (from a remote interface as well). -This work focuses on a Microsoft Wireless Keyboard 800 5 . Mainly because its protocol was unecrypted.

-For further implementations, a GSM chip in order to retrieve locations of KeyJack nodes in case we want to install a network of such devices. -And, of course, something that is low-cost and easily reproductible! -(the USB cable is just here for programming purposes)

Software layer

Figure 3 shows an example of a KeyJack network. Each node is the Adafruit platform described in the previous section running a given Arduino code. When each node collects information, it is transmitted to the self-hosted server where an internal website was developed. As it was said in Section 3, this case study is focused on a Microsoft Wireless Keyboard 800. Furthermore, we only used a single KeyJack node as shown in Figure 2. When the user enters the KeyJack server, an interface as shown in Figure 6 appears. Each keyboard is identified by its MAC address and has a dedicated menu:

-Search. In this part, the user can read logs of former measurements.

-Capture. Reading captures by their date.

-Injection. Transmitting keyboard keys.

-Hacking. This last tab allows to launch attack scripts. Normally, the NRF24L01 chip is not able to work as a sniffer: in fact, the target MAC address is needed and it is not possible to scan the frequency spec-trum around 2.4GHz to find one. However, as Samy Kamkar explained in its Keysweeper project, we can send fake information about the MAC address in order to swindle the wireless chip. With previous works of Travis Goodspeed, Samy Kamkar discovered that if we enter an incorrect value regarding the MAC address size (writing the preamble itself), the upset NRF24L01 chip considers all preambles as the target MAC address. However, all data after the MAC address should be the payload. Therfore, we get all traffic packets with the MAC address and everything else up to the CRC. From there, we can proceed to keyboard detection.

Each brand has its own protocol to deal with the USB dongle on the computer. Microsoft does not encrypt data sent by its keyboards (it is only done since 2015 !). The only security measure is a XOR performed on the payload with the MAC address. As we know how to get MAC address, this is not a problem for us. As a consequence, we only have to detect Microsoft protocols and perform a XOR. Samy Kamkar also discovered that all Microsoft keyboards used a MAC address beginning with 0xCD (this is the only byte we need in further measurements). In fact, Microsoft is done in a way that the key value is in the 10 th position. As the MAC address is 5 bytes wide and 4 first bytes are not encrypted, the key value is always XORed with 0xCD.

The last criteria we use to detect Microsoft keyboards is the value of the first unencrypted bytes. As it is shown in Figure 8, the device type is always 0x0A (for keyboards). Then, the packet type indicates the key category (we only focus on keystrokes or idles). Related codes are 0x78 and 0x38. We are finally ready to scan, for all frequencies from 2403MHz to 2480MHz:

-We check if the MAC address of the transmitter begins by 0xCD.

-We test if the paylod begins by 0xA78 or 0xA38.

Conclusion and perspectives

This work presented KeyJack, a low-cost solution for basic eavesdropping of a specific Microsoft wireless keyboard. The proof-of-concept is a standalone device which can be left in any open-space and small enough to be hidden from people sight. Even if this study focuses on a specific keyboard model, there are opportunities with other models/vendors when communications are not encrypted. Furthermore, KeyJack can be easily modified for data injection as the server side is already implemented. As each keyboard is clearly identified, the next perspective is to make a network of KeyJack node and a single server where we could monitor everything from a remote location. Finally, KeyJack may be adapted for other protocol where security matters in the context of Internet of Things.

Fig. 1 .

 1 Fig. 1. MITM scheme with KeyJack as the eavesdropper/injection device

3. 3

 3 Hardware implementationKeyJack components are shown in Figure2:

Fig. 2 .

 2 Fig. 2. Electronic components used in KeyJack

Fig. 3 .

 3 Fig. 3. Example of a KeyJack network with three nodes and a server

Fig. 4 .

 4 Fig. 4. KeyJack server interface

Fig. 5 .

 5 Fig. 5. KeyJack keyboard interface

Fig. 6 .

 6 Fig. 6. KeyJack injection interface

Fig. 7 .

 7 Fig. 7. NRF24L01 packet structure

Fig. 8 .

 8 Fig. 8. Packet structure

https://www.mousejack.com/

http://virtualabs.fr/ndh16/ndh16-mass-pwning-bug.pdf

https://www.microsoft.com/accessories/en-gb/products/keyboards/ wireless-keyboard-800/2vj-00006


Keywords: Synchrone, Asynchrone, GALS, Desynchronisation, Implantation, Machine d'exécution, Reaction à l'absence d'un signal

Conditions nécessaires et suffisantes pour une désynchronisation déterministe

Résumé : Les formalismes réactives synchrones utilisent une notion d'horloge globale pour préciser l'ordonnancement d'opérations concurrentes. Cela mène à une définition nonambigue de l'absence d'un signal, qui peut etre utilisée ensuite pour prendre des décisions au cours de l'exécution.

Quand à une spécification synchrone on donne une implantation asynchrone (potentiellement répartie), l'absence des signaux doit être signalée explicitement, sauf pour les cas où les comportements sont prouvés indépendents et asynchrones (une propriété introduite précédemment sous le nom d'"endochronie"). Dans cet article, nous caracterisons la classe de systèmes dont l'implantation asynchrone sans encodage de l'absence est déterministe.

Introduction

Synchronous reactive formalisms [START_REF] Halbwachs | Synchronous Programming of Reactive Systems[END_REF][START_REF] Benveniste | The synchronous languages 12 years later[END_REF] are modeling and programming languages used in the specification and analysis of safety-critical embedded systems. They comprise (synchronous) concurrency features, and are based on the Mealy machine paradigm: Input signals can occur from the environment, possibly simultaneously, at the pace on a given global clock. Output signals and state changes are then computed before the next clock tick, grouped as one atomic reaction. Because common computation instants are well-defined, so is the notion of signal absence at a given instant. Reaction to absence is allowed, i.e., a change can be caused by the absence of a signal on a new clock tick. Since component inputs may become local signals in a larger concurrent system, absent values may have to be computed and propagated, to implement correctly the synchronous semantics.

When an asynchronous implementation is meant, where possibly distributed components communicate via message passing, the explicit propagatation of all absent values may clog the system to a certain extend. Thus a natural question is: when can one dispose of such "absent signal" communications?

Sufficient conditions, known as (weak) endochrony [START_REF] Benveniste | Compositionality in dataflow synchronous languages: Specification and distributed code generation[END_REF][START_REF] Guernic | Polychrony for system design[END_REF][START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF][START_REF] Potop-Butucaru | Correct-by-construction asynchronous implementation of modular synchronous specifications[END_REF], have been introduced in the past to figure when the absent values can be replaced in the implementation by actual absence of messages without affecting its correctness and determinism. Weak endochrony determines that compound reactions that are apparently synchronous can be split into independent smaller reactions that are asynchronously feasible in a confluent way (one after the other instead of simultaneously), so that the first one does not discard the second. This is also linked to the Kahn principles for networks [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF], where only internal choice is allowed to ensure that overall lack of confluence cannot be caused by input signal speed variations.

In this paper, we rephrase these issues to better show their mutual relations, we strengthen the theory by asserting necessary and sufficient conditions, and we discuss the structure of the execution machines needed to give a globally asynchronous implementation to a synchronous specification.

Outline. Section 2 explains what we understand by synchronous specification, asynchronous implementation, and signal absence. Section 3 covers the representation of signal absence in various languages. Section 4 is on reaction to signal absence. It gives its formal definition, implementation details, and examples. Section 5 takes into account concurrency and gives our main result, We give examples in Section 6 and conclude in Section 7.

Basic notions

Asynchronous components

Our goal is to facilitate the construction of globally asynchronous systems from synchronous specifications. By globally asynchronous we understand both (1) fully asynchronous systems and components and (2) globally asynchronous, locally synchronous (GALS) systems where each component consists of a synchronous core driven by a wrapper in the globally asynchronous environment.

More specifically, the goal is to allow the construction of asynchronous components that fit inside a model of computation close to that of the Kahn Process Networks (KPN) [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF]. Such components communicate through message passing along asynchronous lossless communication lines (FIFO channels). Incoming messages remain on the FIFOs until they are read. No other communication or synchronization mechanism exists. No logical or physical time can be used to make decisions and trigger computations (only the arrival of messages, and their values).

To simplify the presentation of this paper, we require that the behavior of an asynchronous component is monotonous and deterministic as an I/O stream function, in the sense of Kahn [START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF]. 1 We also require that the asynchronous component is confluent: from a given state and for given inputs, the implementation ends up in the same internal state.

The components must remain deterministic when given arbitrary inputs. This is different from approaches based on don't cares, which assume that the environment never produces incorrect input sequences, and provide no means of rejecting them. By comparison, in the endochrony variant of LeGuernic, Talpin, and Le Lann [START_REF] Guernic | Polychrony for system design[END_REF], the system must only be deterministic and produce correct output for "correct" sets of inputs, which leads to composition problems and more complex analysis techniques.

Synchronous specifications

The various synchronous formalisms are used to develop specifications that can be interpreted as incomplete synchronous Mealy machines. This is the model we use throughout this paper to represent our synchronous specifications. A specification is therefore any finite automaton whose transitions are labeled with reactions. An execution (trace) of the specification is a sequence of reactions indexed by the global clock.

A reaction is a valuation of the input and output signals of the specification. All signals are typed. We denote with D S the domain of a signal S. Not all signals need to have a value in a reaction, to model cases where only parts of the specification compute. We will say that a signal is present in a reaction when it has a value in D S . Otherwise, we say that it is absent. Absence is simply represented with a new value ⊥, which is appended to all domains D ⊥ S = D S ∪ {⊥}. With this convention, a reaction is a valuation of all the signals S of the specification in their extended domains D ⊥ S . We say that two reactions r 1 and r 2 are non-contradictory, denoted r 1 r 2 , when there exists no signal S that is present, but different in the two reactions ⊥ = r 1 (S) = r 2 (S) = ⊥. The support of a reaction r, denoted supp(r), is the set of present signals. Given a set of signals X, we denote with V X the set of all reactions over X.

To represent reactions, we use a set-like notation and omit signals with value ⊥. For instance, the reaction associating 1 to A, to B, and ⊥ to C is represented with < A = 1, B = >. The delimiters can be dropped if there is no confusion. On non-contradictory reactions we define the union (∪) and difference (\) operators, with their natural meanings from set theory. For instance,

< A = 1, B = > ∪ < A = 1, C = 7 >=< A = 1, B = , C = 7 >.
When representing a reaction r, we shall usually separate the valuations of the input and output signals r = i/o, where i is the restriction of r on input signals, and o is the restriction on output signals. All the operators defined above ( , ∪, \, supp()) can be applied on components. With these conventions, the stuttering reaction assigning ⊥ to all input and output signals is denoted /.

Definition 1 (incomplete synchronous Mealy machine) A synchronous automaton is a tuple Σ = (I, O, S, T ), where I and O are the non-void, finite, and disjoint sets of input and output signals, S is the set of states, and T F : S × V I • / / S × V O is the function representing the transitions. The function is partial to represent the fact that the system may not accept any input.

We will write s i/o / / s instead of T (s, i) = (s , o) to represent system transitions. Note that the functional definition of the transitions implies determinism (at most one transition for given state and input), a property we require for all our specifications throught this paper.

A Mealy machine can stutter in state s if the stuttering transition s / / / s is defined.

We say that a Mealy machine has no input-less transition if the only transitions s i/o / / s with supp(i) = ∅ are stuttering transitions. In other words, no state change can be realized and no output can be produced without new inputs. To facilitate the definitions and presentation of this paper, we require all synchronous automata to have no input-less transition (but similar results exist for deterministic systems with input-less transitions).

The implementation problem

The main issue in specifying asynchronous components using synchronous specifications is the treatment of signal absence. In the synchronous model, the absence of a signal in a given reaction can be sensed and tested in order to make decisions. It is a special absent value, denoted ⊥. In the considered asynchronous implementation model, the absence of a message on a channel cannot be sensed or tested. When transforming the synchronous specification into a globally asynchronous implementation, the sequences of present and absent values on each signal are mapped into sequences of messages sent or received on the associated communication channels. To simplify the problem, we assume one asynchronous FIFO is associated with each signal of the synchronous model.

We have to define the encoding of signal values with messages on channels. When a signal S has value v = ⊥ during a reaction, the most natural encoding associates one message carrying value v on the corresponding channel. The message is sent or received, depending on whether S is an output or an input signal. We shall assume this encoding throughout the paper.

Things are more complicated for absent (⊥) values. The most natural solution is to represent them with actual message absence (i.e. no message at all). Unfortunately, forgetting all absence information does not allow the construction of deterministic globally asynchronous implementations for general synchronous specifications. Consider, for instance, the Esterel program of Fig. 1. The program awaits for the arrival of at least one of its two input signals. Assume that A arrives in the start state. Then, we need to know whether C is present or absent, to decide which of B or D is emitted. We will say that the program reacts to signal absence, because the presence or absence of C must be tested. An asynchronous implementation of PREEMPT needs absence information in order to deterministically decide which transition to trigger in state start.

To generate deterministic asynchronous implementations for such synchronous programs, messages must be added to represent the necessary absence information. This can be done either by transmitting absent (⊥) values through messages, or by adding other synchronization messages on new or already existent communication channels.

In this paper, our objective is to characterize the class of synchronous specifications that can be transformed into deterministic asynchronous implementations without adding such new messages to encode absence. We then advocate for a 2-step implementation process, where all absence encoding problems are dealt with inside the synchronous model, thus facilitating the analysis of large specifications:

Step 1: Signal absence encoding. Transform the synchronous specification into one where reaction to signal absence is not needed. This is done by either (1) deciding which ⊥ values are relevant and must be transmitted, and represent them with a new value ⊥ * , or (2) adding new signals and messages to the specification.

Step 2: Implementation synthesis. Give a deterministic asynchronous implementation to the transformed synchronous specification. This implementation follows the natural encoding defined above: no message for the remaining absent ⊥ values, and one message for each other signal value.

Our characterization has important practical consequences, establishing the limits of the two-phase approach and allowing the choice of the best absence encoding.

Related work

Our work is closely related to work on various variants of endochrony, and we show that the various formulations of (weak) endochrony aim at expressing a more fundamental property of a concurrent synchronous specification: the fact that it does not react to signal absence. Moreover, our two-step implementation process reflects the process of the Polychrony [START_REF] Guernic | Polychrony for system design[END_REF] environment developed around the Signal language.

Our work generalizes previous work on weakly endochronous systems by Potop, Caillaud, and Benveniste [START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF][START_REF] Potop-Butucaru | Correct-by-construction asynchronous implementation of modular synchronous specifications[END_REF]. The main difference is that we do not assume here all the goals of the approach based on weak endochrony and weak isochrony. More precisely, we do not address the preservation of the synchronous composition semantics throughout desynchronization. In particular, the decomposition into primitive reactions (extensively used in the proofs of [START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF]) will not be ensured in our approach, so that the characterization is closer to that of microstep weak endochrony [START_REF] Potop-Butucaru | Correct-by-construction asynchronous implementation of modular synchronous specifications[END_REF].

Along the same lines, our work extends or is closely related to work on the various variants of endochrony. Compared with the endochronous systems of Benveniste, Caillaud, and Le Guernic [START_REF] Benveniste | Compositionality in dataflow synchronous languages: Specification and distributed code generation[END_REF], which is used in the compilation of the Signal language [START_REF] Amagbégnon | Implementation of the data-flow synchronous language signal[END_REF], our work generalizes by allowing concurrent reactions and a more relaxed input reading policy (more informations in Section 4.1). We already explained, in Section 2.1, that LeGuernic, Talpin, and Le Lann [START_REF] Guernic | Polychrony for system design[END_REF] take a don't care-based approach, different from ours.

The latency-insensitive systems of Carloni, McMillan, and Sangiovanni-Vincentelli, the Lustre language [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF], and the AAA/SynDEx methodology [START_REF] Grandpierre | From algorithm and architecture specification to automatic generation of distributed real-time executives: a seamless flow of graphs transformations[END_REF] take a very simple solution to the absence encoding problem, by prohibiting the absence of interface signals. This means that the programmer must perform the absence encoding step, and that all concurrency is lost in the system (the approach is not very efficient). The generalized latency-insensitive systems of Singh and Theobald [START_REF] Singh | Generalized latency-insensitive systems for single-clock and multi-clock architectures[END_REF] try to relax these constraints.

Our results do not cover the distributed implementation of reactive systems, as do Caspi, Girault, and Pilaud [START_REF] Caspi | Distributing reactive systems[END_REF], nor have the same global approach. We only deal with the construction of one deterministic asynchronous component from one synchronous component.

From another perspective, the synchronous systems, as defined in distributed computing [START_REF] Attiya | Distributed Computing[END_REF] correspond in our case to synchronous specifications without reaction to signal absence.

Our work has different goals from Boussinot and de Simone's work on instantaneous reaction to signal absence [START_REF] Boussinot | The sl synchronous language[END_REF]. There, the issue is that of determining signal absence while avoiding causality problems.

Programs written in the three main synchronous languages are easily represented with Mealy machines.

For the Signal language, we consider its trace semantics, as defined in [START_REF] Amagbégnon | Implementation of the data-flow synchronous language signal[END_REF]. A reaction of the program is a partial assignment of the signals that satisfies the constraints represented by the statements of the program. When a reaction does not assign a signal, we say that the signal is absent. This absence representation is naturally mapped to our absence encoding which uses explicit ⊥ values. We shall denote with the unique present value of the signals of type event. A Signal program has no explicit global clock, so that all Signal programs are stuttering-invariant (the stuttering transition is defined in all states), but all Signal programs are not deterministic. For the scope of this paper, we shall only consider deterministic Signal programs. Stuttering-invariance and determinism imply that the programs have no inputless transition.

Lustre and the specification formalism of the SynDEx software can be seen as sub-sets of Signal, the main differences being that the global clock is specified, and that no interface signal is ever absent (by consequence, no input-less transition exists). Thus, we can use the same encoding as for Signal.

In Esterel, every signal has a status of present (true) or absent (false). 2 Valued signals also carry a value, that should be read only during reactions where the signal is present (status=true). The mapping from the Esterel absence encoding to ours is again natural: a signal which is present is represented by its value (if the signal is valued), or by (if the signal is not valued). A signal that is absent has value ⊥.

The Esterel language defines a global clock. Time flow, and therefore the reactions where a signal can be absent, is determined by the successive occurrences of the implicit TICK signal. In particular, no other signal can be present if TICK is absent: This program obviously has input-less transitions, because it can produce O without reading a single input (TICK is not an input signal). However, meaningful classes of Esterel programs do not have input-less transitions. Among them, all those containing no pause or suspend statements and no reference to TICK, and where all preemption triggers are reduced to one signal (without not operator).

To represent such behaviors with deterministic Signal programs (which have no inputless transition), the TICK signal must be explicitly represented in the input interface of the program, for instance: Line 3 specifies that the state is read and updated in all reactions (i.e. whenever TICK is present).

Representing the behavior of TIMEFLOW in Lustre leads to different problems. Like in Esterel, Lustre programs define a notion of global clock. However, the use of absence is constrained. More precisely, all the inputs and outputs of a Lustre program (node) need to be present at all instants where the node is executed. This means that the previous example cannot be encoded while sticking to the absence encoding defined above. The only solution is to explicitly encode absence using "present" signal values. One typical solution is to use a Boolean signal with the same encoding as the one used for signal statuses in the compilation of Esterel (present=true/absent=false): node TIMEFLOW() returns (O:boolean); var state : integer ; let state = (-1) -> (pre(state)+1) mod 2 ; O = state==1 ; tel Not having a dedicated signal absence representation for interface signals means that a Lustre program uses one message per absent value. The specification formalism of the SynDEx software has roughly the same constraints as Lustre. The Scade formalism -the graphical counterpart of Lustre -relaxes this rule, but still does not allow the direct representation of the previous example.

Reaction to signal absence

In this section, we formally define reaction to signal absence and we explain how synchronous specifications without reaction to signal absence can be given deterministic asynchronous implementations.

We say that a system reacts to signal absence when the choice between two transitions in a state is based on the choice over the present/absent value of a signal. Formally, it is simpler to define the dual property: Definition 2 (No reaction to signal absence (NRSA)) Let Σ = (I, O, S, T ) be a synchronous Mealy machine. We say that Σ does not react to signal absence if for every state s and every two non-stuttering transitions starting in s s

r k =i k /o k / / s k , r k = /, k = 1, 2,
we have:

r 1 = r 2 ⇒ ∃S ∈ I : ⊥ = i 1 (S) = i 2 (S) = ⊥
In other words, we can decide which transition to do by testing the value (and not the presence/absence) of an input. This choice can be implemented as a deterministic choice in our asynchronous framework.

Asynchronous implementation issues

The NRSA criterion preserves the spirit of endochrony, as defined in [START_REF] Benveniste | Compositionality in dataflow synchronous languages: Specification and distributed code generation[END_REF], but strictly generalizes it. The following example shows the difference between NRSA and endochrony: Choosing between the three non-stuttering transitions can be done without signal absence information, so deterministic implementation is possible in an asynchronous environment. However, the program is not endochronous in the sense of [START_REF] Benveniste | Compositionality in dataflow synchronous languages: Specification and distributed code generation[END_REF]. In an endochronous program, the signals can be organized in a decision tree (called clock tree). Input reading starts with the signals at the top level of the tree, which are present in each reaction. Depending on their values, some of their direct children are read, and the process continues recursively from each present signal to its present children signals. A signal is present in the current reaction iff its clock tree node has been traversed. Blocking reads can be used to produce a fully deterministic top-down input reading process. This form of endochrony stands at the basis of the Signal compiler [START_REF] Amagbégnon | Implementation of the data-flow synchronous language signal[END_REF].

In our example, the signals cannot be organized in a tree determining which signals are present in an incremental fashion. Blocking reads can no longer be used. Instead, each input FIFO must deliver messages as they arrive. Once an input message m arrives on the FIFO head f S corresponding to signal S ∈ I, f S will accept no more messages until a reaction A fireable reaction i/o can be triggered as soon as its input values are available as messages on the input FIFO heads corresponding to the present signals of i. Once this condition is met, the actual transition can be triggered in a variety of ways, without affecting the functionality and determinism of the implementation: by some external clock (periodic or not), when enough input is available to trigger a non-stuttering reaction, etc.

Incremental ASAP input reading

One possible asynchronous execution of the previous example is given in Fig. Note that, in our example, we always perform a reaction as soon as its inputs are available at clock activation time (never delaying execution). This choice is natural, as it minimizes the number of clock cycles needed to complete a computation. We shall say that reactions are executed as soon as possible (ASAP).

Also note that the NRSA property allows an incremental reading of the inputs needed to trigger a reaction r. As soon as the system enters a state where r = i/o is fireable, we can start a process W ait i that waits for the values of i to arrive on the FIFOs. Once the inputs are assembled, r can be executed ASAP. The input reading process W ait i is killed if some input FIFO f S with S ∈ supp(i) brings a message m with i(S) = v(m).

In Fig. 2, for instance, the input reading process W ait B=f alse,C=f alse starts when execution starts. Then, it assembles C = f alse, but B = true arrives and W ait B=f alse,C=f alse is be killed. However, the reaction B = f alse, C = f alse/O2 = is again fireable after the execution of the first reaction. Therefore, W ait B=f alse,C=f alse is restarted. It assembles C = f alse, which is still unconsumed. Finally, B = f alse arrives and the W ait B=f alse,C=f alse completes its execution by triggering the associated reaction at the third activation of the clock (as soon as possible). When ASAP execution is combined with this incremental input reading mechanism, we shall say that we have an Incremental ASAP input reading (and reaction triggering) policy.

Incremental ASAP input reading is more complex than endochronous input reading but allows the deterministic asynchronous implementation of more synchronous systems. The basic Incremental ASAP technique described here can be optimized, e.g. by using blocking reads (like in the endochronous approach) every time this is possible. But we shall not cover optimization aspects here.

Extension to concurrent systems

The NRSA property ensures that for given input messages, the program can choose deterministically the non-stuttering reaction to trigger. However, this strong form of determinism is not always necessary to ensure the I/O determinism of an asynchronous implementation. Consider the following Signal program:

process WE1 = (? event A, B ; ! event C, D ;) (| C := A | D := B |)
The corresponding automaton in our model is the following: More generally, the weak endochrony property introduced by Potop, Caillaud, and Benveniste [START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF] ensures that an Incremental ASAP input reading policy produces deterministic asynchronous implementations.

While weak endochrony is a sufficient condition, we determine here the exact class of synchronous programs (automata) that produce deterministic asynchronous implementations when an Incremental ASAP policy is used.

Concurrency and Incremental ASAP

The first step in this direction is to determine that the Incremental ASAP policy is compatible with concurrent systems such as WE1. In systems with the NRSA property, at most one non-stuttering reaction r is executed during a clock activation because at most one input gathering process can complete between two clock activations. This is no longer the case when concurrent reactions are accepted. For instance, assume that both inputs A and B arrive before the first clock activation of example WE1. Three input gathering processes are started (one for each non-stuttering fireable reaction), and all three are completed before the first clock activation. In the end, to avoid ambiguity, only one should be executed. In our case, the combined reaction A = , B = /C = , D = .

To obtain this behavior, we need to add two new rules allowing the Incremental ASAP policy to handle non-contradictory concurrent reactions. Assume that two input reading processes are started for reactions i 1 /o 1 and i 2 /o 2 , with i 1 i 2 and supp(i 1 ) ∩ supp(i 2 ) = ∅. When a clock activation arrives, the following supplementary rules apply: SR1 (competition for resources) If W ait i1 is completed and W ait i2 is not, then i 1 /o 1 is executed and W ait i2 is killed.

SR2 (the bigger transition wins) If both W ait i1 and W ait i2 are completed and i 1 ⊂ i 2 , then i 2 /o 2 is executed and W ait i1 is killed.

We shall call this extended input reading policy Concurrent Incremental ASAP.

Note that the correctness of an Incremental ASAP policy relies on two fundamental properties:

FP1 The scheduling rules leave at most one transition executable at each activation of the clock.

FP2 A reaction i/o is still fireable when W ait i is completed. This means that the transitions realized from the moment W ait i is started and until it completes (without being killed) leave the reaction fireable.

These properties are implied by the NRSA property, and need to be preserved by its extension to concurrent systems.

Concurrent NRSA

Consider a synchronous specification Σ = (I, O, S, T ) with the property that its implementation using a Concurrent Incremental ASAP input reading policy produces a monotonous and deterministic3 asynchronous automaton.

Assume that Σ is in state s and that s From the confluence property we demanded for the asynchronous implementations in Section 2.1, we can deduce that there exist the reactions i k j /o k j with j ∈ {1, 2} and 0 ≤ k ≤ m j such that: O O (cnrsa)

r k =i k /o k / / s k , k = 1, 2 such that
s 1 i 1 1 /o
where the following equalities hold (their terms being defined):

i 2 \ i 1 = m1 j=1 i j 1 i 1 \ i 2 = m2 j=1 i j 2 (1)
o = o 1 ∪ m1 j=1 o j 1 = o 2 ∪ m2 j=1 o j 2 (2)
This is the property defining concurrent systems without reaction to signal absence.

Definition 3 (Concurrent NRSA) Given a synchronous specification Σ = (I, O, S, T ), we shall say that it satisfies the no reaction to signal absence property for concurrent systems (Concurrent NRSA) if for every two transitions s The following theorem is our main result. It proves that the Concurrent NRSA property indeed characterizes synchronous specifications that give deterministic asynchronous implementations when a Concurrent Incremental ASAP input reading policy is used.

i k /o k / / s k , k = 1, 2 such that i 1 i 2 ,
Theorem 1 (Characterization) Let Σ = (I, O, S, T ) be a synchronous specification. Then, the Concurrent Incremental ASAP asynchronous implementation of Σ is monotonous and deterministic if and only if Σ has the Concurrent NRSA property.

Proof sketch: ⇒. Already done, in a constructive fashion, in this section. ⇐. Consider a finite set of inputs (a sequence of non-absent values for each input signal), consider two arrival orders of these incoming inputs with respect to the clock triggering instants, and consider the associated maximal Concurrent Incremental ASAP executions. Given that every transition (stuttering ones excepted) consumes at least one input, the two executions are finite.

The next step is to prove that the two executions read the same inputs. By assuming that one execution reads one more input than another on some input channel, and by using equation (cnrsa), we contradict the maximality hypothesis on the executions. This reasonment also proves that the destination state is the same.

The last step is to prove that the same outputs are produced on both execution paths. Similarly, by using the Concurrent NRSA property, the rewriting is confluent. End proof.

Relation with weak endochrony

Consider a synchronous system Σ satisfying the Concurrent NRSA property and two non-

contradictory transitions s i k /o k / / s k , k = 1, 2.
Assume the inputs of i 1 arrive before the first activation of the clock, and that the inputs of i 2 \ i 1 arrive before the second activation of the clock. From the determinism of the asynchronous implementation, we know that all the inputs of i will be read, and all the outputs of o produced. However, we have no guarantee on the number of clock activations needed to consume the inputs of i 2 \ i 1 , and to produce the outputs of o \ o 1 .

If we restrict our class of specifications to those where the input arrival order does not lead to an explosion in the number of clock cycles needed for consuming them, we can further require that once a reaction i/o is fireable in a state, and as soon as the inputs of i arrive through the input FIFOs, all the inputs of i are consumed and all the outputs of o are produced. In this class of specifications, those that have deterministic asynchronous implementations are characterized by property (cnrsa), with the restriction that m 1 , m 2 ≤ 1 (the diagram (cnrsa) closes in at most one step). This property is similar to the microstep variant of weak endochrony defined by Potop and Caillaud [START_REF] Potop-Butucaru | Correct-by-construction asynchronous implementation of modular synchronous specifications[END_REF].

Similarly, if we require that rule SR1 is never applied, which greatly simplifies the structure of the asynchronous implementation, we are lead to a decomposition of all executions into atomic reactions. The result is macrostep weak endochrony [START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF]. The way signals are lost is more obvious here. The lines 5 and 6 show how inputs are read at each reaction. At the same time, the input data is only used when stateA, respectively stateB are true.

It is important to note that all useful Esterel programs lose messages. More precisely, the only programs that do not lose inputs are those that read all their inputs at all instants. This is due to the fact that Esterel programs do not constrain their environment, or do it in elementary ways, whereas a Signal program specifies both the system and its environment. To allow the use of Esterel for the specification of systems that do not react to signal absence, we need to constrain the environment, using a constraint language such as Signal, so that signals do not arrive when they are not awaited.

The previous Signal program, which can lose signals, can be "fixed" by requiring inputs to come only in instants where they are awaited, for instance by changing line 3 as follows.

Signal merging and splitting

A special form of signal loss occurs when two or more statements simultaneously emit or read a signal, while reading can also be done separately:

The simplest case is that of emission, illustrated by the following Esterel program:

Conclusion

We have introduced a simple formal definition of reaction to signal absence. We have defined an execution machine that allows the deterministic execution of synchronous programs with no reaction to signal absence (NRSA) in an asynchronous environment. We have determined a formal criterion characterizing the class of concurrent programs that are deterministic when run using this execution machine. The Concurrent NRSA criterion generalizes various notions of (weak) endochrony and establishes theoretical and practical limits for deterministic desynchronization. Intuitive examples have been used to illustrate the various concepts.

Future work will concentrate on practical application of these results to the optimization of the communication mechanisms of GALS implementations generated by systems such as SynDEx. We will also develop analysis and synthesis techniques for the deterministic asynchronous implementation of programs written in common synchronous languages.

Figure 1 :

 1 Figure 1: The PREEMPT example (top), and its Mealy machine representation (bottom)

  If A arrives alone, then the program terminates by emitting B. If C arrives alone or if A and C arrive at the same time, then then the program terminates by emitting D.

  process TIMEFLOW = (? event TICK ; ! event O ;) (| State ^= TICK | State := preState $init (-1) | preState := (State+1) modulo 2 | O := when State=1 |) where integer State,preState ; end ;

  A, B, C ; ! event O1, O2, O3;) (| O1 ^= when A=true ^= when B=true | O2 ^= when B=false ^= when C=false | O3 ^= when A=false ^= when C=true |)The corresponding automaton in our model is the following:

Figure 2 :

 2 Figure 2: Incremental ASAP asynchronous execution of NOABSENCE1

2 .

 2 It corresponds to a GALS implementation where reactions are triggered by an external clock. The input FIFO associated with signal C is the first to deliver a value (false). Then, new values arrive for B and C. When a reaction is triggered by the external clock, the only non-stuttering fireable reaction is A = true, B = true/O1 = . This reaction is performed, O1 is emitted, the FIFOs of A and B unblocked (new messages can be accepted), but the FIFO of C remains blocked by the unconsumed message on it. After a new value arrives for A, a new reaction is triggered by the external clock. Given the available inputs, the only fireable transition is ⊥, which changes nothing. The third reaction is B = f alse, C = f alse/O2 = .

  The automaton does not satisfy the NRSA property, because absence is needed to choose between A = /C = , B = /D = , and A = , B = /C = , D = . However, the program can be asynchronously implemented, without added signalling, if we use an Incremental ASAP input reading and reaction triggering policy. Indeed, as soon as A is received, the reaction A = /C = can be executed, whether B has been received or not.Intuitively, reactions A = /C = and B = /D = are independent. The interleaving between incoming messages on the A and B channels, and the associated interleaving of reactions do not change the asynchronous I/O behavior of WE1. The same is true for the corresponding Esterel program: module WE1: input A,B ; output C,D ; [ every immediate A do emit C end || every immediate B do emit D end ] end module

  there exist s ∈ S and o valuation of the output signals such that o 1 ∪ o 2 ⊆ o, as well as the reactions i k j /o k j with j ∈ {1, 2} and 0 ≤ k ≤ m j satisfying equations (cnrsa),(1), and (2).

| 12 |

 12 stateB := stateBnxt $ init true 10 | stateBnxt := stateB and not BE 11 | C := when stateA and AE

(

  | A ^< TICK | B ^< TICK | A ^< when stateA=true | B ^< when stateB=true One could imagine combining Esterel programs with Signal environment constraints, to obtain the same effect.

  module LOSS2 : input A, B ; output C ; [ await immediate A ; emit C || await immediate B ; emit C ] end module Depending on the arrival of A and B, the asynchronous implementation of the program can produce one or two messages on C. The following example can read two messages for signal E (in two different reactions), or just one (when A, B, and E arrive simultaneously), or none (when no A, nor B arrive): module LOSS3 : input A, B, E ; output C, D ; [ await immediate [A and E] ; emit C || await immediate [B and E] ; emit D ] end module

  r 1 and r 2 are not stuttering transitions and i 1 i 2 . Assume that all the inputs of i 1 ∪ i 2 arrive through messages before a new activation of the clock. Then, W ait i1 and W ait i2 are both completed, but to comply with property FP1 only one reaction must be executed. Rule SR1 cannot be used to make this choice, meaning that we have to use rule SR2. This means that the reaction i/o that is executed must satisfy i 1 ⊆ i and i 2 ⊆ i. At the same time, given the available input, we also need i ⊆ i 1 ∪ i 2 . Therefore, i = i 1 ∪ i 2 . Also, from the I/O monotony of the asynchronous implementation, and from the fact that Σ has no input-less transitions, we have o 1 ⊆ o and o 2 ⊆ o, and therefore o 1 ∪ o 2 ⊆ o.

1 1

 1 / / . . .

	i1/o1	? ?	i	m 1 1 /o	m 1 1
	s i2/o2 ? ? ? ? ? ? ? ? s 2	(i1∪i2)/o i 1 2 /o 1 2 / / . . .	/ / s i m 2 m 2 2 /o 2

As explained in[START_REF] Potop-Butucaru | Concurrency in synchronous systems[END_REF], monotony can be relaxed into predictability, which allows for non-deterministic internal choices of the component as long as they are published through the outputs, allowing the environment to change its behavior accordingly. But we will not cover this aspect here.

We consider here only correct programs, and ignore all causality issues.

In the sense of Kahn[START_REF] Kahn | The semantics of a simple language for parallel programming[END_REF].

All Lustre programs are endochronous in the sense of Benveniste [START_REF] Benveniste | Compositionality in dataflow synchronous languages: Specification and distributed code generation[END_REF], and therefore satisfy property NRSA.

But it is more interesting to explain which common properties of a synchronous program mean that it does not satisfy the NRSA or Concurrent NRSA properties. We give here intuitive examples where signal absence information necessary in the deterministic asynchronous implementation of a synchronous system. We explained in section Section 2.3 that the program does not have the NRSA property. If we use no message to encode signal absence, the resulting asynchronous implementation is non-deterministic: For given input (one message on channel A, and one message on channel B) 2 different outputs can be obtained.

The Signal language counterpart makes reaction to signal absence even more obvious, under the form of "not CE", used in the lines 8 and 11.

Signal loss

Other properties that introduce encoding problems in the asynchronous implementation of synchronous specifications can be traced back to reaction to signal absence.

First of all, programs written in Esterel and Signal can lose incoming signals. By losing signals we mean that signal valuations can be left unread (and thus discarded) without influencing the behavior of the system in any way. This is generally not acceptable when we want to achieve determinism in the chosen asynchronous framework, because we don't know the number of messages to read. We start with a simple Esterel example: