Mehdi Sabraoui

Jeffrey Hieb

Adrian Lauf

James Graham

Chapter 14 MODELING AND MACHINE-CHECKING BUMP-IN-THE-WIRE SECURITY FOR INDUSTRIAL CONTROL SYSTEMS

Keywords: Industrial control systems, security, formal methods, verification 1

This chapter describes the formal modeling and machine-checking of a bump-in-the-wire device that secures field device communications in industrial control networks. Field devices serve as the connection points between computer-based control systems and the physical processes being controlled. Industrial control network traffic is routinely checked for transmission errors, but limited mechanisms are available for combating attacks that exploit industrial control protocols to target critical infrastructure assets.

This chapter focuses on a bump-in-the-wire solution that can be retrofitted on field devices to provide security functionality. The TLA+ formal specification language in combination with the isolation guarantees provided by the seL4 microkernel are used to demonstrate that the bump-in-the-wire solution provides important security and liveness properties. The resulting machine-checked system correctly applies hash-based message authentication to verify the authenticity of incoming messages while being resistant to attacks.

Introduction

In 2014, the National Institute of Standards and Technology (NIST) released a cyber security framework [START_REF]Framework for Improving Critical Infrastructure Cybersecurity, Version 1.1[END_REF] intended to enhance the cyber security postures of critical infrastructure assets. Industrial control systems are used across the critical infrastructure sectors, including chemical, critical manufacturing, dams, energy, food and agriculture, nuclear facilities, transportation systems and water treatment systems. These installations are often unpatched, offer low resilience to unexpected network traffic and incorporate few mechanisms that protect against malicious activities [START_REF] Stouffer | Guide to Industrial Control Systems (ICS) Security[END_REF]. The NIST framework - and the executive order that drove it [START_REF] Obama | Presidential Policy Directive 21: Critical Infrastructure Security and Resilience (PPD-21)[END_REF] -highlight the need for strong cyber security in critical infrastructure assets that have historically focused on safety and physical security.

A secure system, like a safe system, should be designed to preserve certain properties and the implementation should satisfy these properties. Thus, the problem of developing a secure system involves two sub-problems: (i) formally express the core security properties of the system; and (ii) prove that the core security properties hold for every possible system state. Whether the system is a virtual banking application or a water treatment plant control system, high degrees of trust in the system design and implementation are paramount.

An industrial control system is a general term that describes myriad configurations of networked computer systems that operate and control physical equipment and processes in infrastructure assets. These systems make heavy use of mature, low-power and low-overhead technologies such as RS-232 communications and decades-old networking protocols to pass control commands and data between devices [START_REF] Igure | Security issues in SCADA networks[END_REF].

Figure 1 shows a typical industrial control system with three major components: (i) central control unit (or master terminal unit (MTU)) at the control center; (ii) remote control units (or remote terminal units (RTUs) or more generally field devices) at field sites; and (iii) communications equipment and protocols that link the central and remote units. The central control unit has a human-machine interface (HMI) used for plant operations. The field devices, which perform sensing and control, range from simple circuit boards powered by embedded controllers to expensive programmable logic controllers (PLCs) with racks of components. Since the master or central control unit gathers data from the field devices and sets operating parameters and issues commands to field devices to orchestrate plant operations, the overall system is often referred to as a supervisory control and data acquisition (SCADA) system.

Unlike typical enterprise information technology networks where confidentiality is a priority, industrial control networks value availability and integrity above confidentiality [START_REF] Mackenzie | SCADA security basics: Why industrial networks are different than IT networks[END_REF] -keeping the data in the system private is not as important as keeping the system running properly. Cyber threats to industrial control systems reflect this priority -attackers seek to disturb and disrupt the controlled processes rather than exfiltrate sensitive data. Attacks that disrupt network flows in industrial control systems can be devastating from the financial and safety perspectives [START_REF] Falliere | Stuxnet introduces the first known rootkit for industrial control systems, Symantec Security Response Blog[END_REF][START_REF] Shamir | Analyzing a New Variant of BlackEnergy 3: Likely Insider-Based Execution[END_REF][START_REF] Sullivan | How cyber-attacks in Ukraine show the vulnerability of the U.S. power grid[END_REF][START_REF] Wagner | Infrastructure under attack[END_REF]. The importance of maintaining availability disincentivizes regular system changes or updates for fear of unscheduled downtime. Attacks on SCADA protocols are often trivial because the protocols have few, if any, security features. Modbus, one of the most popular SCADA protocols, was developed in 1979 [START_REF]Modbus over Serial Line: Specification and Implementation Guide, V1.02[END_REF]. Modbus is a simple, connectionless protocol that can be modeled rigorously. This research considers the Modbus ASCII protocol [START_REF]Modbus over Serial Line: Specification and Implementation Guide, V1.02[END_REF].

Figure 1 shows the layout of a Modbus ASCII protocol data unit (PDU). It comprises a colon ":" to signal a new packet, two bytes for the recipient address, two bytes for the function code; up to 504 bytes for payload data, two bytes for a longitudinal redundancy check (LRC) that helps detect transmission errors and an ending character sequence "\r\n."

A fully verified microkernel such as seL4 [START_REF] Klein | seL4: Formal verification of an OS kernel[END_REF] provides a platform for constructing software solutions for high assurance environments. Instead of a security statement such as "this system works for my expected inputs," seL4 enables a high-assurance statement to be made about the system: "this system works as expected for every possible input at an affordable cost." The platform provides process isolation through isolated address spaces. This supports the development of logically-contained processes, where each component acts on its own accord and communications between each component are controlled strictly.

