No Arabic abstract
Internet of Things (IoT) applications drive the behavior of IoT deployments according to installed sensors and actuators. It has recently been shown that IoT deployments are vulnerable to physical interactions, caused by design flaws or malicious intent, that can have severe physical consequences. Yet, extant approaches to securing IoT do not translate the app source code into its physical behavior to evaluate physical interactions. Thus, IoT consumers and markets do not possess the capability to assess the safety and security risks these interactions present. In this paper, we introduce the IoTSeer security service for IoT deployments, which uncovers undesired states caused by physical interactions. IoTSeer operates in four phases (1) translation of each actuation command and sensor event in an app source code into a hybrid I/O automaton that defines an apps physical behavior, (2) combining apps in a novel composite automaton that represents the joint physical behavior of interacting apps, (3) applying grid-based testing and falsification to validate whether an IoT deployment conforms to desired physical interaction policies, and (4) identification of the root cause of policy violations and proposing patches that guide users to prevent them. We use IoTSeer in an actual house with 13 actuators and six sensors with 37 apps and demonstrate its effectiveness and performance.
We uncover privacy vulnerabilities in the ICAO 9303 standard implemented by ePassports worldwide. These vulnerabilities, confirmed by ICAO, enable an ePassport holder who recently passed through a checkpoint to be reidentified without opening their ePassport. This paper explains how bisimilarity was used to discover these vulnerabilities, which exploit the BAC protocol - the original ICAO 9303 standard ePassport authentication protocol - and remains valid for the PACE protocol, which improves on the security of BAC in the latest ICAO 9303 standards. In order to tackle such bisimilarity problems, we develop here a chain of methods for the applied $pi$-calculus including a symbolic under-approximation of bisimilarity, called open bisimilarity, and a modal logic, called classical FM, for describing and certifying attacks. Evidence is provided to argue for a new scheme for specifying such unlinkability problems that more accurately reflects the capabilities of an attacker.
Internet of Things (IoT) consists of a large number of devices connected through a network, which exchange a high volume of data, thereby posing new security, privacy, and trust issues. One way to address these issues is ensuring data confidentiality using lightweight encryption algorithms for IoT protocols. However, the design and implementation of such protocols is an error-prone task; flaws in the implementation can lead to devastating security vulnerabilities. Here we propose a new verification approach named Encryption-BMC and Fuzzing (EBF), which combines Bounded Model Checking (BMC) and Fuzzing techniques to check for security vulnerabilities that arise from concurrent implementations of cyrptographic protocols, which include data race, thread leak, arithmetic overflow, and memory safety. EBF models IoT protocols as a client and server using POSIX threads, thereby simulating both entities communication. It also employs static and dynamic verification to cover the systems state-space exhaustively. We evaluate EBF against three benchmarks. First, we use the concurrency benchmark from SV-COMP and show that it outperforms other state-of-the-art tools such as ESBMC, AFL, Lazy-CSeq, and TSAN with respect to bug finding. Second, we evaluate an open-source implementation called WolfMQTT. It is an MQTT client implementation that uses the WolfSSL library. We show that tool detects a data race bug, which other approaches are unable to find. Third, to show the effectiveness of EBF, we replicate some known vulnerabilities in OpenSSL and CyaSSL (lately WolfSSL) libraries. EBF can detect the bugs in minimum time.
Internet users increasingly rely on commercial virtual private network (VPN) services to protect their security and privacy. The VPN services route the clients traffic over an encrypted tunnel to a VPN gateway in the cloud. Thus, they hide the clients real IP address from online services, and they also shield the users connections from perceived threats in the access networks. In this paper, we study the security of such commercial VPN services. The focus is on how the client applications set up VPN tunnels, and how the service providers instruct users to configure generic client software. We analyze common VPN protocols and implementations on Windows, macOS and Ubuntu. We find that the VPN clients have various configuration flaws, which an attacker can exploit to strip off traffic encryption or to bypass authentication of the VPN gateway. In some cases, the attacker can also steal the VPN users username and password. We suggest ways to mitigate each of the discovered vulnerabilities.
Cloud-application add-ons are microservices that extend the functionality of the core applications. Many application vendors have opened their APIs for third-party developers and created marketplaces for add-ons (also add-ins or apps). This is a relatively new phenomenon, and its effects on the application security have not been widely studied. It seems likely that some of the add-ons have lower code quality than the core applications themselves and, thus, may bring in security vulnerabilities. We found that many such add-ons are vulnerable to cross-site scripting (XSS). The attacker can take advantage of the document-sharing and messaging features of the cloud applications to send malicious input to them. The vulnerable add-ons then execute client-side JavaScript from the carefully crafted malicious input. In a major analysis effort, we systematically studied 300 add-ons for three popular application suites, namely Microsoft Office Online, G Suite and Shopify, and discovered a significant percentage of vulnerable add-ons in each marketplace. We present the results of this study, as well as analyze the add-on architectures to understand how the XSS vulnerabilities can be exploited and how the threat can be mitigated.
A smart home connects tens of home devices to the Internet, where an IoT cloud runs various home automation applications. While bringing unprecedented convenience and accessibility, it also introduces various security hazards to users. Prior research studied smart home security from several aspects. However, we found that the complexity of the interactions among the participating entities (i.e., devices, IoT clouds, and mobile apps) has not yet been systematically investigated. In this work, we conducted an in-depth analysis of five widely-used smart home platforms. Combining firmware analysis, network traffic interception, and blackbox testing, we reverse-engineered the details of the interactions among the participating entities. Based on the details, we inferred three legitimate state transition diagrams for the three entities, respectively. Using these state machines as a reference model, we identified a set of unexpected state transitions. To confirm and trigger the unexpected state transitions, we implemented a set of phantom devices to mimic a real device. By instructing the phantom devices to intervene in the normal entity-entity interactions, we have discovered several new vulnerabilities and a spectrum of attacks against real-world smart home platforms.