Many solutions have been proposed to curb unexpected behavior of automation apps installed on programmable IoT platforms by enforcing safety policies at runtime. However, all prior work addresses a weaker version of the actual problem due to a simpler, unrealistic threat model. These solutions are not general enough as they are heavily dependent on the installed apps and catered to specific IoT platforms. Here, we address a stronger version of the problem via a realistic threat model, where (i) undesired cyber actions can come from not only automation platform backends (e.g., SmartThings) but also close-sourced third-party services (e.g., IFTTT), and (ii) physical actions (e.g., user interactions) on devices can move the IoT system to an undesirable state. We propose a runtime mechanism, dubbed Maverick, which employs an app-independent, platform-agnostic mediator to enforce policies against all undesired cyber actions and applies corrective-actions to bring the IoT system back to a safe state from an unsafe state transition. Maverick is equipped with a policy language capable of expressing rich temporal invariants and an automated toolchain that includes a policy synthesizer and a policy analyzer for user assistance. We implemented Maverick in a prototype and showed its efficacy in both physical and virtual testbeds, incurring minimal overhead.

Protocols are one of the founding pillars of network communication. Given their importance, protocols have received great attention not only from the research community but also from adversaries. Protocols, particularly their implementations, have been lucrative targets for adversarial attacks to induce network insecurity by compromising the guarantees that these implementations should provide. Most of these attacks can be traced back to the leniency in their design, code, or configuration. Finding leniency in implementations is challenging as these lenient instances are primarily tied to the semantics of the protocol and thus demand for techniques unlike existing approaches that we use for finding low-level memory corruption bugs.

In this paper, we perform the first multifaceted measurement study to investigate the widespread insecure practices employed by tertiary education institutes (TEIs) around the globe when offering WPA2-Enterprise Wi-Fi services. The security of such services critically hinges on two aspects: (1) the connection configuration on the client-side; and (2) the TLS setup on the authentication servers. Weaknesses in either can leave users susceptible to credential theft. Typically, TEIs prescribe to their users either manual instructions or pre-configured profiles (e.g., eduroam CAT). For studying the security of configurations, we present a framework in which each configuration is mapped to an abstract security label drawn from a strict partially ordered set. We first used this framework to evaluate the configurations supported by the user interfaces (UIs) of mainstream operating systems (OSs), and discovered many design weaknesses. We then considered 7045 TEIs in 54 countries/regions, and collected 7275 configuration instructions from 2061 TEIs. Our analysis showed that majority of these instructions lead to insecure configurations, and nearly 86% of those TEIs can suffer from credential thefts on at least one OS. We also analyzed a large corpus of pre-configured eduroam CAT profiles and discovered several misconfiguration issues that can negatively impact security. Finally, we evaluated the TLS parameters used by authentication servers of thousands of TEIs and discovered perilous practices, such as the use of expired certificates, deprecated versions of TLS, weak signature algorithms, and suspected cases of private key reuse among TEIs. Our long list of findings have been responsibly disclosed to the relevant stakeholders, many of which have already been positively acknowledged.

This paper focuses on developing an automatic, black-box testing approach called Morpheus to check the non-compliance of libraries implementing PKCS#1-v1.5 signature verification with the PKCS#1-v1.5 standard. Non-compliance can not only make implementations vulnerable to Bleichenbacher-style RSA signature forgery attacks but also can induce interoperability issues. For checking non-compliance, Morpheus adaptively generates interesting test cases and then takes advantage of an oracle, a formally proven correct implementation of PKCS#1-v1.5 signature standard, to detect non-compliance in an implementation under test. We have used Morpheus to test 45 implementations of PKCS#1-v1.5 signature verification and discovered that 6 of them are susceptible to variants of the Bleichenbacher-style low public exponent RSA signature forgery attack, 1 implementation has a buffer overflow, 33 implementations have incompatibility issues, and 8 implementations have minor leniencies. Our findings have been responsibly disclosed and positively acknowledged by the developers.