The seL4 architecture enables a properly-designed microkernel environment to be treated as a distributed system on a single chip. A concurrency modeling language such as TLA+ [START_REF] Lamport | The temporal logic of actions[END_REF][START_REF] Lamport | Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers[END_REF][START_REF] Lamport | The TLA Home Page (lamport.azurewebsites.net/tla[END_REF] can be used to model the states and interactions of components, and each trace of state transitions can be machine-checked to conform to the modeled security properties (e.g., the secret key is confined to a certain component and only valid packets can reach the inner components). PlusCal, an algorithm language translatable to TLA+, can be used to model the sequential steps in the operation of each component.

This research focuses on a bump-in-the-wire solution that can be retrofitted on SCADA field devices to provide security functionality. It leverages TLA+ and PlusCal to model the components of the Modbus-based bump-in-the-wire security device that is designed with the seL4 microkernel in mind. The TLA+ formal specification language in combination with the isolation guarantees provided by the seL4 microkernel are used to demonstrate that the bump-in-thewire device provides the desired security and liveness properties. The resulting machine-checked system correctly applies hash-based message authentication to verify the authenticity of incoming messages while being resistant to attacks. In particular, the verified specification assures that only valid, authenticated Modbus packets flow across a field device, that a compromised component cannot break the security properties of adjacent components, that the device is not vulnerable to replay and spoofing attacks, and that the device is resilient to malformed and malicious traffic.

Background

The threats to traditional information technology infrastructure are well documented, but when industrial control systems merge with traditional information technology networks, the threats become even more significant in their scope and magnitude. Attacks such as the 2000 Maroochy Water breach [START_REF] Abrams | Malicious control system cyber security attack case study -Maroochy Water Services[END_REF] and the 2010 Stuxnet worm [START_REF] Anderson | Confirmed: US and Israel created Stuxnet, lost control of it[END_REF][START_REF] Falliere | Stuxnet introduces the first known rootkit for industrial control systems, Symantec Security Response Blog[END_REF][START_REF] Falliere | Stuxnet Dossier, Version 1.4[END_REF] demonstrate that even isolated industrial control systems are vulnerable to external threats. A Kaspersky Lab report [START_REF]Threat Landscape for Industrial Automation Systems in the Second Half of 2016[END_REF] states that more than 10% of all blocked threats on industrial control computers originated from removable media such as USB drives. An attacker who gains access to an industrial control network finds little in the way of security mechanisms. Industrial communications protocols have limited, if any, security mechanisms and the SCADA protocols often lack basic authentication and integrity checking [START_REF] Martin-Liras | Comparative analysis of the security of configuration protocols for industrial control devices[END_REF]. Meanwhile research has demonstrated that certain interactions involving industrial control protocols (e.g., Modbus TCP) and their carrier protocols (e.g., TCP/IP) can defeat security and integrity guarantees [START_REF] Edmonds | Security analysis of multilayer SCADA protocols[END_REF].

The longevity and uptime requirements imposed on industrial control systems present unique challenges to keeping them secure. Physical systems can be difficult to test, upgrade and replace. Thus, the ages of physical systems and their software are often measured in decades and the downtime costs are significant. Fragile, out-of-date firmware and protocol stacks are common and they exhibit anomalous behavior with non-conforming, let alone, malicious, traffic. Unexpected network traffic can cause heavy machinery to act in unpredictable ways. Any system state that has not been explicitly evaluated during the design phase poses a risk of disruption.

Industrial Control System Security

Efforts to address industrial control system security are generally aligned with the categories defined in the NIST framework [START_REF]Framework for Improving Critical Infrastructure Cybersecurity, Version 1.1[END_REF] -detect, protect, identify, recover and respond. Detection leverages monitoring methodologies and tools for generating logs for low-performance field devices in SCADA systems, exporting logging data without fear of opening new attack vectors and con-ducting analyses without impacting system operations (see, e.g., [START_REF] Gary | ICS/SCADA smart scanning: Discover and assess IT-based systems in converged IT/OT environments[END_REF][START_REF] Scarfone | Guide to Intrusion Detection and Prevention Systems (IDPS)[END_REF]). Protection involves the development and application of security mechanisms in software [START_REF] Amoah | Formal modeling and analysis of DNP3 Secure Authentication[END_REF] or hardware [START_REF]Blue Coat ICS Protection, Scanner[END_REF]. Identify involves cataloging system assets and potential risks with efforts concentrating on the system as a whole [START_REF] Gary | ICS/SCADA smart scanning: Discover and assess IT-based systems in converged IT/OT environments[END_REF] as well as on individual components such as vendor software and hardware [23][START_REF]Threat Landscape for Industrial Automation Systems in the Second Half of 2016[END_REF][START_REF]Threat Landscape for Industrial Automation Systems in H2 2017[END_REF]. Recovery involves picking up the pieces after an incident (accident or malicious) and incorporating the lessons learned in preparing for future incidents [START_REF] Bartock | Scarfone, Guide for Cybersecurity Event Recovery[END_REF][START_REF]The Protection of Critical Infrastructure against Terrorist Attacks: Compendium of Good Practices[END_REF]. Finally, response involves all activities that follow the detection of an incident (whether successful or not), including communication, analyses and mitigation [START_REF] Cichonski | Computer Security Incident Handling Guide[END_REF][START_REF] Permann | Mitigations for security vulnerabilities found in control system networks[END_REF]. The work described in this chapter falls in the protection and detection categories, with the cryptographic signing mechanism supporting both forgery protection and detection.

seL4 and CAmkES

The seL4 microkernel has been fully verified from design to implementation to provide an exceptionally high level of assurance [START_REF] Klein | Experience report: seL4: Formally verifying a high-performance microkernel[END_REF][START_REF] Klein | seL4: Formal verification of an OS kernel[END_REF]. It has evolved from the OKL4 family of microkernels that were reduced in size to the point where guarantees of bug-free code could still be realized. The seL4 microkernel has the verified ability to logically separate processes and implement highly-specified channels of communications between components in an architecture. If a cell in the kernel is compromised, it is shown that the other cells still maintain their desired security properties. This enables an abstract implementation of Rushby's separation kernel [START_REF] Rushby | Design and verification of secure systems[END_REF] for reducing a large security kernel into smaller, more easily provable, components that mimic a distributed system.

CAmkES is a component platform designed to address the increasing complexity and unreliability of embedded systems by facilitating the modular design of system services [START_REF] Fernandez | CAmkES Formalization of a Component Platform[END_REF][START_REF] Kuz | CAmkES: A component model for secure microkernel-based embedded systems[END_REF]. CAmkES supports microkernel development; its design favors a low-overhead approach to accommodate the challenges involved in microkernel development. The CAmkES architecture provides a component model, standard interfaces (including support for user-defined interfaces) and user-defined interactions between components using these interfaces.

TLA+ and PlusCal

TLA+ is a formal language for modeling and reasoning about concurrent systems [START_REF] Lamport | The temporal logic of actions[END_REF][START_REF] Lamport | Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers[END_REF][START_REF] Lamport | The TLA Home Page (lamport.azurewebsites.net/tla[END_REF]. PlusCal is a language for modeling algorithms in a much more expressive manner than typical programming languages. TLA+ and PlusCal use mathematical notation to expand their reach beyond programming languages to allow for rigorous definitions and descriptions of algorithms and systems. The mathematical notation also facilitates model checking and proofs of properties of algorithms and systems.

PlusCal, which is a programmer-friendly option in the TLA+ toolchain, can be automatically translated to TLA+ and used with the TLC model checker provided by TLA+. TLC is a brute-force model checker that explores states up to a certain number of transitions, raises alerts about properties that have been violated and provides traces where the violations occurred. This research has employed TLA+ for two categories of checks that are defined and performed for each state and transition reached by the model checker: (i) invariants; and (ii) liveness properties.

Invariants are statements are always true regardless of the system state. An invariant in a simple banking example is: an account balance is never less than zero. This invariant is expressed in TLA+ as follows:

∀ acct ∈ Accounts : acct.balance ≥ 0 ( 1 )
The initial state of a system might satisfy all the invariants, but then the system may never leave its initial state. A system that never changes its state is not useful. Therefore, liveness properties are specified. A liveness property -or temporal property -checks that a property is eventually true. A liveness property for a binary clock that alternates between zero and one is: if the clock bit is currently one, then it will eventually be zero. An example liveness property that is applicable to this research is: if an incoming message is a valid communications packet, then it will eventually be processed and forwarded. This liveness property is specified as follows:

message.valid = T rue f orward = T rue (2)

Related Work

The DNP3 SCADA communications protocol is commonly used to transmit commands and data between a central operations center and remote substations [START_REF]Control Microsystems, DNP3 User and Reference Manual[END_REF][START_REF] Curtis | A DNP3 Protocol Primer (Revision A), DNP3 Users Group[END_REF][START_REF] East | A taxonomy of attacks on the DNP3 protocol[END_REF]. DNP3 Secure Authentication [START_REF] Gilchrist | Secure authentication for DNP3[END_REF] adds security mechanisms to the basic DNP3 protocol to provide authentication and authorization. Amoah et al. [START_REF] Amoah | Formal modeling and analysis of DNP3 Secure Authentication[END_REF] have conducted a formal behavioral analysis of DNP3 Secure Authentication. They employed colored Petri Nets to model common replay, modification and spoofing attacks on the DNP3 Secure Authentication specification, in the process, discovering a previously-unknown attack that could be launched by an attacker with access to data in motion, but without access to the secret key. Their modeling of the communicating entities and an attacker revealed that the snooping of non-aggressive challenge response sessions by the attacker could modify the sequence number and issue a request in the aggressive mode of DNP3 communications. This resulted in the attacker being able to spoof a valid request and replay previous messages sent in the network. This attack specifically targeted critical requests that changed system operations by modifying set-points and setting parameters.

Kuhn and Dray [START_REF] Kuhn | Formal specification and verification of control software for cryptographic equipment[END_REF] have applied formal modeling and verification techniques to a microprocessor-based device to create a smart token system for controlling access to network hosts. Their objective was to create a civilian securitycritical system where formal methods could be used to improve the system; this system could then serve as a testbed for applying formal methods for securing larger projects. The application of formal methods contributed to correcting inconsistencies in the smart token design, improving its resilience and finding a subtle, but critical, bug that could have completely compromised the security provided by the smart token. Kuhn and Dray noted that the application of formal methods to their project had tangible benefits despite its limited focus and small budget.

The DARPA-funded High-Assurance Cyber Military Systems (HACMS) Program [START_REF] Fisher | The HACMS Program: Using formal methods to eliminate exploitable bugs[END_REF] has worked with Boeing to increase the security of an unmanned H-6U helicopter in a practical manner using formally-verified code and the seL4 microkernel. Engineers were able to separate the components of the H-6U into different virtual machines running on an seL4 hypervisor and then convert certain components from the virtual machines to fully-verified native components. Although verifying the entire H-6U system was infeasible, the effort was able to verify select components to expand the trusted computing base of the system and enhance its reliability. The upgraded H-6U was able to stay in flight and complete its test mission despite being actively attacked by multiple compromised components and a professional red team. The attackers were unable to pivot from the compromised components to affect H-6U flight control or mission control.

Security Preprocessor Checking Using TLA+

Hieb and Graham [START_REF] Hieb | Security preprocessor for industrial control networks[END_REF] have proposed a bump-in-the-wire solution that enhances communications security between control centers and field sites that employ legacy systems. The solution introduces an inline security preprocessor that retrofits raw communications packets with authorization and authentication; the encapsulations are stripped at the field sites. The bump-in-the-wire design does not impact control and configuration operations because the preprocessor is transparent to the control center and field devices. The approach adds some latency; however, since the timing requirements for control systems range from microseconds to seconds, the latency provided by the added security is acceptable in many industrial control systems [START_REF] Gilchrist | Secure authentication for DNP3[END_REF][START_REF] Hieb | Security preprocessor for industrial control networks[END_REF].

The preprocessor of Hieb and Graham [START_REF] Hieb | Security preprocessor for industrial control networks[END_REF] incorporates three components: two for communications and a middle component that performs the authorization and authentication checks. This section extends the design by adding higher assurance via guarantees provided by seL4 and model verification using TLA+. The desired properties of the preprocessor are first translated into TLA+. Following this, a model is built that preserves the security properties.

System Modeling

The new system model has four components that logically separate the security functions: (i) checking that messages conform to the Modbus specification; (ii) signing messages with SHA-2; (iii) networking with raw Modbus messages in a trusted network; and (iv) networking with encapsulated/signed Modbus messages in an untrusted network. The separation isolates critical decisions, rendering exploitation more difficult and supporting parallelism to improve performance should the need arise. Each of the four components runs as a separate process, confining each critical decision-making block of code to its own memory space. Each component was also modeled separately in TLA+, following which all the components were modeled together to explore the security properties of the system as a whole. Figure 2 shows the four components. Each component provides a message interface and consumes messages from two other components.

Crypto

Modchk

Modtx Signtx

Each thread component was specified separately using PlusCal and then collectively as an asynchronous system. An example is the signature checking thread of the Crypto component in Figure 2. Each thread is provided with a queue from which it dequeues a message and performs its processing. The Modtx component can place messages in the queues of Modchk and the message signing thread of Crypto. The Signtx component can place messages in the queue of Modchk and the signature verification thread of Crypto. This system of message passing to queues is an abstraction of the interprocess communications between the four CAmkES components.

TLA+ and its TLC model checker enable sets to be defined and each element of the sets to be used when exploring model states. It would make sense to define a set that includes every possible input for every thread. However, in the case of network communications, it is impossible to specify the set of all possible bits that can be read from or written to a serial port. This task is infeasible even when the message size is restricted to the Modbus specification. Therefore, this work uses specially-crafted packets to test the typical cases and edge cases of valid and invalid messages that could be encountered with the goal of showing that every message is covered by these cases. The serial port was also abstracted as receiving and sending messages one byte at a time to limit the search spaces of incoming and outgoing data to single bytes at a time. The checking begins when a set of messages arrive at the Modtx component and a different set of messages arrive at the Signtx component. The simulation ends when all the queues are empty and there are no further states to explore. Microsoft's specification of Cosmos DB [START_REF] Azure | Azure Cosmos TLA+ specifications[END_REF] is a similar message passing system that uses TLA+.

Invariants and Liveness Guarantees

Table 2 shows the desired system properties. The four invariants ensure that: (i) only messages with valid lengths make it to the inner components; (ii) messages in the queues of the networking components are checked for validity by the components from where they came and the valid messages are printed to the screen; (iii) only well-formed and properly-verified Modbus messages reach the trusted network; and (iv) only well-formed and properly-signed Modbus messages reach the untrusted network.

Liveness properties are more difficult to check in a large model. However, the two liveness properties in Table 2 ensure that: (i) messages entering the preprocessor from a networking component eventually reach the opposite networking component and are eventually consumed; and (ii) all queues are eventually emptied.

The messages selected to push through the system drive the model. Since it is not possible to model every possible input to the networked components, only certain amounts and types of messages that exercise every state in the model are employed. The TLC model checker keeps track of the number of times each state is reached; states that are reached zero times are of particular interest. Although a concise set of messages has not been found to hit every state in a single run without running out of memory, each state can be reached over multiple runs with different sets of inputs. The inputs include messages that are too short to be valid, messages that are too long to be valid, messages that are valid, messages that contain incorrect characters, messages that cause restarts, and all possible single-byte inputs.

Specifying and Checking Properties

Two components interface with an output (i.e., printing to the screen in a virtual machine and printing to a serial port on hardware). The first component, Modtx, reads and transmits Modbus messages while the second component, Signtx, reads and transmits signed Modbus messages.

The Modtx component has a read thread and a write thread. The component reads a byte at a time from the serial buffer until its buffer is full or a colon (:) is received to signal a new Modbus packet or a carriage return/line feed (\r\n) is received to signal the end of a Modbus packet. The Modtx buffer is large enough to hold the largest Modbus packet as defined in the Modbus specification. When the buffer fills without the \r\n, it is cleared and its index is reset. If a colon is received, then the buffer is cleared and the colon is placed at the head of the buffer. When a \r\n is received, the Modtx component interprets its buffer as containing a completed Modbus packet. The packet is assigned an ID and is simultaneously passed to both the cryptography component and the Modbus checking component.

The Modtx write thread gathers messages from the Modbus checking component and Crypto component. If a new message with a unique ID comes from the Crypto component, it is stored until a message with the same ID is also received from the Modbus checking component. After the two messages have been received, both messages are checked for validity. If the Crypto component was able to validate the message signature and the Modbus checking determined that the message contained a correctly-formed Modbus packet, then the raw Modbus message is printed to the output. Thus, a message is printed only if both the checking components agree the message is valid.

The invariants and liveness properties in the Modtx specification ensure that only well-formed, verified packets are printed, that the data to be transmitted is eventually transmitted and only whole (not necessarily well-formed) messages reach the inner components.

The top half of Table 3 shows the two invariants and two liveness checks for the Modtx read thread, which reads bytes from the trusted serial port. The fist invariant stipulates that the receiving buffer never exceeds the maximum size of a Modbus message. The second invariant stipulates that the application buffer (holding data to be forwarded to the inner components) never exceeds the maximum size of a Modbus message. The two liveness checks ensure that if a complete Modbus message is received (starting with a colon and ending with \r\n) and is under the maximum size, then the message is eventually processed and forwarded to the inner components.

The bottom half of Table 3 shows the two invariants and three liveness checks for the Modtx write thread. The first invariant stipulates that a byte is only sent if the original message is a valid Modbus message. The second invariant stipulates that only valid Modbus characters reach the sending register. The Table 3. Desired Modtx component properties.

Modtx Read Thread Property

A receiving buffer containing bytes read from the Invariant serial port does not hold more than a Modbus message A buffer containing bytes to be forwarded to inner Invariant components does not hold more than a Modbus message A well-formed Modbus message in the receiving buffer Liveness is eventually processed A well-formed Modbus message is eventually forwarded Liveness to inner components

Modtx Write Thread Property

A byte is printed to the serial port only if the entire Invariant Modbus message is valid Only valid Modbus characters are stored in the serial Invariant port register A sending buffer containing a valid Modbus message is Liveness eventually emptied A valid Modbus message to be printed is eventually Liveness printed A transmit flag that is raised is eventually lowered Liveness first liveness check ensures that if there is a message to send (transmit flag is raised) and the message is a valid Modbus message, then the buffer is eventually emptied. The second liveness check ensures that if there is a valid Modbus message to send, then the bytes are eventually sent. The third liveness check ensures that if the transmit flag is raised, then it is eventually lowered to allow a new message to start the process again. The Signtx component works in a similar manner as the Modtx component, but with two exceptions. Its reading thread looks for a complete encapsulated message instead of a complete Modbus message and it utilizes the Crypto component to validate signatures instead of its signing functionality. The Signtx component assigns ID numbers to incoming messages and forwards decapsulated messages to the Modbus checking component.

Checking Modbus Properties

The Modbus protocol is modeled within TLA+ and a mechanism is incorporated to check that a given stream of bytes conforms to the Modbus standard [START_REF]Modbus over Serial Line: Specification and Implementation Guide, V1.02[END_REF]. These are necessary to ensure that only valid Modbus packets can traverse the preprocessor.

The Modbus specification is more a definition than a model of behavior. As shown in Table 1, a Modbus message has five simple fields and a longitudinal redundancy check for determining transmission errors. The lengths and character sequences in the fields in a Modbus packet are clearly defined, so it is straightforward to analyze each field. The head of the packet is checked to be the colon. The address and function fields are both checked to be two-byte hexadecimals. The data field is checked to be between zero and 504 bytes long and all the characters are hexadecimal. The end of the data field is found by taking every character from its start to the length of the packet and subtracting four. The longitudinal redundancy field is checked to be two hexadecimal characters and that the value in the packet matches the computed value. The end field is checked to contain exactly \r\n.

The Modbus message definition is used as an invariant in other specifications. This requires checking that the length of a received message is within the Modbus size limits. Next, each field of the message is examined individually to determine if it matches its definition. A message is a valid Modbus message when all the components match the definitions in Table 1. The Modchk component passes its decision (valid or invalid) along with the message itself to the opposite component from which the message was received.

Checking Cryptographic Properties

The Crypto component has two functions: (i) message signing; and (ii) signature verification. The seL4 architecture makes the signing capabilities available only to the Modtx component and the verifying capabilities available only to the Signtx component. This means that signed data only flows one way and unsigned data only flows the other way.

When Modtx receives a raw Modbus message to be signed, it passes the message and message ID to the message signing function in the Crypto component. The Crypto component generates a hash-based message authentication code (HMAC) using the Beringer-Appel verified HMAC and SHA-256 implementations [START_REF] Appel | Verification of a cryptographic primitive: SHA-256[END_REF][START_REF] Beringer | Verified correctness and security of OpenSSL HMAC[END_REF] with a preshared key, then forwards the raw Modbus message, the generated HMAC and the message ID to the Signtx component. Alternatively, when Signtx receives a signed message from the untrusted network, it passes the message and the message ID to the signature verification function. The signature verification function separates the raw Modbus message from the received HMAC, generates its own HMAC and compares the two HMACs. It then passes the raw Modbus message, the message ID and the Crypto component decision (valid or invalid) to the Modtx component.

Modeling the Crypto component hides the cryptographic techniques behind a Boolean abstraction as the verification work for the target implementation of HMAC has been done elsewhere [START_REF] Appel | Verification of a cryptographic primitive: SHA-256[END_REF][START_REF] Beringer | Verified correctness and security of OpenSSL HMAC[END_REF]. The specification uses an HMAC comparison function that simply returns true or false regardless of the strings being compared. When checking the model, the TLA+ model checker expands the state space for both possibilities, ensuring that the safety or liveness properties are not violated regardless of the decision made by the Crypto component.

Message Signing Property

A macMessage is empty or contains a well-formed packet Invariant

The input and output of the signing function are different Invariant

A password does not change Invariant

A message that is received is eventually processed Liveness A message that is processed is eventually forwarded Liveness

Signature Verification Property

A password does not change Invariant

A message that is flagged as valid is, in fact, valid Invariant A message that is invalid is never flagged as valid Invariant A message that is received is eventually flagged as Liveness valid or invalid A message that is received is eventually forwarded Liveness

The message signing function has three invariants and two liveness checks (top half of Table 4). The buffer that holds the processed string to be forwarded, macMessage, is checked in all the invariants. The first invariant stipulates that macMessage is either empty or contains a well-formed packet. The second invariant stipulates that the information received and passed by the message signing function are different, demonstrating that processing has taken place. The third invariant stipulates that the password variable is never changed. The two liveness check ensure that a message that is received is eventually processed and forwarded.

The signature verification function has three invariants and two liveliness checks (bottom half of Table 4). As in the case of the message signing function, the first invariant stipulates that the password variable is never changed. The second invariant stipulates that a message marked as valid when it is forwarded to the Modtx component has a validated HMAC. The third invariant stipulates that an invalid message is never flagged as valid. The two liveness checks ensure that, if a message is received, then it is eventually flagged and forwarded to the Modtx component.

Discussion

An attacker who targets the network in which the bumper-in-the-wire device operates may attempt to forge messages, or tamper with or replay captured messages. Alternatively, the attacker may attempt to exploit the trust rela-tionship between the internal network and the device by assuming control and generating malicious traffic that originates from the device as described in [START_REF]Industrial Control Systems Cyber Emergency Response Team (ICS-CERT), Advisory (ICSA-12-231-01B), Sixnet Universal Protocol Undocumented Function Codes (Update B)[END_REF]. However, the device is immune to these types of attacks because invariants ensure that, regardless of the model state, only valid Modbus messages (whether encapsulated or not) can be printed. Further, if the assumptions described above hold, then the system would not accept messages that have been tampered with (i.e., messages that do not match the attached HMACs). A nonce is included in each encapsulated message to prevent replay attacks.

Restricting the model checking to a feasible state-space required a few tricks. The simplest incarnation of the model completed in roughly ten minutes, but the number of states extended to the tens of millions. Modeling each thread individually enabled around 10,000 states to be explored to verify the invariants and perform the liveness checks. Relying on the verification work applied to the seL4 component architecture enabled the component models to be kept separate while maintaining the queue-based message passing structure of the general model. While these strategies may change according to the project, researchers have shown that even larger projects can see benefits when the state space is restricted to a manageable size [START_REF] Azure | Azure Cosmos TLA+ specifications[END_REF][START_REF] Newcombe | Use of Formal Methods at Amazon Web Services[END_REF]

Conclusions

Industrial control network traffic is routinely checked for transmission errors, but limited security mechanisms are available for combating attacks that exploit industrial control protocols to target field devices. The bump-in-the-wire solution considered in this research is designed to be retrofitted on field devices to provide the needed security functionality. The TLA+ formal specification language in combination with the isolation guarantees provided by the seL4 microkernel are used to demonstrate that the bump-in-the-wire device provides the desired security and liveness properties. Indeed, the resulting machinechecked system correctly applies hash-based message authentication to verify the authenticity of incoming protocol messages while being resistant to attacks. In particular, the verified specification assures that only valid, authenticated Modbus packets flow across a field device, that a compromised component cannot break the security properties of adjacent components, that the device is not vulnerable to replay and spoofing attacks, and that the device is resilient to malformed and malicious traffic.

Future research will focus on formal proofs at the code level and a verified implementation targeting the seL4 microkernel. The modular design would be conducive to full formal verification because the components are limited in how they interact with other components (if they interact at all). The seL4 proof work provides the isolation and interprocess communications guarantees, facilitating a component-based architecture. The component-based architecture can be abstracted to a distributed system of critical decision points, which TLA+ excels at modeling and checking. Thus, the important next step is to move from a TLA+ specification to executable, verified C code. The verified C code could be incorporated in the CAmkES build and deployed in a native seL4 application.

Figure 1 .

 1 Figure 1. Typical industrial control system.

Figure 2 .

 2 Figure 2. CAmkES components.

Table 1 .

 1 Modbus ASCII protocol data unit.

	Start Address Function	Data	LRC	End
	":"	2 bytes	2 bytes	Up to 504 bytes 2 bytes "\r\n"

Table 2 .

 2 Desired system properties.

	System

Table 4 .

 4 Desired Crypto component properties.


Jason Staggs

Sujeet Shenoi

Securing Wireless Coprocessors from Attacks in the Internet of Things

Keywords: Wireless coprocessor, Internet of Things, intrusion prevention

de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

A Statista report [START_REF]Internet of Things (IoT) connected devices installed based worldwide from 2015 to 2025 (in billions)[END_REF] estimates that nearly 31 billion Internet of Things (IoT) devices will be in use by 2020. Consumer demand for smart devices has surged, launching a time-to-market race by manufacturers to release Internet of Things devices with rich features at affordable prices. Unfortunately, security has taken a back seat to features, significantly increasing the risks to devices, networks and users [START_REF] Krebs | Mirai botnet authors avoid jail time, Krebs on Security (krebs onsecurity.com[END_REF].

Further complicating matters are the diversity and complexity of wireless protocols and communications systems that interconnect Internet of Things devices [START_REF] Palattella | Standardized protocol stack for the Internet of (important) Things[END_REF]. Internet of Things devices use wireless coprocessors and protocols to support communications with smart devices and networks. These communica-tions coprocessors are normally separate microcontrollers that are independent of the main CPUs. The heterogeneity of wireless communications coprocessors and protocol stacks has inadvertently increased the attack surfaces of Internet of Things and mobile devices. The security problems associated with wireless communications coprocessors are also inherited by devices such as remote terminal units and programmable logic controllers that help operate critical infrastructure assets.

Previous research has demonstrated that wireless communications coprocessors lack rudimentary security measures to combat attacks, especially data execution prevention (DEP), address space layout randomization (ASLR) and basic memory protections [START_REF] Artenstein | Broadpwn: Remotely compromising Android and iOS via a bug in Broadcom's Wi-Fi chipsets[END_REF][START_REF] Blanco | One firmware to monitor 'em all[END_REF][START_REF]iPhone Dev Team, Purplesn0w, The iPhone Wiki[END_REF][START_REF] Weinmann | All your baseband are belong to us[END_REF][START_REF] Weinmann | Baseband attacks: Remote exploitation of memory corruptions in cellular protocol stacks[END_REF]. Although it is important to consider attacks that target the main CPUs of devices, it is equally imperative to consider attacks that focus on wireless network coprocessors. Internet of Things and mobile devices must be engineered to be more resilient to attacks that target communications coprocessing units, especially if the security threats posed by insecure devices that plague the Internet [START_REF] Krebs | Mirai botnet authors avoid jail time, Krebs on Security (krebs onsecurity.com[END_REF] and some operational technology environments are to be reduced.

This work focuses on mitigating attacks by applying security defenses to a specific type of wireless communications coprocessor -the cellular baseband processor. Baseband processors, also known as cellular modems, are present in all mobile phones and in many Internet of Things devices and industrial control systems that require cellular wide-area networking connections to the Internet [START_REF] Shaw | Cybersecuriy for SCADA Systems[END_REF]. These independent systems provide direct, unfiltered radio access to public cellular GSM, UMTS and LTE networks, and are attractive targets for attackers who seek to intercept, modify, fabricate or interrupt communications.

Despite concerns about attacks on communications coprocessors, relatively few attempts have been made to secure their external interfaces [START_REF] Mulliner | Mitigating signaling based attacks on smartphones[END_REF]. This work addresses the gap by mitigating exploitation attempts from the application processor (main CPU) that leverage malformed or unauthorized vendorspecific serial AT commands to target the baseband processor. Such attacks are commonly employed to unlock cell phones, but they can be repurposed to perpetrate nefarious baseband system compromises [START_REF]iPhone Dev Team, ultrasn0w, The iPhone Wiki[END_REF][START_REF]iPhone Dev Team, Purplesn0w, The iPhone Wiki[END_REF][START_REF] Tian | ATtention spanned: Comprehensive vulnerability analysis of AT commands within the Android ecosystem[END_REF].

This chapter describes a proof-of-concept application-processor-interfacebased AT command intrusion prevention system that combats exploitation attempts against the baseband processor. The intrusion prevention system relies on rules (signatures) based on AT command syntax and semantics. The signatures help detect and prevent malicious AT commands and payloads (parameters) from being sent to the baseband processor. The proof-of-concept system incorporates a Raspberry Pi 3 hardware platform for main CPU emulation and a SIM900 GSM module (baseband processor). Empirical testing reveals that the system combats baseband processor attacks from the application processor. Although the system employs hobbyist hardware, the underlying techniques can be applied to Internet of Things and mobile devices by making slight modifications to their operating systems or by adding a dedicated security coprocessor that inspects input/output messages on the data bus.

Security of Communications Stacks

The vast majority of Internet of Things and mobile devices incorporate wireless communications processors for wide-area networking and personal area networking radio needs. These independent coprocessors facilitate communications between other smart devices, sensors, motors, relays and supporting telecommunications infrastructure assets (e.g., cellular base stations). Communications technologies such as 802.15.4 (i.e., Zigbee and WirelessHART), 802.11 (i.e., Wi-Fi), Bluetooth and GSM/UMTS/LTE have emerged over the years and are now widely integrated in Internet of Things devices. In many cases, the wireless chipsets operate independently of the main CPUs and, therefore, have their own attack surfaces [START_REF] Lonzetta | Security vulnerabilities in Bluetooth technology as used in IoT[END_REF].

Previous research has demonstrated that wireless communications coprocessors lack basic security mechanisms. Although it is important to consider attacks that target the main CPUs of devices, it is imperative that future Internet of Things and mobile devices are engineered to be resilient to attacks that target communications coprocessors. Researchers have identified a number of security problems and vulnerabilities in wireless coprocessors and protocol stacks [START_REF] Artenstein | Broadpwn: Remotely compromising Android and iOS via a bug in Broadcom's Wi-Fi chipsets[END_REF][START_REF] Blanco | One firmware to monitor 'em all[END_REF][START_REF] Weinmann | All your baseband are belong to us[END_REF][START_REF] Weinmann | Baseband attacks: Remote exploitation of memory corruptions in cellular protocol stacks[END_REF]. Some attacks target vulnerabilities in coprocessor firmware while others target kernel modules or libraries used by the operating systems of the main CPUs to interact with wireless subsystems on the devices [START_REF] Seri | Exploiting BlueBorne in Linux-based IoT devices[END_REF].

In particular, several vulnerabilities have been identified in Broadcom Wi-Fi chipsets. Beniamini [START_REF] Beniamini | Over the Air: Exploiting Broadcom's Wi-Fi Stack (Part 1), Project Zero Team, Google[END_REF][START_REF] Beniamini | Over the Air: Exploiting Broadcom's Wi-Fi Stack (Part 2), Project Zero Team, Google[END_REF][START_REF] Beniamini | Exploiting the Wi-Fi Stack on Apple Devices, Project Zero Team, Google[END_REF] demonstrated heap and stack overflow vulnerabilities that lead to remote code execution (RCE) on a common Broadcom Wi-Fi chipset. These vulnerabilities stem from inadequate data field checking by the Wi-Fi coprocessor unit when processing certain 802.11r-2008 (fast BSS transition) authentication frames. Building on Beniamini's work, Artenstein [START_REF] Artenstein | Broadpwn: Remotely compromising Android and iOS via a bug in Broadcom's Wi-Fi chipsets[END_REF] weaponized the exploits by incorporating them in a propagating worm that could target other Wi-Fi chipsets. Meanwhile, Seri and Livne [START_REF] Seri | Exploiting BlueBorne in Linux-based IoT devices[END_REF] have developed a new attack called "BlueBorne" that targets Bluetooth implementations in operating systems used by billions of Internet of Things and mobile devices. Arguably, the most terrifying wireless chipset attacks involve the exploitation of cellular baseband processors.

Cellular baseband stack exploits have been discussed for nearly a decade [START_REF] Golde | Breaking band: Reverse engineering and exploiting the Shannon baseband[END_REF][START_REF] Weinmann | All your baseband are belong to us[END_REF][START_REF] Weinmann | Baseband attacks: Remote exploitation of memory corruptions in cellular protocol stacks[END_REF]. The exploitation of communications coprocessors presents an existential threat to the devices they support, and by extension, the physical environments in which they are used (e.g., industrial Internet of Things and industrial control systems). Novel ideas, techniques and mechanisms are needed to counter the threats to frail and insecure communications coprocessors.

This chapter presents an approach for retrofitting security in one of the external interfaces used by baseband processors in order to mitigate hostile activity originating from the main CPU. Admittedly, this is not a perfect solution to the overall problem, but the approach is useful when security controls have to be implemented in current mobile phones and legacy industrial control systems.

Main CPU

Cellular

Cellular Baseband Processors

Baseband processors -also called cellular modems -are present in Internet of Things devices and mobile phones that require wide-area networking connections to the Internet and other cellular functions. The independent baseband systems, which provide direct, unfiltered access to public cellular networks, are prime targets for attackers interested in intercepting, modifying, fabricating or blocking voice, text, data and signaling traffic.

Symbiotic System of Systems

Internet of Things devices and modern mobile phones incorporate supporting microcontrollers and subsystems, each serving a dedicated and crucial role. These subsystems are interconnected directly or indirectly over a common data bus, enabling the smart device to provide rich interactions with the external environment via sensors (e.g., camera, microphone, gyroscope and accelerometer) and radios. Because the microcontrollers operate independently of the main CPUs, they have their own firmware that is usually stored in read-only memory (ROM).

Figure 1 presents a logical view of the peripheral systems in a smartphone. Examples include the GPS, camera, battery, Wi-Fi, near-field communications (NFC), Bluetooth and cellular baseband systems. Although the systems are viewed as being independent, it is important to note that some of these systems are often encapsulated in a single integrated circuit called a "system on a chip" (SoC). The systems may be housed in a single integrated circuit package, but a common input/output interface is still required for them to exchange commands and data (e.g., UART, CAN, SPI, I2C, USB or shared memory). Just like any other embedded system, each encapsulated system has its own volatile memory (RAM) and non-volatile memory (flash), along with various peripherals. This architecture enables the main CPU to focus on its operating system and user applications, while relying on the independent supporting systems to handle other tasks and provide external data upon request via hardware interrupts. It is common for the tasks performed by these systems to be subject to stringent synchronization and timing constraints, as in the case of a cellular protocol stack that runs on a baseband processor.

The two main components of cellular-enabled Internet of Things and mobile devices are the application processor and baseband processor. Figure 2 shows the relationship between the two processors [START_REF] Drake | Android Hacker's Handbook[END_REF].

The application processor system houses the main CPU and operating system (e.g., Linux, Android, Windows IoT or iOS). User applications and display interfaces execute on the application processor.

The baseband processor system serves as the cellular modem that independently handles cellular network communications between the mobile device and cell towers, including signaling for radio resource management, mobility management, connection management, voice calls, SMS text messages and cellular data. Like the application processor system, the baseband processor system contains dedicated hardware peripherals such as RAM, flash memory and digital signal processor, and provides direct access to the cell phone speaker and microphone [START_REF] Sauter | From GSM to LTE: An Introduction to Mobile Networks and Mobile Broadband[END_REF]. The baseband processor system is analogous to a dial-up modem or Ethernet controller in a personal computer, providing layer 1 modulation and demodulation of carrier signals to encode and decode information over dedicated cellular links.

Baseband Processor

Application Processor RAM (shared) IPC IPC Figure 3. Shared memory architecture.

Baseband Firmware

In order to manage hardware resources and perform cellular modem tasks, the baseband processor typically runs a bootloader that initializes the hardware and loads a real-time operating system (RTOS) into memory [START_REF] Welte | Anatomy of Contemporary GSM Cellphone Hardware[END_REF]. The realtime operating system executes tasks for the entire cellular network stack (e.g., GSM, UMTS and LTE) [START_REF] Miras | The baseband playground[END_REF][START_REF] Weinmann | Baseband attacks: Remote exploitation of memory corruptions in cellular protocol stacks[END_REF]. The tasks, which are engineered to provide reliable signal connectivity to carrier networks, generally have the requirement of minimal power consumption during operation.

Although baseband system codebases have been updated over the years to accommodate the latest cellular protocol specifications, significant portions of early GSM, UMTS and LTE codebases are still used in modern baseband stacks. Implementing the 3GPP cellular protocol specifications in software is a complex endeavor that can be ambiguous in some instances. Unfortunately, the messages used by cellular protocol stacks sometimes contain high concentrations of variable length fields that are not handled properly and, thus, can be targeted by fuzzing and vulnerability discovery activities. These factors create a perfect storm for exploiting baseband systems [START_REF] Hond | Fuzzing the GSM Protocol[END_REF][START_REF] Weinmann | Baseband attacks: Remote exploitation of memory corruptions in cellular protocol stacks[END_REF].

It is important to note that cellular baseband processors are not limited to mobile phones. In fact, the processors are commonly found in Internet of Things devices such as vehicle telematics units, automated teller machines and smart meters used in electricity, gas and water distribution infrastructures. All these devices typically require low bandwidth connectivity to transmit data.

Baseband Architectures

Command and data exchange between the application and baseband processors depend on the device architecture. The two architectures are: (i) shared memory architecture; and (ii) independent memory architecture. Figures 3 and4 illustrate the two architectures [START_REF] Drake | Android Hacker's Handbook[END_REF][START_REF] Weinmann | All your baseband are belong to us[END_REF].

In the shared memory architecture, the application processor and baseband processor address spaces are mapped to the same physical RAM [START_REF] Weinmann | All your baseband are belong to us[END_REF]. In this case, a form of interprocess communications is employed to exchange information between baseband and application processes.

The independent memory architecture is more commonly used in Internet of Things devices and modern phones. The architecture requires a dedicated data bus between the application and baseband processors to facilitate communications. Common data bus communications interfaces are UART, SPI, I2C and USB.

Serial Communications Protocols

Baseband processor command and control protocols vary from device to device. The protocols are used to instruct the baseband to execute cellular functions such as making a call and sending data. The protocols are also used to send information back to the application processor (e.g., notification of an incoming call, SMS or data). Common protocols include standard GSM AT commands [START_REF]European Telecommunications Standards Institute, Digital Cellular Telecommunications System (Phase 2+), AT Command Set for GSM Mobile Equipment (ME), GSM 07.07[END_REF][START_REF] Sanglard | Tracing the Baseband: Part 1[END_REF] and proprietary vendor-specific command protocols [START_REF] Delugre | Reverse engineering a Qualcomm baseband[END_REF]. GSM AT commands are similar to the Hayes AT commands used by old dial-up modems [START_REF]History of Computers, The modem of Dennis Hayes and Dale Heatherington (history-computer[END_REF]. Some baseband processor vendors incorporate additional proprietary commands for extended functionality and debugging; in some instances, they provide backdoors to the application processor [START_REF] Kocialkowski | Samsung Galaxy Back-Door[END_REF][START_REF] Tian | ATtention spanned: Comprehensive vulnerability analysis of AT commands within the Android ecosystem[END_REF]. Additionally, the commands are usually sent in the clear and are not authenticated.

Securing the Baseband Processor

Despite the increased scrutiny leveled on communications coprocessors as potential attack targets, few attempts have been made to secure their external interfaces [START_REF]iPhone Dev Team, ultrasn0w, The iPhone Wiki[END_REF]. The application processor interface and the air-interface expose the baseband processor to untrusted data and, thus, a number of external threats (Figure 5).

Baseband firmware reverse engineering is required in order to fully appreciate the baseband system security issues. The mobile phone unlocking communities are the most advanced at understanding the complexities involved in baseband processor firmware reverse engineering and exploitation. The application processor interface is routinely leveraged by mobile phone unlocking enthusiasts to exploit vulnerabilities in baseband processors to unlock phones for use in other carrier networks. Although such attacks generally require root access to the application processor (e.g., by jailbreaking or rooting), the application processor has a rich attack surface of its own that could be used to indirectly target the baseband processor.

Tian et al. [START_REF] Tian | ATtention spanned: Comprehensive vulnerability analysis of AT commands within the Android ecosystem[END_REF] describe a methodology and analysis framework for identifying and assessing vendor-specific AT commands that are injected via the USB modem interfaces of Android devices. They discovered hundreds of commands that can be used to bypass screen locks, enable developer debugging tools and perform firmware updates. Additionally, they discovered other vendor-specific AT commands that could be used to probe and potentially manipulate baseband processors. Over-the-air remote code execution attacks against the airinterfaces of baseband processors are also a concern because they could be leveraged to compromise the baseband processors remotely.

Some baseband processors incorporate a dedicated JTAG interface that can be used to help reverse engineer and/or read/write to the flash memory of the processor. JTAG is a hardware debugging interface that is commonly used by manufacturers for device testing and verification. Although this interface could provide substantial low-level access to the code, data and operational context of a baseband processor, it is outside the scope of this work. Instead, this section investigates techniques that could be used to retrofit security around the baseband processor to mitigate external attacks from the application processor interface.

Retrofitting Security

Embedded systems typically have design requirements that stress reliability and efficiency. This is especially true for embedded systems with strict power constraints and those that support human or physical processes (e.g., cell phones, programmable logic controllers and pacemakers) [START_REF] Moe | hackers. Break my heart[END_REF]. Unfortunately, security usually comes in second after performance requirements and is often considered only after a serious incident impacts consumers. Reactive approaches to addressing security problems are rarely robust and often have serious ramifications [START_REF] Krebs | Mirai botnet authors avoid jail time, Krebs on Security (krebs onsecurity.com[END_REF]. As a result, proactive measures that incorporate security engineering best practices must be considered early in system design and definitely before system integration.

The longevity of embedded system deployments (e.g., industrial control systems) and the lack of regular firmware updates make them ideal targets for adversaries. The ubiquity of insecure communications interfaces and protocols contributes to inherent vulnerabilities in embedded systems that persist over their lifespans -these are collectively referred to as "forever days."

Retrofitting security in an insecure external communications interface of an embedded system is an active research challenge. Bump-in-the-wire solutions that secure unencrypted IP-based industrial control system protocols such as Modbus/TCP and DNP3 have been developed [START_REF] Tsang | YASIR: A low-latency, high-integrity security retrofit for legacy SCADA systems[END_REF]. Additionally, specialized firewalls have been deployed to perform rigorous message filtering across trust domains in industrial control system environments [START_REF] Nivethan | A Linux-based firewall for the DNP3 protocol[END_REF][START_REF]Tofino Firewall LSM[END_REF].

In the case of Internet of Things and mobile devices, the interface between the application and baseband processors is fundamentally insecure. The interface transports serial character streams of commands and data that initiate cellular processes in the devices [START_REF] Sanglard | Tracing the Baseband: Part 1[END_REF][START_REF] Sanglard | Tracing the Baseband: Part 2[END_REF]. Unfortunately, this interface enables malware executing on the application processor to target the baseband processor with malicious commands and data.

AT Command Filtering

Mulliner et al. [START_REF] Mulliner | Mitigating signaling based attacks on smartphones[END_REF] have developed a "virtual modem" protection mechanism that mitigates malicious injections of cellular signaling traffic from mobile phones. The virtual modem mediates signaling traffic between the application processor and baseband processor. This independent system intercepts and inspects AT commands before forwarding them to the baseband processor.

The virtual modem solution incorporates an AT command filter that enforces a security policy on messages destined for the baseband processor. The policy specifies temporal thresholds on the frequencies of transmitted AT commands. The enforcement of the strict policy on AT commands that initiate critical cellular operations mitigates denial-of-service attacks. However, this solution does not address attacks on the baseband processor itself.

Baseband Processor Exploitation

The mobile phone unlocking communities have for years focused on understanding how proprietary baseband processors work in order to bypass network carrier locking restrictions [START_REF]iPhone Dev Team, ultrasn0w, The iPhone Wiki[END_REF]. The Apple iOS and Android communities have acquired substantial expertise in reverse engineering, vulnerability analysis and exploit development for targeting baseband processor firmware. Their focus is on baseband processor exploitation from the perspective of the application processor interface, not the air-interface.

Baseband processor exploitation over the air-interface generally occurs by leveraging remote code execution or denial-of-service vulnerabilities in frail cellular protocol stack implementations. The vulnerabilities are triggered by sending specially-crafted cellular messages (e.g., signaling, voice or data) to the baseband processor. These messages are usually malformed and are constructed to take advantage of inadequate checking of GSM/UMTS message field lengths (e.g., resulting in buffer/heap overflows) or they employ improper variable data types (e.g., resulting in integer overflows) [START_REF] Weinmann | All your baseband are belong to us[END_REF][START_REF] Weinmann | Baseband attacks: Remote exploitation of memory corruptions in cellular protocol stacks[END_REF]. In contrast, baseband exploitation via the application processor interface typically involves sending crafted AT commands that trigger remote code execution vulnerabilities in the AT command handler code of the baseband processor.

Modern phones support hundreds of AT commands for initiating cellular activities and providing vendor-specific features. This has created large attack surfaces for the baseband and application processors that can be leveraged by attackers to rewrite firmware, bypass security mechanisms, exfiltrate sensitive device data, unlock screens and inject touch events [START_REF] Tian | ATtention spanned: Comprehensive vulnerability analysis of AT commands within the Android ecosystem[END_REF].

The approach adopted in this research is to identify suspicious AT commands and create the associated signatures. These AT command signatures are employed in real time to thwart exploitation attempts against the baseband processor.

AT Command Exploitation Methodology

The iOS and Android unlocking/jailbreaking communities are great sources for information about baseband processor exploitation. This information can also be used to assist in developing reactive and proactive security mechanisms that detect and mitigate attacks against the baseband processor. This work has leveraged the theiphonewiki.com community resources to understand baseband processor exploitation from the application processor. It has also drawn on vulnerability and exploit information from theiphonewiki.com to develop mitigation techniques.

The first step in unlocking a phone is to understand how and where network carrier locking is implemented. In most cases, this is handled by the baseband processor. Traditionally, a security researcher who intends to unlock a phone unpacks and reverse engineers the baseband firmware of the target phone. Next, the researcher identifies sections of code and data in the firmware where the carrier lock logic is implemented.

A method for remote code execution is then needed to patch the memory of the targeted baseband processor. This can be accomplished by analyzing the AT command interface handler for software vulnerabilities that provide control of the system (e.g., memory corruption). The vulnerabilities are normally triggered (exploited) using anomalous AT commands sent from the application processor. The anomalous AT commands, which are usually valid per specification, are constructed to exploit vulnerabilities in the AT command handler to gain control over the program counter of the baseband processor. In some cases, the AT commands may contain shellcode that is eventually executed in order to unlock the phone. Common memory corruption vulnerabilities that are routinely identified and exploited include stack-and heap-based buffer overflows [START_REF] One | Smashing the stack for fun and profit[END_REF][START_REF]iPhone Dev Team, ultrasn0w, The iPhone Wiki[END_REF].

Figure 6 shows a proof-of-concept stack overflow exploit employed by the Purplesn0w unlock to trigger an AT command vulnerability in the iPhone 3GS X-Gold 608 baseband processor [START_REF]iPhone Dev Team, Purplesn0w, The iPhone Wiki[END_REF]. In the example, the second parameter of at+xlog=1,"jjjjjjjjjjjjjjjjjjjjjjjjjjjj44445555PPPP" j's = junk padding R4 = 4 R5 = 5 PC = P the +xlog AT extended command is crafted to gain control of the program counter of the baseband processor.

AT Command Intrusion Prevention System

Data entering the baseband processor from an external source should be considered to be untrusted until it is vetted for signs of malicious behavior. A proof-of-concept AT command intrusion prevention system was developed to mitigate exploitation or dynamic vulnerability discovery attempts against the baseband processor that originate from the application processor interface. The intrusion prevention system enables users to define rules (signatures) based on the AT command syntax and semantics. The signatures are used to detect and prevent malicious AT commands and payloads (parameters) from being sent to the baseband processor. Signatures are also specified to detect and prevent fuzzing attempts and unauthorized uses of vendor-specific AT commands.

AT Command Syntax

The Hayes AT and GSM AT command sets are character-based messaging protocols (strings) that are commonly used by application processors to instruct baseband processors to perform cellular operations. Cellular routines for voice, SMS and data are invoked by AT commands to instruct baseband processors to perform the relevant functions. The AT command specifications cover hundreds of commands. This work focuses on application processor interface protocols that use standard AT and GSM AT commands, as well as proprietary vendorspecific AT commands [START_REF] Tian | ATtention spanned: Comprehensive vulnerability analysis of AT commands within the Android ecosystem[END_REF]. Other types of proprietary messaging protocols exist [START_REF] Delugre | Reverse engineering a Qualcomm baseband[END_REF]; however, the rigorous treatment of these protocols is the subject of future research.

Several categories of AT command messages, each with its own syntax, have been specified [START_REF]European Telecommunications Standards Institute, Digital Cellular Telecommunications System (Phase 2+), AT Command Set for GSM Mobile Equipment (ME), GSM 07.07[END_REF][START_REF]AT Commands Set, SIM900 ATC V1.00[END_REF]. The three AT command categories considered in this research are basic, extended and s-parameter commands.

Basic Commands: Basic commands have the structure AT<x><n> or

AT&<x><n> where <x> is a command and <n> denotes the command parameters.

Extended Commands: Extended commands have the structure AT+<x> <n> or AT%<x><n> where <x> is a command and <n> denotes the command parameters.

operating system). In general, AT command inspection may be performed in three ways, each requiring different levels of device access and intrusiveness: (i) adding an additional security coprocessor tasked with moderating AT commands; (ii) kernel-level modifications; and (iii) user-level library preloading [START_REF] Sanglard | Tracing the Baseband: Part 1[END_REF][START_REF] Sanglard | Tracing the Baseband: Part 2[END_REF]. This research leveraged the library pre-loading technique for AT command inspection because of its ease of implementation.

In order to simulate the cellular functionality of a malicious application or rooted phone, a test application was written for the Raspberry Pi 3 to send arbitrary and malicious AT commands to the SIM900 GSM module. The application sends AT commands to the SIM900 GSM module by creating a file descriptor to the serial device /dev/uart and calling the libc write() function to write a stream of characters to the serial device.

The write() function is hooked to inspect AT commands before being written to the serial device. An easy way to hook a library function in Linux is to use the LD PRELOAD environment variable [START_REF] Sanglard | Tracing the Baseband: Part 1[END_REF][START_REF] Sanglard | Tracing the Baseband: Part 2[END_REF], which enables a designated shared library to be loaded before any other shared libraries. This precedence technique is leveraged to overwrite stock shared library symbols in order to define an alternative version of write(). This method gains control of the data content passed to the baseband processor.

After hooking the write() function with LD PRELOAD, control is passed to the intrusion prevention code that checks the AT commands and data. Only verified write() function calls passed with a file descriptor to the baseband processor (UART device) are processed further. If a write() call does not contain a file descriptor that points to a valid serial device, then the function calls the regular libc version of write().

If the altered version of write() is invoked, then the buffer containing the message is parsed by the intrusion prevention system and matched against the predefined rules (signatures). If a rule is triggered by a particular AT command, then the command is dropped and the function simply returns to the calling function the number of bytes that were supposed to be written to the device. This ensures that the intrusion prevention logic is transparent to the underlying application and that the application is unaware that the AT command has been dropped.

Alternatively, if the AT command does not trigger on a rule, it is passed on and written to the UART interface for serial transmission to the baseband processor. The inspection system thus moderates potentially malevolent commands and data sent over an insecure, albeit trusted, serial interface.

Figure 8 illustrates the application-processor-based AT command intrusion prevention process used in the proof-of-concept implementation. The AT command parser parses the command contained in the buffer that is passed to the write() call. In addition to performing syntactic checks, an appropriate data structure is created for the AT command (e.g., basic, extended or s-parameter). The data structure, which contains granular attributes that apply to the AT command, is employed when applying the rule-based logic.

Intrusion Prevention System

The rule parser reads in the rules that are defined in an external configuration file. A rule has the syntax: <operator> <command><parameter(s)>. Note that the parameters are operator specific.

Four basic operators are employed by the intrusion prevention system:

Length: This operator provides the length of an AT command parameter. It is useful for flagging AT commands with abnormal parameter lengths (e.g., used to induce stack-based buffer overflows, where the padding size of the exploit is known to be at least a certain length).

-Example 1: length +xlog 25 blocks the AT +xlog command when the parameter length is exactly 25 characters.

-Example 2: length +xlog >= 25 blocks the AT +xlog command when the parameter length is greater than or equal to 25 characters.

Match:

This operator matches a substring against the parameters of a specific AT command or all AT commands. If a match occurs, the AT command is blocked. The operator is useful for catching script kiddies or commonly-used shellcode snippets (e.g., used in phone unlocking attempts).

-Example 1: match "baddata" blocks all commands containing the string "baddata" in their parameters.

-Example 2: match +xapp "\0xDE\0xAD\0xBE\0xEF" blocks +xapp commands containing the shellcode "\0xDE\0xAD\0xBE\0xEF" as a parameter.

Msg Sequence: This operator triggers an alert when a contiguous sequence of AT commands is encountered; the commands are also blocked.

It is useful for establishing context-based rules where a single AT command may not be malicious, but a series of commands in the specified order could be malicious.

-Example 1: msg sequence +xlog +xlog triggers an alert on backto-back occurrences of the +xlog command; the commands are also blocked.

Block: This operator adds an AT command to the blacklist, which causes the command to be dropped as soon as it is encountered. It is useful for blocking vendor-specific AT commands that could be abused by attackers [START_REF] Tian | ATtention spanned: Comprehensive vulnerability analysis of AT commands within the Android ecosystem[END_REF].

-Example 1: block at%imei= prevents the IMEI of a phone from being changed.

-Example 2: block at+fus? prevents a phone from going into the firmware download mode.

-Example 3: block at+xabbtrace prevents the baseband trace configuration from being returned.

Experimental Analysis and Testing

The application-processor-based AT command intrusion prevention system was subjected to several tests to verify that it could detect and prevent malicious AT command exploitation attempts on the baseband processor without degrading device performance. Specifically, the subscriber should not experience noticeable delays and should be able to use the device as intended (e.g., to make/receive phone calls and send/receive SMS texts and data). Several malicious AT commands were used in the tests, including some that target the X-Gold 608 and 618 baseband processors in older iPhones. These malicious AT commands were selected because of their documentation and use in iPhone baseband unlocks.

Another consideration was to appropriately tune the AT command signatures to minimize false positives and false negatives. Tuning requires the profiling of messages to establish baselines. Signatures that are too general increase the false positive rate and block valid AT commands. Signatures that are too specific increase the false negative rate and fail to block malicious AT commands. Tuning the signatures was determined to be as much art as a science; a thorough treatment of AT command signature tuning is a topic for future work.

Malicious AT commands used in the tests were obtained from Tian et al. [START_REF] Tian | ATtention spanned: Comprehensive vulnerability analysis of AT commands within the Android ecosystem[END_REF] and theiphonewiki.com. During the tests, regular cellular communications procedures were performed, including sending and receiving voice calls, SMS messages and streaming data while periodically injecting malicious AT commands.

The following tests were conducted:

Test 1: Injection of a single malicious AT command during a two-minute voice call.

Test 2: Injection of a malicious AT command every 100 ms during a two-minute voice call.

Test 3: Injection of a single malicious AT command while the baseband was not being used (i.e., in the standby mode).

Test 4: Injection of a malicious AT command every 100 ms while the baseband was not being used (i.e., in the standby mode).

Test 5: Injection of a malicious AT command during a streaming data session.

Test 6: Injection of a malicious AT command every 100 ms during a streaming data session.

Table 1 shows the test results along with the rules used to detect and block malicious AT commands. Five malicious or risky AT commands were used in the tests, all of which were successfully detected by the intrusion prevention system. The intrusion prevention functionality did not noticeably impact the normal use of the cellular modem (e.g., making and receiving calls, and sending and receiving SMS messages and packetized data). Additionally, no false positives were observed during tests. Future work will pursue a rigorous testing regimen that considers all the cellular functionality under real-world conditions.

Conclusions

Wireless communications coprocessors provide wide-area and personal-area networking capabilities to Internet of Things and mobile devices. These coprocessors have been the targets of exploitation research in recent years. In particular, the baseband processors, which are responsible for cellular communications, are attractive targets for adversaries interested in intercepting, modifying, interrupting or fabricating voice, text, data and signaling traffic.

This research has made key contributions to securing baseband processors from exploitation attempts by hostile applications that execute on the application processor. Retrofitting an AT command intrusion prevention system between the application processor and baseband processor mitigates the negative effects of malicious AT commands. Because the intrusion prevention system is vendor agnostic and focuses on analyzing text-based AT commands, the approach is easily implemented to secure baseband processors produced by diverse manufacturers.

Future research will focus on integrating the AT command intrusion prevention technique in Internet of Things and mobile device platforms and operating systems. Additionally, techniques for retrofitting security mechanisms in other vulnerable wireless chipsets will be explored. Finally, efforts will focus on employing cryptographically-sound techniques for firmware attestation to combat threats ranging from unauthorized surveillance to insidious system compromises.

Figure 1 .

 1 Figure 1. System of systems in a smartphone.

Figure 2 .

 2 Figure 2. Relationship between the application processor and baseband processor.

Figure 4 .

 4 Figure 4. Independent memory architecture.

Figure 5 .

 5 Figure 5. External input/output interfaces to the baseband processor.

Figure 6 .

 6 Figure 6. iPhone 3GS Purplesn0w AT command exploit.

Figure 8 .

 8 Figure 8. Application-processor-based AT command intrusion prevention system.

Baseband Processor RAM Flash DSP Mic RTOS GSM/UMTS/LTE UART RAM Flash Display Android/iOS Apps Anti-Virus Application Processor (Main CPU) Kernel UART Serial AT Commands

Table 1 .

 1 Malicious AT command test cases. ...............CONTINUED................... 20xx"

	AT Command	IPS Rule	Detected
	at+xlog=1, "jjjjjjjjjjjjjjjjjjjjjjjjjjjj44445555PPPP"	length +xlog >= 30	Yes
	at+xapp="aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa	length +xapp >= 50	Yes
	aaaa4444555566667777PPPP"
	at%IMEI="490154203237518"	block at%imei=	Yes
	at+fns="00000000000000000000000000000000000000	length +fns >=1024	Yes
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000000000000000000000000000
	0000000000000000000000111111222233334444555566
	66677"
	at+stkprof=1,"064a541c044b1878222803d010700132	match "\x32\x0F\x27"	Yes
	0133f8e720470000bf9f154000170100546e56402000000
	05c130100266e5640ddddddddeeeeeeeeb890512000000
	0001010101020202020611301000c000000";"\x10\x32
	\x0F\x27\xBA\x43 \x17\x1C\x0E\xA4\x0B\xA5
	\x01\x35\x21\x78\x78\x29\x0C\xD0\xA8\x47
	\x0B\x01\x61\x78\xA8\x47\xC0\x46 \xC0\x46
	\xC0\x46\xC0\x46\xC9\x18\x11\x70 \x02\x34\x01
	\x32\xEF\xE7\xC0\x46\xC0\x46 \x01\x37\x38
	\x47\x30\x30\x41\x29\x01\xDA 09pG79pG02480
	3A1013101601FBD00004C711140F0B51C4B8026
	8BB03601188008911A4C301CA04700250990
	...

The application-processor-based AT command intrusion prevention system has three components: (i) AT command parser; (ii) rule parser; and (iii) intrusion detection/prevention engine.

S-Parameter Commands: S-parameter commands have the structure

ATS<n>=<m> where <n> is the index of the s-register to be set and <m> is the value to be assigned.

Design and Implementation

A SIM900 GSM module and a Raspberry Pi 3 hardware platform running a Linux Debian operating system (Raspbian) were selected to develop the proofof-concept AT command intrusion prevention system (Figure 7). The SIM900 GSM module was selected as the baseband processor because of its wide support and availability of documentation. The flexibility provided by the Raspberry Pi was leveraged to program it to emulate application processor functionality. The GSM module was connected to the GPIO pins of the Raspberry Pi to facilitate serial UART communications. OpenBTS was used as the test GSM network.

A method is needed to conduct real-time passive analysis of AT commands in transit to the baseband processor. Monitoring the transmission of AT commands requires an understanding of the dataflow from the source (application processor operating system) to the destination (baseband processor real-time