Abstract
Industrial Control Systems (ICS) are sensible targets for high profile attackers and advanced persistent threats, which are known to exploit USB thumb drives as an effective spreading vector. In ICSes, thumb drives are widely used to transfer files among disconnected systems and represent a serious security risks, since, they may be promiscuously used in both critical and regular systems. The threats come both from malware hidden in files stored in the thumb drives and from BadUSB attacks. BadUSB leverages the modification of firmware of USB devices in order to mimic the behaviour of a keyboard and send malicious commands to the host.
We present a solution that allows a promiscuous use of USB thumbs drives while protecting critical machines from malware, that spreads by regular file infection or by firmware infection. The main component of the architecture we propose is an hardware, called USBCaptchaIn, intended to be in the middle between critical machines and connected USB devices. We do not require users to change the way they use thumb drives. To avoid human-errors, we do not require users to take any decision. The proposed approach is highly compatible with already deployed products of a ICS environment and proactively blocks malware before they reach their targets. We describe our solution, provide a thorough analysis of the security of our approach in the ICS context, and report the informal feedback of some experts regarding our first prototypes.
Keywords
Introduction
Cyber-attacks to critical infrastructures constitute a serious risk for society [19]. Specifically crafted malware can be used by attackers to alter an industrial process or gather industrial secrets, and, in the end, gain some market or political advantage. Due to the inherent criticality of ICSes, best practices [43] suggest to isolate the most critical parts of the system from other IT components, either physically or by means of firewalls. To overcome the limitation of a poorly connected environment, file transfers are usually performed by means of USB thumb drives and other Removable Storage Devices (RSDes). The use of RSDes turned out to be an important vector of malware spread [36] making isolation efforts to protect ICSes from the rest of the IT systems largely ineffective. Further, the recent class of attacks called BadUSB [31] disclosed new threats that involve USB devices. These attacks are based on a modification of the device firmware, that forces the infected device, typically a thumb drive, to behave as a different kind of device, for example as a keyboard. In this way, a malicious firmware can inject commands that end up in a malware infecting the host. These malicious commands could download a malware from the Internet, but can also create it on-the-fly, for example, by “typing” the content of a malicious script and running it.
Regular antiviruses are largely ineffective against innovative malware, i.e. malware that exploit zero-day vulnerabilities, and, especially against BadUSB attacks since they exploit basic capabilities (e.g., typing operating system commands) that the user is normally allowed to use.
In our approach, machines are either critical (SCADA, embedded devices, etc.) or regular (personal notebooks, company PC, etc.). We consider regular machines and RSDes as possible sources and vectors of attacks against critical machines.
In this paper, we propose a solution that enables promiscuous use of RSDes in critical infrastructures, while preventing the spread of both conventional and firmware-based malware into the critical machines.
About the promiscuous use of a RSD, consider the file copy scenario that is depicted in Fig. 1: (1) a critical machine (e.g. a development workstation) writes some data into the RSD, e.g. a software update to be transferred into a critical machine, (2) the RSD is plugged into a, possibly compromised, regular machine, which can infect the software update, add other malicious files in the RSD, or tamper with the firmware of the RSD, and (3) the RSD is plugged into the critical machine (e.g. a SCADA server) that is the destination of the file transfer and also the target of the attack.
A promiscuous use of a RSD.
Our goals are to allow this kind of use while preventing potentially malicious data or code originated from regular machines to spread into critical ones as well as prevent the damage of critical machines by malicious firmware. To achieve the first goal, we rely on cryptographic integrity protection along with the use of authenticated data structures for efficiency. Our approach does not rely on malware signatures and is a strong obstacle to the spread of zero-day attacks, even if RSDes are used promiscuously in critical and regular machines. To achieve the second goal, we rely on an hardware-based “captcha”. The basic idea is that the authenticity of a real Human Interface Device (HID) can be easily checked by asking the user to use it.
We also consider non-malicious data flows from regular machines to critical machines that are occasionally needed, for example, for maintenance purposes. This need was exploited in notable cases (see, for example, [9]). We introduce a complete mediation point, called gatekeeper, where data and/or software are forced to undergo a verification process before reaching any critical machine. The whole architecture is independent from the actual verification whose accuracy depends on the security level to be achieved and may involve, for example, sandboxing or human based analysis. Additionally, the gatekeeper provides a single logging point of external data/software reaching critical machines and collects information that might be fundamental in case of post-incident analysis.
Our hardware-based solution does not require any change to host systems and, hence, it is easily deployable in real ICS environments. Our proposal cannot detect attacks in which a real HID (e.g., a keyboard or a mouse) has a malicious firmware installed and it is promiscuously used in critical and regular machines. However, the promiscuous use of real HIDes can be easily blocked by other means without affecting their usability (e.g., physical and/or procedural means).
The rest of this paper is organized as follows. In Section 2, we review the state of the art. Section 3 introduces actors involved in our solution and formalises the requirements we intend to meet. In Section 4, we describe the security model and the threat model on which we base our work. Section 5 shows the architecture of the proposed solution. Section 6 provides a formal security analysis and discusses assumptions and requirements fulfillment. In Section 7, we modify our solution to provide additional security features. Section 8 discusses the applicability of our approach in ICS environments. In Section 9, we present a prototype of the proposed solution and report informal feedback from experts. Section 10 draws the conclusions.
To mitigate the risk for critical systems to be infected by a malware, an antivirus can be adopted and properly configured to scan the data stored in the USB thumb drive before any access.
Most commercial antiviruses perform detection based on a database of known malware signatures. This approach has some drawbacks: it cannot detect zero-days attacks, it needs regular signatures updates to keep its effectiveness, its performances depend on the size of the data to be protected, and it cannot protect from generic tampering. Further, the class of attacks that leverage on the modification of the firmware (BadUSB attacks) makes regular antivirus largely ineffective since they use capability this kind of devices are allowed to use. However, it may detect or block further malware actions occurring after the BadUSB attack.
The primary countermeasure proposed against BadUSB was to protect USB devices by a firmware authentication feature that limits the firmwares that can be uploaded into a device to those signed by the device vendor (see for example [39]). However, this approach protects devices but not hosts, which are secured only if they are forcibly limited to interact with just protected devices. Further, this strongly limits the choice of USB storage devices and it is insecure, if the limitation is delegated to error-prone user behaviour.
GoodUSB [44] is a software solution that aims at protecting the host against BadUSB attacks. When a new USB device is attached, a message is shown to the user, which must declare his/her expectation about the functionalities of the device. The user has to make a decision, that means there is the possibility to incur in a human mistake or a deliberate malicious human behaviour. A similar approach is adopted by [17,22,27]. USBlock [30] consider the timing of USB traffic similarly to certain the intrusion detection approaches for IP networks. An architecture sketch to enable proactive firmware verification is proposed in [18].
There are a number of products on the market that specifically address security for RSD (e.g., see [4]) and USB thumb drives (e.g., see [40]). These are mostly focused on confidentiality, which, however, is not our primary objective. In these cases, support to integrity is on a file basis or on a block basis, and there is no integrity protection for the whole storage: an attacker can delete selected portions of data and also revert part of them to a previously saved version. Further, all solutions imply some form of authentication, usually password-based, but once the user is authenticated, full access to data is allowed, and a malware can easily infect the stored files. Further, the adoption of a password as a protection impacts the usability in term of ease to allow different people to use the device, i.e., the possibility to pass the device from hand to hand.
Integrity
Concerning techniques for checking the integrity of data, a large body of work is known in literature.
Protecting information by means of integrity in a scenario where there exists different types of machines (i.e. regular and critical) recalls the well known Biba integrity model [3], which describes a set of access control rules that can be used to protect the integrity of certain data. In the Biba model, each element is associated with an integrity level. The rules of this model deny any flow of information from lower levels to higher levels and can be summarised with the statement “no read down, no write up”. This model is implemented in recent versions of the Windows operating system [38]. However, any form of access control on a filesystem must be performed by a trusted operating system, while we want an USB thumb drive to be promiscuously usable even on untrusted machines.
Many integrity approaches rely on robust cryptographic hash functions [37]. When the dataset to be protected is large, using hash functions is inefficient. In fact, for each change, even small ones, the hash of the whole dataset have to be re-computed. Also, to check the authenticity of a small part of the dataset, the hash of the whole dataset should be checked. Authenticated Data Structures (ADS) allow a user to efficiently update a cryptographic hash of a large dataset when just a small part of the dataset is changed. For an ADS, the hash of the whole dataset is called root hash or basis. They also allow a user to efficiently check the integrity of a small subset of data by only comparing against the root hash an integrity proof of size
Widely-known ADSes are Merkle Hash Trees (MHT) [24] and authenticated skip lists [13]. MHTs are balanced search trees where leaves contains a cryptographic hash of the data and each internal node contains a cryptographic hash of a concatenation of the hashes stored in the children. For MHTs, the proof for a leaf l is made of the hashes stored in the sibling of the nodes that are in the path from l to the root.
For these data structures, updates and checks are performed in logarithmic time with respect to the size of the dataset, which is comparable to the efficiency of many indexes for databases and filesystems. For this reason, MHTes or other ADSes have been used in commercial, free, or research products. For example, MHTes were used for securing filesystems (see for example, [20,42]). Authenticated data structures were also adopted to authenticate relational database operations [7]. The problem of efficiently using ADSes with regular DBMS was studied in [8,26,32,33]. The efficiency problem of using ADSes in client server applications is studied in [34]. Other uses of ADSes in decentralized applications are shown in [5,6,23,35].
Actors and requirements
The actors of our solution are machines, humans, and USB devices. USB devices can be USB HIDes (for simplicity we consider only mice and keyboards) or RSDes. Machines are divided in critical and non-critical (or regular). The set of critical (non-critical) machines is the critical (non-critical/regular) realm. We consider critical realm as the part of the system that requires special protection against malware generated in the non-critical realm and spread by means of RSDes, which include thumb drives.
In the USB protocol, the newly attached device declares its type to the host (i.e., if it is a keyboard, mouse, or RSD). As for the protocol, a device is allowed to act only according to the type it stated.
We consider two different possible ways to interact with machines: data-flows and inputs. We define data-flows as data transferred from machine to machine realised by means of read and write operations on RSDes. We define inputs as data generated by device that allege to be HIDes. We have a malicious data-flow when the flow is from a regular machine to a critical machine. We do not consider a data-flow as malicious when data pass through a regular machine to a critical machine with the mediation of a special component of the architecture called Gatekeeper (see Section 5). We have a malicious input when the input is generated by a RSD that states to be an HID and, hence, the input itself was not generated by an interaction between a human and the HID.
In the following, we list the requirements that we have considered in the design of our solution.
The solution should prevent malicious data-flows and malicious inputs from reaching while allowing non-malicious ones. The solution should be able to detect malicious data-flows. In other words, the solution has to detect all kinds of integrity violations, comprising deletions and restoration of previous versions of files or parts of them. Malicious data-flows and malicious inputs should be detected before they reach critical machines. The solution should be usable in conjunction with the existing systems and software suites (SCADA, HMI, harsh laptops, development environments, inventory management, etc.), without requiring any invasive change to those products. The solution should preserve the convenience and high usability perceived by users when using RSDes and USB HIDes. The solution should not introduce asymptotic complexity overhead. Since operations for regular non-protected storage technologies run in at most The solution should be not vulnerable to human mistakes or intentional misbehaviour, hence, it has not to be based on any decision made by humans. The solution should be regarded deterministic for any practical purpose, that is, the probability that each single attack to be successful should be so small to make any brute-force attack not viable.
Security and threat model
We model an ICS as a set of machines (e.g. notebooks, workstations, SCADA, embedded systems, etc.) equipped with USB ports. In our model we assume that only RSDes and HIDes can be used as USB devices. Different USB devices are not allowed. RSDes and HIDes can be used promiscuously in both critical and non-critical realm. We define a RSD as malicious when it states to be an HID.
All data generated in the critical realm are considered trusted. Data flows from regular to critical realm are forbidden and allowed only using a gatekeeper (see Section 5.4). All other information flows should be allowed. This ideal setting conforms to the Biba integrity model [3] with just two integrity levels, where the rule “no read down, no write up” applies and the critical and regular realms are the higher and lower integrity level respectively.
Physical keyboards and mice are considered trusted and cannot be source of infections. RSD devices are considered non-trusted due to the possibility to change the firmware so that the device can act in a malicious way, i.e in a way that aim at damaging the system.
In our model, we consider an attack to be (1) any write operation performed by a regular machine on something that is supposed to be read by a critical machine comprising addition, deletion and changes to data, metadata and directory structure, and (2) any input generated by malicious RSDes that reaches a critical machine.
Architecture
In this section, we describe the architecture of our solution. We equip each critical machine with an hardware, that we call USBCaptchaIn, intended to be connected to one of the USB ports of the host. USBCaptchaIn is itself provided with a USB port where other USB devices can be connected. The idea is that USBCaptchaIn should always be in the middle between any USB device that is intend to be connected with a critical machine and the critical machine itself. For this reason, we assume that USBCaptchaIn cannot be unplugged from the machine and each critical machine has all available USB ports either protected by USBCaptchaIn or disabled.
Components of the proposed architecture.
In our approach, regular machines are not equipped with any specific hardware or software. The general architecture is depicted in Fig. 2. We also consider a special machine called gatekeeper that allows exceptional data transfer from regular to critical machines and whose details are described in Section 5.4. We now focus on the internal architecture of USBCaptchaIn.
The internal details of USBCaptchaIn are shown in Fig. 3. USBCaptchaIn is equipped with two USB ports: one upstream port and one downstream port (also called up/down ports). The up port of USBCaptchaIn is connected to one of the USB ports of a critical machine that we intend to protect. All USB devices that a user intends to attach to the critical machine should be attached to a down port. For the sake of simplicity, we present the architecture of USBCaptchaIn with only one down port. The introduction of additional down ports is a straightforward extension of the approach proposed in this paper.
Components of the USBCaptchaIn device.
Near the up port, there is an orange LED that indicates that the host is powering USBCaptchaIn and it is correctly working. Near the down port, there is a status red/green LED. The LED blinks green when one of the attached devices, possibly through a hub, is undergoing the authorisation procedure, turns fixed green when all devices are successfully authorized and can interact with the host, and turns blinking red if the authorization procedure of one of the attached devices failed too many times and the device must be disconnected. Messages required for user interaction are presented to the user on a 2.1″ TFT display which is embedded in USBCaptchaIn.
In USBCaptchaIn, a software intercepts, inspects, redirects, and injects USB traffic between up and down ports. When a user attaches the device to USBCaptchaIn, the interaction between device and USBCaptchaIn follows the USB protocol: an enumeration phase is performed, during which the device is supposed to provide specific information about itself. USBCaptchaIn listens the capabilities declared by the device and records all information provided during enumeration. If the device declares to be a RSD, USBCaptchaIn behaves as described in Section 5.2. If it declares to be a HID, USBCaptchaIn behaves as described in Section 5.3. In both cases, the software realises the rules described in our security model. The actual operation depends on the state of the authorisation procedure described in the above mentioned sections.
USBCaptchaIn encompasses the following components.
The screening router is in charge of routing USB packets to and from the ports, the controller, and the integrity subsystem. Its action depends on the authorization status of the device as explained in Sections 5.2 and 5.3, which may end up in filtering out certain USB traffic. It also performs standard USB enumeration, when a new device is connected.
The integrity subsystem handles read and write operations related to RSDes and executes additional actions to guarantee that the data flows constraints of our security model are met (see Section 4). The integrity techniques adopted are detailed in Section 5.2.
The controller orchestrates the display, the status leds, and the authorizators to realise the authorization procedure and human-machine interaction described in Section 5.2 and 5.3. It also reconfigures the screening router depending on the result of the authorisation procedure.
The authorizators manage the authorisation process of RSDes and supported HIDes types. The correct authorizator is chosen by the controller according to what is declared by the device. The RSD Authorizator performs some consistency checks (see Section 5.2), while each HID Authorizator generates challenge codes for the user, keep track of the number of attempts, and check the correctness of the submitted code (see Section 5.3).
The integrity subsystem is in charge of ensuring that data flows through RSDes comply with the constraints described in Section 4. Essentially, any data transfer from regular machines to critical machines should be blocked (exceptions are handled as described in Section 5.4). To efficiently perform this task and fulfil the Requirement E, we base our solution on ADSes (see Section 2.1).
Each RSD has a secure partition and an ADS partition. In the secure partition, we store data to be protected. In the ADS partition, we store an ADS over the data do be protected plus some additional cryptographic information. The state of the ADS is tightly coupled with the content of the secure partition.
RSDes store sequentially-numbered equal-sized blocks of bytes. In the USB protocol read and write operations issued by the host are at block level. The integrity subsystem intercepts these operations and inhibits those targeting blocks outside the secure partition. Operations that target the secure partition are performed along with additional tasks: reading encompasses integrity checks based on the ADS and writing encompasses update of the ADS. The root-hash of the ADS is kept signed in the ADS partition and used during the integrity checks. In the following, we provide the details of our solution.
In our approach, the following kinds of operations can be identified.
Protected-reads are read operations performed by the critical machine on data stored in the secure partitions of a RSD. Protected-reads are mediated by USBCaptchaIn, which checks the integrity of the read data. If data is recognised as genuine, the data is reported to the critical machine as result of the read. If data is recognised as tampered, the read operation is blocked and an error is communicated to the critical machine. As detailed below, this fulfil Requirements Ds, T, R and Dt and partially FI.
Protected-writes are the write operations performed by the critical machine on data stored in the secure partitions of a RSD. Protected-writes are mediated by USBCaptchaIn, which additionally updates the ADS and the signature of the root hash. During the ADS update some integrity checks are performed. If they fail, an error is communicated to the critical machine. This contributes to fulfilment of Requirements Ds, T, R, and partially FI.
An illegal-write is a write operation performed on a secure partition by a regular machine. The data changed by an illegal-write are always recognised by the subsequent protected-reads as tampered.
Plain-reads are normal read operations performed by regular machines when reading any part of a RSD comprising the secure partition.
Secure and ADS partitions are realised as regular partitions on the RSD. Before the Integrity Subsystem starts to mediate the interaction between host and RSD, the RSD authorizator performs the following checks that guarantee the safety of read/write operations performed by the Integrity Subsystem.
It reads the partition table and check its compliance with its standard format to exclude attacks at this level.
It identifies secure and ADS partitions. If they are not present, this procedure is aborted and the RSD is not authorised.
It checks the correctness of format and size of the ADS partition.
If the above actions are successful, it configures the screening router to pass all host read/write requests to the Integrity Subsystem. Further, it asks the Integrity Subsystem to initialise itself for handling the identified secure and ADS partitions (see below).
Before describing the Integrity Subsystem we need to introduce some concepts. Within each partition, we adopt the common approach of identifying blocks by a numbering, assigning zero to the first block of that partition. The size of the partitions are defined at the moment of their creation. Creation of partitions is handled by a specific software that can create only partitions with empty state, which are always recognised as genuine by USBCaptchaIn. This software just resizes existing partitions (like standard partitioning tools do) and create secure and ADS partitions with the empty state. This procedure can be performed on regular machines without affecting security, since partition creation does not imply any data flow in the sense described in Sections 3 and 4.
Each USBCaptchaIn device keeps, in local storage, its own private key and a corresponding certificate signed by a unique Certification Authortiy (CA), whose public key is also stored. We denote by U an instance of USBCaptchaIn and by
During initialisation of the Integrity Subsystem, right after the authorisation of the RSD, the last writer certificate is read and verified against the certificate of CA. The root-hash and its signature are read and verified against the last writer certificate. If any of these steps fails, the RSD is blocked and no operations are allowed on it, otherwise the root-hash is considered trusted.
When the critical machine asks to read a block b from Z through U, U retrieves the proof of b from the ADS (see Section 2). If it is consistent with the current trusted root-hash, the content of b is deemed to be genuine and is passed to the critical machine. When the critical machine asks to update Z through U, the ADS (comprising root-hash) and the signature should also be updated. This fulfils Requirements Ds, T, R, and Dt as far as access to RSDes is concerned.
To fulfil Requirement E, USBCaptchaIn has a caching mechanism: it performs update of the ADS partition only when there are no write operations pending, with a timer triggering the actual write, similarly to what regular operating systems do. The last writer certificate is updated the first time it is changed.
This approach does not completely fulfil Requirement FI. In fact, it cryptographically detects all kinds of tampering except the full reversion of both secure and ADS partitions to an older genuine version. A version of our approach that completely fulfil Requirement FI is presented in Section 7. A detailed security analysis is provided in Section 6.
We now describe the representation of the ADS in the ADS partition and its relationship with the secure partition (see Fig. 4).
For the sake of simplicity, we assume the secure partition contains n blocks, where n is a power of 2. In this case, our ADS has n leaves, in one-to-one correspondence with the blocks of the secure partition, and is a complete binary Merkle Hash Tree (see Section 2.1). From the properties of binary trees, the total number of nodes (comprising internal ones) is
Relationship between secure partition, ADS, array, and ADS partition.
In this section, we describe the HID authorisation process and interaction between USBCaptchaIn, the user, and the HID (i.e., a keyboard or a mouse), that occurs when the latter is plugged into the down port.
The authorisation process is based on a physical interaction between human beings and the HID just connected. After the enumeration phase, USBCaptchaIn starts the authorisation process asking to the user to input, by means of the HID itself, a randomly-generated challenge code.
Interactions and messages among user, device, USBCaptchaIn, and host for HID authorization.
The interaction for an HID that declares to be a keyboard is summarised in Fig. 5. In this case, the challenge code is a 5-characters alphanumeric string, which is communicated to the user by showing on the display a proper message with the code (Step 3 in Fig. 5). The user types the elements of the challenge code (Fig. 5, Step 4), which for a keybord are characters. Each typed character is sent by the device to USBCaptchaIn according to the normal USB protocol for HID (Fig. 5, Step 5). The authorizator checks that each received element matches with the corresponding element of the challenge code. If it matches, USBCaptchaIn provides a visual feedback to the user (Fig. 5, Step 6). For a keyboard we colour green the corresponding correctly typed element on the display. Then, USBCaptchaIn loops expecting further elements and checking them until the challenge code is finished.
If the challenge inputs are correctly inserted, USBCaptchaIn notifies the user that the new device has been authorised and that it can be used (Fig. 5, Step 7).
At the same time, USBCaptchaIn impersonates the device toward the host by performing a “replay” of the enumeration that was previously recorded (Fig. 5, Step 8). Then USBCaptchaIn configures the screening router to short-circuit (logically) the up and down ports (Fig. 5, Step 9).
USBCaptchaIn keeps monitoring the exchanged packets between the host and the device in order to recognise hardware or logic detach/re-attach operations and then trigger a new authorisation procedure, when needed.
If any of the received elements does not match the corresponding element of the challenge code, the authorization is started over again showing a message that, for a keyboard, is like the following
The authorisation process can be tried (Fig. 5, steps 3–6) for a maximum of three times. After three wrong attempts, USBCaptchaIn definitely blocks the device, ignoring any more input from it, and shows a message on the display, as follows:
To try again, the user has to detach and re-attach the device. This physical interaction makes a completely automatic brute-force attack impossible (see Section 6 for further details). Clearly, this is also the message displayed when a device maliciously declares to be a keyboard and tries a repeated guess attack. This approach fulfil Requirements Ds and T.
If the device is a mouse, USBCaptchaIn asks the user to move a pointer on the display to draw a line between two randomly-placed targets, for 3 times. The procedure was selected to obtain a good compromise between security and usability.
In this case, each element of the challenge is a pair of points of the USBCaptchaIn display, and the input of the user matches the element of the challenge if and only if the distance between the points of the challenge and the clicked ones is below a certain radius. The radius is chosen so that 24 non-overlapping targets can fit in the display (see Fig. 6).
The mouse authorisation method. (a) Allowed target positions and radius R. (b), (c), (d) The three steps of the authorization: in (a) just two rows are available for second target positioning, in (b) and (c) three rows are available.
Note that, instruction messages for the user are adaptively placed on the display on an unused zone, after the first point was chosen, to allow higher freedom in target positioning and make the required interaction harder to guess for a malicious RSD that pretends to be a mouse. See Section 6 for a security analysis.
Once the HID is authorised, USBCaptchaIn allows the HID to interact directly with the host, without adding any overhead to the USB packets exchanged by them, complying with Requirement E.
The above described architecture ensures high level of security and usability but does not support the relevant use case of bringing new legitimate data or software into the critical realm, like for example manuals or firmware. Note that, this need was leveraged in notable cases [9] in which an operator unintentionally transferred a malware into the critical realm in the context of a maintenance operation. For this reason, the first time data or software enters the critical realm from the regular realm accurate audit should be performed.
We introduce in our architecture a gatekeeper machine with the following three purposes:
enabling transfer of data or software from the regular realm to the critical realm realizing an exception to the Biba security model,
ensuring that, in these cases, an accurate verification is performed on the transferred data in accordance with a policy decided by the organisation that operates the gatekeeper,
logging this kind of operations.
The gatekeeper realises the “complete mediation” security principle [1]. Practically, it is a dedicated machine that (i) has one of its USB ports only partially protected, in the sense that it is not protected by USBCaptchaIn, but it is configured so that only RSDes can be plugged and from which any file can be read (i.e., checks of Section 5.2 are not performed), (ii) has all other ports protected by USBCaptchaIn, (iii) runs a specific software that performs thorough checks on the data read from the partially protected port, and (iv) writes the checked data on a secure partition on a RSD plugged into USBCaptchaIn of a protected port.
We point out that the gatekeeper is a complete mediation and policy enforcing point as it is true for other notable architectural elements used in cybersecurity contexts, like firewalls for networks and security reference monitors for operating systems. As in those cases, the security of the software that the gatekeeper runs and of the whole gatekeeper machine is paramount. We remark that the partially protected USB port must be configured so that only devices that declare themselves as RSDes can be attached, otherwise the gatekeeper itself could be vulnerable to BadUSB attacks. This can be also achieved by a distinct intermediate hardware blocking all devices that declare themselves not to be an RSD.
The gatekeeper is the single point where the policy regarding data flows from the regular realm to the critical realm is enforced and needs to be configured. While the actual policies may depend on the specific industrial context, we think the gatekeeper should perform at least (a) the authentication of the operator that requires the transfer, (b) the authorization or denial of the transfer according to the policy of the organization, and (c) the logging of the details of the operations performed, to allow subsequent auditing.
Our gatekeeping approach has two notable features.
It enables to scale-up the security level that an organization can achieve regarding data flows from the regular realm to the critical realm enabling the implementation of arbitrarily thorough analysis of the data to be transferred, adopting arbitrarily complex workflow to obtain the authorisation, which may also involve human decision or complex tests in virtual environments.
It helps keeping the infrastructural cost low, independently on the size of the critical realm, since one gatekeeper can, in principle, serve an arbitrarily large critical realm.
A formalisation of the role of the gatekeeper in ensuring the security of our architecture is part of the formal security analysis shown in Section 6.1.
Security
The intent of this section is to make a number of assumptions explicit and to formally prove the soundness of our approach, under those assumptions. We also discuss practical applicability and fulfilled requirements.
Formal analysis
Let C be the set of critical machines and R be the set of regular machines. A particular machine g is called gatekeeper and we also denote by
A malicious RSD is an RSD that declares to be an HID.
We intend that RSDes are not equipped with hardware that allows users to physically interact as HIDes do. Malicious RSDes declare themselves to be HIDes for malicious purposes due to a firmware change (the BadUSB attack, see Section 4) but are still not equipped with HID-like hardware. A non-malicious RSD is a good RSD. Good RSDes can possibly store malicious data.
A legitimate HID is a device that declares to be an HID, is actually equipped with hardware that enables a user to provide input, and passes to the host only the input provided by the user.
Examples of legitimate HID are real mouse or a real keyboard with properly working firmware. We do not deal with real HIDes with malicious firmware (we discuss this restriction at the end of Section 6.3). Hence, in the following, a device that declare to be an HID is either a legitimate HID or malicious RSD.
Any exchange of data between any machine in
This assumption essentially states that there are no alternative communication means between
A USB port is protected if it is equipped with USBCaptchaIn. A partially protected USB port completely blocks devices that declare to be HIDes and allows unprotected access to any partition of RSDes. In all other cases, a USB port is unprotected.
A partially protected port can be realized by a specific operating system configuration, or by an intermediate HID-blocking hardware to avoid relying on the operating system.
An attacker cannot remove the protection of any (partially) protected port.
This means that any USBCaptchaIn cannot be unplugged from protected ports. This also holds for partially protected ports obtained by HID-blocking hardware. For partially protected ports obtained by an operating system configuration, Assumption 2 means that the configuration cannot be changed by the attacker (see also Section 6.2).
USB port protection for machines in C: all ports are protected, G: one port is partially protected and all others ports are protected, R: all ports are unprotected.
The immediate consequence of the above assumptions is that any interaction of RSD or HID devices with a host in C is through USBCaptchaIn. For simplicity, when we write that a device d is “plugged into a machine
USBCaptchaIn correctly realizes all the checks described in Section 5 and cannot be itself compromised by malformed input.
With Assumption 4, we rule out any buggy implementation of USBCaptchaIn. In particular, we assume a correct realization of the checks mandated by our approach and proper standard sanity checks on the input (e.g., checks for respecting the USB protocol, for well-formed partition tables and ADS partitions, etc.).
With the following standard assumptions, we state the effectiveness of cryptographic primitives and of the realization of the public key infrastructure.
The adopted cryptographic primitives (signature and cryptographic hash function) are ideal and unbreakable.
Attackers cannot obtain a private key or force the certification authority to sign a new certificate.
The following lemma states the security of the HID authorization procedure, described in Section 5.3.
The probability that a USB device authorized as HID is a malicious RSD (and not a legitimate HID) is very close to zero and constant.
For an HID to be authorised, the user must successfully input a challenge code proposed by USBCaptchaIn. An RSD does not provide any means for the user to provide input, hence, for a malicious RSD that pretends to be an HID the only way to pass HID authorization is by guessing. After three failed attempts, the human intervention is required to gain more attempts. Hence, a malicious RSD has a very limited possibility to guess the challenge (see below) and brute force approaches cannot be used. Further, the attacker cannot exploit a successful RSD authorization since once a device is authorised as non-HID, any attempt to mimic HID behaviour requires a re-enumeration (by USB protocol). This can be triggered by a logic detach signal, but this, in turn, triggers a new authorisation process by USBCaptchaIn.
Now, we evaluate the probability of a malicious RSD to pass the HID authorization by chance. For keyboard authorisation, the challenge code consists of 5 characters each ranging within 26 letters plus 10 digits. The probability for a malicious RSD to correctly guess one random challenge is
For mouse authorisation, each challenge code consists of 3 pairs of points. The first point of each pair ranges within 24 possible positions. The second point ranges within the unused positions that remain after the text message is placed: 11 for the first elements (Fig. 6b) and 17 for the second and third element (Figs 6c and 6d). The probability of a successfully guessing all point pairs in a challenge is
The above considerations prove the statement. □
We are now ready to state the following lemma about allowed data flows.
Any machine in C can receive only data originated from other machines in C or data originated from R that has passed through the gatekeeper, except with very low probability.
To prove the statement, we analyse all possible data paths from R to C that do not pass through the gatekeeper and we show that USBCaptchaIn interdicts them.
By Assumption 1, in our model, R, C and G can only communicate by means of RSDes. Consider a RSD d plugged into a machine
By Assumptions 2 and 3, all the interactions between d and m are mediated by USBCaptchaIn. By Assumption 4, USBCaptchaIn cannot be compromised by inserting RSDes that contains malformed data (e.g., a malformed partition table or ADS partition) or performs a malformed USB protocol. Hence, d should undergo the authorisation procedures described in Section 5.
If d is malicious, by Lemma 1, d has a probability that is constant, but very close to zero, to pass the authorisation procedure. Hence, malicious data or software can be injected into m by maliciously mimicking user interaction from d only with very low probability.
If d is not malicious, it can store malicious content from R. This includes data stored in the secure partition, and all data stored in the ADS partition, namely, ADS, signature, and last writer certificate. We start by considering a tampering of a secure partition. Since the result of any protected-read operation is checked against the signed hash, through the proof derived by the ADS in the ADS partition, the tampering of data stored in the secure partition is easily detected. The attacker could try to avoid detection by tampering also the ADS partition. An attack to the ADS, that does not change the root hash, requires to find a collision for the hash function on which the ADS is based, which is against Assumption 5. On the other hand, to change the root hash the attacker should be able to violate the signature. However, this attack is ruled out by Assumptions 5 and 6.
If d shows itself as two virtual devices, one HID and one RSD, the above considerations hold independently for the two virtual devices. Hence, the virtual HID is blocked with very high probability and no m cannot read any data originating from R stored in the virtual RSD.
The above considerations prove that any data that m reads from d are written into a secure partition by an instance of USBCaptchaIn, i.e., by a protected USB port. Since protected ports are only in
Lemma 2 just states a result about allowed data flows. We now intend to prove the protection of C against data that do not comply with a “policy”, independently from the possibly promiscuous use of the RSDes.
We call policy a rule or a procedure that states if certain data are accepted or forbidden.
In the above definition, the word “data” should be intended as the unit on which the policy check is performed. As an example, the policy check can involve a single file, however, it may also act on a whole directory or on a directory tree. If certain data are accepted by the policy, we say that they comply with the policy or they are policy-compliant.
The policy does not change over time.
The following assumption formally asserts that the operators activity on machines in C is trusted.
No human intervention on any machine
The following assumption formally states the correct behaviour of the gatekeeper.
The gatekeeper checks all data read from partially protected port for compliance with the policy. Only data that are accepted by the policy are allowed by the gatekeeper to be transferred into a secure partition of an RSD plugged into a protected USB port.
We remark that the policy checks can involve knowledge of what data was accepted in the past or is currently in C. This enables also policies that can be effective against attacks that divide malicious data or software into smaller, seemingly legitimate, pieces.
The set C is healthy if all data in all machines of C comply with the policy, otherwise C is compromised.
Now, we can state the main result of our security analysis regarding the protection of machines in C. Under the above assumptions, and on the basis of Lemma 2, we now prove that an healthy system remains healthy over time, even if RSDes are promiscuously used.
If the set of critical machines C is healthy, it remains healthy after any operation involving a removable storage device d, independently from how d was used in the past, except with very low probability.
The RSD d may be malicious or contain malicious data or meta-data depending on its past usage. Any operation involving d encompasses plugging d into a machine
Now, we briefly discuss some practical implications of our assumptions.
Assumptions 1 and 2, regard the way critical machines are managed or physically realised. The idea that a critical realm should be physically disconnected from the regular realm is within the best practices in critical systems [43], matching Assumption 1. We can fulfil Assumption 2, by physically binding each instance of USBCaptchaIn (and any HID-blocking hardware) to its machine. This can be done for example by gluing the device to the USB port or by embedding it into the chassis. For partially protected ports, obtained by operating system configurations, Assumptions 2 can be fulfilled by using mandatory access control approaches, like SELinux [29].
Regarding Assumption 3, the first two items can be enforced by procedural practices during provisioning and deployment. The third item essentially imposes that an attacker cannot obtain a rogue USBCaptchaIn instance to use in the regular realm. Clearly, the hardware is useless for the attacker if its corresponding certificate is not properly signed. Hence, this item requires to have a strict management of the certification authority (see also Assumption 6) and to physically bind instances of USBCaptchaIn with properly signed certificates to their machines so that they cannot be used by an attacker for malicious purposes (see also Assumption 2).
Assumption 4 may be regarded as a demanding one. However, honouring it for a dedicated hardware is surely easier than honouring it for a software which runs on the host. In fact, the security of USBCaptchaIn is based on the security of a reasonably small and stable amount of software, while for a host-based solution all software running on the machine should be trusted unless proper mandatory access control configurations are in place, which may not be feasible in many environments. Further, certification procedures are much easier for a small embedded system whose elements are not subject to upgrades.
Assumption 5 is about ideality of cryptographic primitives. These primitives are not ideal in real-life, but they are computationally hard to break, if proper realization practices are adopted. From a practical point of view, we are assuming that cryptographic primitives are soundly realized and that the probability that an attacker can break one of them is irrelevant.
Regarding Assumption 6, private keys can be generated within USBCaptchaIn during manufacturing, possibly with the help of a dedicated secure hardware that makes exporting of the private key unfeasible (e.g. a TPM [45]). Proper certificate signing procedures should be in place during deployment of critical machines not to give the possibility to the attacker to obtain a rogue USBCaptchaIn to be used in an attack.
Assumption 7 imposes that the policy is stationary. While we think that a policy in a critical system rarely needs to be changed, we cannot exclude that this is actually needed in practice. A policy change clearly requires a change in the policy checking procedures in the gatekeeper, but this is not enough. In case of changing from policy P to policy
Assumption 8 is about trust in human operators which is a primary concern of organizations running critical infrastructures.
Assumption 9 rules out a buggy or badly configured gatekeeper with respect to the policy to be enforced. While, this is a demanding assumption, it is a single point where a high security level should be kept. The cost of designing/keeping the security of the gatekeeper may be high, but it is constant even if the size of C is large.
Other considerations about the practical application of our approach can be found in Section 8.
Fulfilment of security requirements
Now, we discuss the fulfilment of security-related requirements stated in Section 3, namely Requirements Ds, FI, T, R, and Dt. A discussion of non security-related requirement is provided in Section 8.
Requirement Ds is fulfilled since our approach can discern by cryptographic means data originating form C from data originating from R (see Lemma 2).
Requirement T is fulfilled since data whose origin is R is detected before they can be processed by any machine in C. Further, also any malicious RSD is blocked before it can perform any attack.
Requirement Dt is fulfilled since for both cryptographic integrity checks and HID authorization the probability of a successful attack is negligible.
Requirement FI is only partially fulfilled, as also mentioned in Section 5.2. Lemma 2 admits the case in which the attacker replaces the whole content of both the secure and the ADS partitions with an old version of them. In fact, origin of read data is in
Requirement R is fulfilled since our approach is not vulnerable to human mistakes or intentional misbehaviour regarding the usage or RSDes. In fact, we do not ask to the user to take any decision. Regarding the data integrity checks, they are totally transparent to the user. Regarding the authorisation process of HIDes, the user does not have to accept device features or authorize the device class. Actually, not even a malicious user can force USBCaptchaIn to authorise a device that claims to be an HID but offers no physical means to the user to provide the requested challenge code.
As already stated in the introduction, USBCaptchaIn cannot prevent a malicious HID (i.e., a keyboard or a mouse containing malicious code embedded in the firmware), to actually allow the user to enter the challenge code. Other proposals, like for example [44], have similar limitations. However, solutions like [28] analyse the timing characteristics of the USB traffic, which may detect a malicious HID. Nothing prevents to integrate into USBCaptchaIn a similar approach. Regarding to this limitation, it is useful to note that the promiscuous use of HIDes is much rarer that the promiscuous use of RSDes. Further, the promiscuous use of real HIDes can be easily blocked by other means without affecting usability. For example, the HIDes can be first approved by a technical team and then physically bound to the machines.
Ensuring full integrity and providing additional functionalities
As noted in Sections 5.2 and 6.3, the solution presented till now, does not completely fulfil Requirement FI. In fact, reversion to a previous version of the secure partition, along with its consistent ADS parition, is not detected as tampering. This may be regarded as an acceptable behaviour or not depending on the context. In this section, we modify our solution so that Requirement FI is completely fulfilled. The changes that we propose are not free. They introduce additional complexity, and in a certain sense, additional costs. This is the reason why they are presented here as an improvement and not in the main design, leaving open the possibility to adopt the limited version in situations in which partial fulfilment of Requirement FI is acceptable. The changes described in this section also offer the opportunity to provide additional functionalities that may be desirable.
How the coordination service fits the architecture described in Section 5.
The new general architecture is shown in Fig. 7. We introduce a coordination service (CS), whose functionality is to store key-value pairs in which each key is associated with one RSD (for example, the USB device identifier may be used for this purpose) and the value is the current root-hash of the ADS (and in turn of the current state of the secure partition). To connect with CS, a communication channel is needed. The bandwidth requirement for it is very small: only the RSD key and the cryptographic hash (the final root-hash) for each update of the secure partition should be sent. To support it, even a low bandwidth GPRS connection may be enough. We note that the availability of CS and of the connection might be an issue. In fact, if CS is not available or reachable, RSDes cannot be used. However, nothing prevents the adoption of standard high-availability approaches. Clearly, the communication between USBCaptchaIn and CS must be properly protected using standard technology (e.g., TLS [10]) and CS must be secured and authenticated.
If we accept the presence of a (low-bandwidth) communication channel, we can exploit it to provide an additional remote administration/monitoring functionality, which may be enabled on-demand under the control of CS. To realise this, we equip USBCaptchaIn with the capability to create a VPN toward CS, then a data connection between USBCaptchaIn and the critical machine can be created in two ways. If the critical machine supports fully fledged USB protocol, USBCaptchaIn may present itself during enumeration with an additional functionality of USB network card. Otherwise, a physical cable may connect USBCaptchaIn with a physical network interface of the critical machine.
This architecture may also support a certificate revocation procedure. In fact, CS may periodically provide to all USBCaptchaIn devices a certificate revocation list and possibly distribute new certificates.
Additional easy to implement functionalities are logging and monitoring of RSD activity and capability of administratively disable the use of RSDes on certain critical machines.
In Section 6.2, we already discussed practical aspects of our assumptions. In the following, we discuss other aspects of the applicability of our approach in real ICS environments.
RSD data integrity protection. Contrary to current suggested best practices [43], with our approach, users are allowed to use the same RSD with any machine without relying on passwords and without the need to install specific software. It is enough to equip critical machines with USBCaptchaIn. Protections offered by the integrity subsystem are largely transparent to users, addressing Requirement U (see Section 3). When an RSD is plugged into a USBCaptchaIn, only the secure partition is accessible to the critical machine. When an RSD is plugged into a regular machine, secure and ADS partitions should not be touched. To avoid unintentional tampering of them, the secure partition can be logically write-protected using capabilities supported by certain filesystems (e.g., NTFS) or partition tables (e.g., GPT). In this case, the secure partition can be mounted read-only on regular machines. Note that, if the above solutions cannot be adopted (for example for FAT-formatted drives with MBR partition tables), automatic read-write mounting of a secure partition may happen on a regular machine, which may end up in a detection of tampering due to automatic changes (e.g., update of mounted-bit flag, auto-defragmentation, etc.). To avoid this issue, we slightly change the behaviour described in Section 5.2: we store the content of the secure partition shifted of (at least) one block, so that, the first block(s) are unused and zeroed. USBCaptchaIn provides block numbers translations on-the-fly during protected-read/write operations. In this way, the filesystem cannot be recognised and mounting cannot occur on regular machines.
User interaction with USBCaptchaIn. We now briefly discuss the interaction of the user with USBCaptchaIn with respect to usability (see Requirement U). Concerning RSDes, no user interaction is required to authorise a RSD with well formatted secure and ADS partitions. HIDes authorisation requires the users to use the device in a regular way. If the device is a keyboard, they have to type. If it is a mouse, they have to click. A keyboard or a mouse attached to USBCaptchaIn can be used also to interact during the boot process and to execute recovery procedures.
Deployment impact. It is easy to deploy USBCaptchaIn in the critical realm since it does not need any driver on critical machines to work. USBCaptchaIn is totally independent from the operating system (OS) of the host it is connected to. It can be connected to any machine equipped with a USB port supporting standard USB protocol for keyboard, mouse and/or storage.
Our approach allows an organization to use any standard RSDes, promiscuously, complying with Requirement I.
The gatekeeper provides the organization with great flexibility about the security policies, but this means that they should be carefully designed and possibly integrated with business or decision processes. For strict security policies, traversing the gatekeeper may be costly, hence, it is advisable to deploy a critical machine realizing a repository of commonly used files ready to be used in the critical realm.
The coordination service may be realised in several ways. The simplest one, supporting only the full Requirement FI, is by ZooKeeper [16], which also supports high availability out-of-the-box.
The key management is quite simple. The integrity subsystem requires only the presence of an off-line certification authority which may already be present in the organization for other purposes. Aspects related with certificate revocations have been dealt with in Section 7.
We assumed RSDes and HIDes communicate with critical machines through USBCaptchaIn. This assumption can be easily guaranteed in several ways. For instance, a costly approach in term of money and changes required for the deployment, can be to integrate USBCaptchaIn directly into the hardware of critical machines. Instead, a cheaper approach, for example, can be to leave in critical machines only one USB port enabled and weld USBCaptchaIn to that port. Adopting one of these approaches, it is impossible to bypass the mediation of USBCaptchaIn without physical tampering.
Finally, since USBCaptchaIn is not able to prevent attacks coming form malicious HIDes (see Section 6) an organization adopting USBCaptchaIn should inhibit promiscuous use of HIDes by procedural of physical means, for example, by bonding HIDes to their assigned machine and prohibit the use of extraneous HIDes.
Prototypical realisation and feedbacks from experts
We realised two prototypes that implement the more important parts of the architecture described in Section 5. Our main objective is to evaluate the usability of USBCaptchaIn in practice. We showed the prototypes to ICS security experts. In this section, we also report their feedback.
We focused on assessing the fulfilment of the usability requirement for the authorisation process for HID devices and for accessing RSDes, that is for the use of the integrity system module.
Our first prototype realises USBCaptchaIn (see Section 5.1) on a Beaglebone Black board [2] on which a Linux kernel is running. In this prototype, we realised the elements that are needed to test the HID authorisation process, namely, screening router, controller, and HID authorizators. The software running on USBCaptchaIn is a customised version of USBProxy [41]. The filter and the authorizator are USBProxy plugins. The communication between the device connected to a down port and the screening router is realised by means of libUSB [21], a library that supports the interaction with generic USB devices, while the communication between the host and the screening router is realised by means of gadgetFS, a linux kernel module that allows the Beaglebone to act as a client towards the host. We packaged our prototype so that it can be used on real systems. The final result is shown in Fig. 8.
The hardware prototype for HID authorisation. The display shows a message during keyboard authorisation procedure.
Our second prototype mimics the functionalities of the integrity system module (see Section 5.2). It consists of a software that, differently from our target design, is intended to be installed in critical machines. However, it provides the same level of security and a very similar user interaction. In our simplified realisation, we intercept file system actions at the system call level by using standard open source drivers [11,12]. User files and directories are stored in a regular directory of the RSD, while the corresponding ADS is stored in an auxiliary directory according to a proprietary format. Files and directories can be accessed using the regular system calls of the operating system. Our software intercepts them and performs corresponding operations on plain data and on the ADS using regular read and write primitives of the kernel. More details about this prototype can be found in [14].
We showed our prototypes to security experts that we met within meetings of the Preemptive EU research project [25]. The feedback was very positive for both of them. We recorded no complaints about usability. One of the most appreciated aspects was the possibility to realise them in independent hardware. Some of the people we talked with, also suggested that USBCaptchaIn could be physically mounted within existing hardware whose USB ports should be protected, while keeping it isolated from the rest of the system for security. Some have pointed out that promiscuously using RSDes formatted for use with USBCaptchaIn into other systems may raise annoying false positives due to users accidentally manipulating integrity-protected data on a regular system. However, this can be easily mitigated by exploiting support for soft read-only protection of files (in the prototype) or partitions (in the target design), which should avoid most of the accidental modifications, as described in Section 8.
Concerning efficiency, on the HID authorisation side, once mice and keyboards are authorised, the mediation of USBCaptchaIn does not introduce any noticeable delay for a user with respect to the case where the HIDes are directly connected to the host. On the integrity protection side, our experiments performed with our prototype have shown that the additional overhead is negligible with respect to timings involved in normal user interactions, like working on documents and opening multimedia files. The overhead is mainly due to the fact that for each operation on data a corresponding operation on the ADS must also be performed. While for read operations this might be mitigated by proper caching (which is automatically performed by the operating system in our prototype), caching is not helpful for write operations. With the diffusion of USB 3.0 devices, this kind of overhead will progressively be less and less important. On the other hand, the limited computing power of a cheap board may severely limit the transfer bandwidth to and from the RSD, with respect to the bandwidth supported by USB 3.0. However, this aspect is more related with a market strategy trade-off and out of the scope of this paper.
We presented an architecture based on a dedicated hardware for protecting critical machines in a ICS against malware spread by means of USB devices. USBCaptchaIn realises a new approach to protect hosts, both against BadUSB attacks, in which generic USB devices maliciously mimic the behaviour of HID devices, and against malware embedded in data stored in RSDes. The proposed approach proactively blocks attacks before they reach the target and does not rely on decision of the users. It is highly compatible with already deployed products, comprising embedded devices, like Programmable Logic Controllers, Remote Terminal Units, etc., on which is often not feasible to install new software. The occasional need of transferring software or data into the critical realm is also addressed providing a single policy enforcement and logging point for this kind of operations.
The user experience is only slightly altered by the protection offered by our solution and the presence of USBCaptchaIn does not impact USB devices responsiveness.
Our informal contacts with experts, to whom we have shown our prototypes, have reported that a solution like the one we described might be accepted in a real ICS environment.
Further research work may encompass the study of supporting a Biba security model with more than two security levels. This may be useful, for example, to support a split of the critical realm in a production realm (highly critical) and a testing realm (less critical). Further classes of HIDes may also be supported (e.g., touch tablet, track-ball, joystick, etc.). The integration in USBCaptchaIn of a solution like the one described in [28] may add a form of protection against real keyboards with malicious firmware without affecting security and usability.
Footnotes
Acknowledgments
We would like to thank Marco Sacchetti and Diego Pennino for their contribution to the realisation of the prototypes. This work was partially supported by the European Commission under project “Preemptive” (grant agreement n. 607093).