This paper focuses on developing a security mechanism geared towards appified smart-home platforms. Such platforms often expose programming interfaces for developing automation apps that mechanize different tasks among smart sensors and actuators (e.g., automatically turning on the AC when the room temperature is above 80 F). Due to the lack of effective access control mechanisms, these automation apps can not only have unrestricted access to the user's sensitive information (e.g., the user is not at home) but also violate user expectations by performing undesired actions. As users often obtain these apps from unvetted sources, a malicious app can wreak havoc on a smart-home system by either violating the user's security and privacy, or creating safety hazards (e.g., turning on the oven when no one is at home). To mitigate such threats, we propose Expat which ensures that user expectations are never violated by the installed automation apps at runtime. To achieve this goal, Expat provides a platform-agnostic, formal specification language UEI for capturing user expectations of the installed automation apps' behavior. For effective authoring of these expectations (as policies) in UEI, Expat also allows a user to check the desired properties (e.g., consistency, entailment) of them; which due to their formal semantics can be easily discharged by an SMT solver. Expat then enforces UEI policies in situ with an inline reference monitor which can be realized using the same app programming interface exposed by the underlying platform. We instantiate Expat for one of the representative platforms, OpenHAB, and demonstrate it can effectively mitigate a wide array of threats by enforcing user expectations while incurring only modest performance overhead.

Network protocol implementations must comply with their specifications that include properties describing the correct operational behavior of the protocol in response to different temporal orderings of network events. Due to inconsistent interpretations of the specification, developers can unknowingly introduce semantic bugs, which cause the implementations to violate the respective properties. Detecting such bugs in stateful protocols becomes significantly difficult as their operations depend on their internal state machines and the complex interactions between the protocol logic. In this paper, we present an automated tool to help developers analyze their protocol implementations and detect semantic bugs violating the temporal properties of the protocols. Given an implementation, our tool (1) extracts the implemented finite state machine (FSM) of the protocol from the source code by symbolically exploring the code and (2) determines whether the extracted FSM violates given temporal properties by using an off-the-shelf model checker. We demonstrated the efficacy of our tool by applying it on 6 protocol implementations. We detected 11 semantic bugs (2 with security implications) when we analyzed these implementations against properties obtained from their publicly available specifications.

The X.509 Public-Key Infrastructure has long been used in the SSL/TLS protocol to achieve authentication. A recent trend of Internet-of-Things (IoT) systems employing small footprint SSL/TLS libraries for secure communication has further propelled its prominence. The security guarantees provided by X.509 hinge on the assumption that the underlying implementation rigorously scrutinizes X.509 certificate chains, and accepts only the valid ones. Noncompliant implementations of X.509 can potentially lead to attacks and/or interoperability issues. In the literature, black-box fuzzing has been used to find flaws in X.509 validation implementations, fuzzing, however, cannot guarantee coverage and thus severe flaws may remain undetected. To thoroughly analyze X.509 implementations in small footprint SSL/TLS libraries, this paper takes the complementary approach of using symbolic execution. We observe that symbolic execution, a technique proven to be effective in finding software implementation flaws, can also be leveraged to expose noncompliance in X.509 implementations. Directly applying an off-the-shelf symbolic execution engine on SSL/TLS libraries is, however, not practical due to the problem of path explosion. To this end, we propose the use of SymCerts, which are X.509 certificate chains carefully constructed with a mixture of symbolic and concrete values. Utilizing SymCerts and some domain-specific optimizations, we symbolically execute the certificate chain validation code of each library and extract path constraints describing its accepting and rejecting certificate universes. These path constraints help us identify missing checks in different libraries. For exposing subtle but intricate noncompliance with X.509 standard, we cross-validate the constraints extracted from different libraries to find further implementation flaws. Our analysis of 9 small footprint X.509 implementations has uncovered 48 instances of noncompliance. Findings and suggestions provided by us have already been incorporated by developers into newer versions of their libraries.

As the Internet becomes an important part of the infrastructure our society depends on, it is crucial to construct networks that are able to work even when part of the network is compromised. This paper presents the first practical intrusion-tolerant network service, targeting high-value applications such as monitoring and control of global clouds and management of critical infrastructure for the power grid. We use an overlay approach to leverage the existing IP infrastructure while providing the required resiliency and timeliness. Our solution overcomes malicious attacks and compromises in both the underlying network infrastructure and in the overlay itself. We deploy and evaluate the intrusion-tolerant overlay implementation on a global cloud spanning East Asia, North America, and Europe, and make it publicly available.

