Rahmadi Trimananda

Rahmadi Trimananda, Weiyu Luo, Brian Demsky et al.

Event-driven architectures are broadly used for systems that must respond to events in the real world. Event-driven applications are prone to concurrency bugs that involve subtle errors in reasoning about the ordering of events. Unfortunately, there are several challenges in using existing model-checking techniques on these systems. Event-driven applications often loop indefinitely and thus pose a challenge for stateless model checking techniques. On the other hand, deploying purely stateful model checking can explore large sets of equivalent executions. In this work, we explore a new technique that combines dynamic partial order reduction with stateful model checking to support non-terminating applications. Our work is (1) the first dynamic partial order reduction algorithm for stateful model checking that is sound for non-terminating applications and (2) the first dynamic partial reduction algorithm for stateful model checking of event-driven applications. We experimented with the IoTCheck dataset: a study of interactions in smart home app pairs. This dataset consists of app pairs originated from 198 real-world smart home apps. Overall, our DPOR algorithm successfully reduced the search space for the app pairs, enabling 69 pairs of apps that did not finish without DPOR to finish and providing a 7X average speedup.

Rahmadi Trimananda, Hieu Le, Hao Cui et al.

Virtual reality (VR) is an emerging technology that enables new applications but also introduces privacy risks. In this paper, we focus on Oculus VR (OVR), the leading platform in the VR space and we provide the first comprehensive analysis of personal data exposed by OVR apps and the platform itself, from a combined networking and privacy policy perspective. We experimented with the Quest 2 headset and tested the most popular VR apps available on the official Oculus and the SideQuest app stores. We developed OVRseen, a methodology and system for collecting, analyzing, and comparing network traffic and privacy policies on OVR. On the networking side, we captured and decrypted network traffic of VR apps, which was previously not possible on OVR, and we extracted data flows, defined as <app, data type, destination>. Compared to the mobile and other app ecosystems, we found OVR to be more centralized and driven by tracking and analytics, rather than by third-party advertising. We show that the data types exposed by VR apps include personally identifiable information (PII), device information that can be used for fingerprinting, and VR-specific data types. By comparing the data flows found in the network traffic with statements made in the apps' privacy policies, we found that approximately 70% of OVR data flows were not properly disclosed. Furthermore, we extracted additional context from the privacy policies, and we observed that 69% of the data flows were used for purposes unrelated to the core functionality of apps.

Rahmadi Trimananda, Ali Younis, Thomas Kwa et al.

Smart home IoT systems often rely on cloud-based servers for communication between components. Although there exists a body of work on IoT security, most of it focuses on securing clients (i.e., IoT devices). However, cloud servers can also be compromised. Existing approaches do not typically protect smart home systems against compromised cloud servers. This paper presents FIDELIUS: a runtime system for secure cloud-based storage and communication even in the presence of compromised servers. FIDELIUS's design is tailored for smart home systems that have intermittent Internet access. In particular, it supports local control of smart home devices in the event that communication with the cloud is lost, and provides a consistency model using transactions to mitigate inconsistencies that can arise due to network partitions. We have implemented FIDELIUS, developed a smart home benchmark that uses FIDELIUS, and measured FIDELIUS's performance and power consumption. Our experiments show that compared to the commercial Particle.io framework, FIDELIUS reduces more than 50% of the data communication time and increases battery life by 2X. Compared to PyORAM, an alternative (ORAM-based) oblivious storage implementation, FIDELIUS has 4-7X faster access times with 25-43X less data transferred.

Rahmadi Trimananda, Janus Varmarken, Athina Markopoulou et al.

Smart home devices are vulnerable to passive inference attacks based on network traffic, even in the presence of encryption. In this paper, we present PINGPONG, a tool that can automatically extract packet-level signatures for device events (e.g., light bulb turning ON/OFF) from network traffic. We evaluated PINGPONG on popular smart home devices ranging from smart plugs and thermostats to cameras, voice-activated devices, and smart TVs. We were able to: (1) automatically extract previously unknown signatures that consist of simple sequences of packet lengths and directions; (2) use those signatures to detect the devices or specific events with an average recall of more than 97%; (3) show that the signatures are unique among hundreds of millions of packets of real world network traffic; (4) show that our methodology is also applicable to publicly available datasets; and (5) demonstrate its robustness in different settings: events triggered by local and remote smartphones, as well as by homeautomation systems.