Numerous routing protocols have been designed and subjected to model checking and simulations. However, model checking the design or testing the simulator-based prototype of a protocol does not guarantee that the implementation is free of bugs and vulnerabilities. Testing implementations beyond their basic functionality (also known as adversarial testing) can increase protocol robustness. We focus on automated adversarial testing of real-world implementations of wireless routing protocols. In our previous work we created Turret, a platform that uses a network emulator and virtualization to test unmodified binaries of general distributed systems. Based on Turret, we create Turret-W designed specifically for wireless routing protocols. Turret-W includes new functionalities such as differentiating routing messages from data messages to enable evaluation of attacks on the control plane and the data plane separately, support for several additional protocols (e.g., those that use homogeneous/heterogenous packet formats, those that run on geographic forwarding (not just IP), those that operate at the data link layer instead of the network layer), support for several additional attacks (e.g., replay attacks) and for establishment of adversarial side-channels that allow for collusion. Turret-W can test not only general routing attacks, but also wireless specific attacks such as wormhole. Using Turret-W on publicly available implementations of five representative routing protocols, we (re-)discovered 37 attacks and 3 bugs. All these bugs and 5 of the total attacks were not previously reported to the best of our knowledge.

Security and performance are critical goals for distributed systems. The increased design complexity, incomplete expertise of developers, and limited functionality of existing testing tools often result in bugs and vulnerabilities that prevent implementations from achieving their design goals in practice. Many of these bugs, vulnerabilities, and misconfigurations manifest after the code has already been deployed making the debugging process difficult and costly. In this paper, we present Turret, a platform for automatically finding performance attacks in unmodified implementations of distributed systems. Turret does not require the user to provide any information about vulnerabilities and runs the implementation in the same operating system setup as the deployment, with an emulated network. Turret uses a new attack finding algorithm and several optimizations that allow it to find attacks in a matter of minutes. We ran Turret on 5 different distributed system implementations specifically designed to tolerate insider attacks, and found 30 performance attacks, 24 of which were not previously reported to the best of our knowledge.

We focus on automated adversarial testing of real-world implementations of wireless routing protocols. We extend an existing platform, Turret, designed for general distributed systems, to address the specifics of wireless routing protocols. Specifically, we add functionality to differentiate routing messages from data messages and support wireless specific attacks such as blackhole and wormhole, or routing attacks such as replay attacks. The extended platform, Turret-W, uses a network emulator to create reproducible network conditions and virtualization to run unmodified binaries of wireless protocol implementations. Using the platform on publicly available implementations of two representative routing protocols we (re-)discovered 14 attacks and 3 bugs.

The openness of the Android operating system increased the number of applications developed, but it also introduced a new propagation vector for mobile malware. We model the propagation of mobile malware using epidemiology theory and study the problem as a function of the underlying mobility models. We define the optimal approach to heal an infected system with the help of a set of static healers that distribute patches, as the T-COVER problem and show that it is NP-HARD. We then propose two families of healer protocols that trade-off time recovery and energy consumed by sending patches. The first one uses randomization to ensure a small recovery time but may result in healers sending more patches than needed. The second one uses system feedback to optimize energy consumed by sending patches, but it may result in a larger recovery time. We show through simulations using the NS-3 simulator that despite lacking knowledge of the future, our protocols obtain a recovery time within a 10x bound of the oracle solution that knows the arrival time of the infected nodes.

Privacy protection is a very important issue during authentications in RFID systems. In order to achieve high-speed authentication in large-scale RFID systems, researchers propose tree-based approaches, in which any pair of tags share a number of key components. Another technique can be to perform group based private authentication that improves the tradeoff between scalability and privacy by dividing the tags into a number of groups. This is a novel authentication scheme that ensures privacy of the provers. However, one limitation of this technique is that the level of privacy provided by the scheme decreases as more and more tags are compromised Therefore, in this paper, we propose a group based anonymous private authentication protocol (AnonPri) that provides higher level of privacy than the above mention group based scheme and achieves better efficiency than the approaches that prompt the reader to perform an exhaustive search. Our protocol provides unlinkability and thereby preserves privacy. The adversary cannot link the responses with the tags, even if she can learn the identifier that the tags are using to produce the response. To evaluate AnonPri, we have compared both the protocols, AnonPri and the group based authentication. The experiment results establish that the level of privacy provided by AnonPri is higher than that of the group based authentication.