Modern web sites make extensive use of client-side code, but this code runs on untrusted machines and thus the server-side code must validate all client-side requests. Errors in code that validates requests open the server to attacks by adversaries that send malicious requests. SecureDart extends the Dart language and runtime to support writing trustable client-side code. Requests from trusted client-side code contain a certificate that the server uses to validate the request’s authenticity.

We have implemented SecureDart as an extension to the Dart compiler. We have evaluated SecureDart on web application benchmarks and were able to secure the applications against client-side attacks with minimal overhead.

Writing correct concurrent code that uses atomics under the C/C++ memory model is extremely difficult. This thesis presents C11Tester, a race detector for the C/C++ memory model that can explore executions in a larger fragment of the C/C++ memory model than previous race detector tools. Relative to previous work, C11Tester's larger fragment includes behaviors that are exhibited by ARM processors. C11Tester uses a new constraint-based algorithm to implement modification order that is optimized to allow C11Tester to make decisions in terms of application-visible behaviors. This thesis evaluates C11Tester on several benchmark applications, and compare C11Tester's performance to both tsan11rec, the state of the art tool that controls scheduling for C/C++; and tsan11, the state of the art tool that does not control scheduling.

Control flow integrity or CFI has emerged as an important technique for

preventing attacks on software. Previous approaches relied on static

analysis and thus largely target static binaries and are limited in how

tightly they can constrain a program's runtime behavior. Unfortunately,

modern Windows applications make extensive use of dynamically generated

code. We introduce a new dynamic analysis based approach in DCFI to

control flow integrity that precisely learns a program's behavior by

monitoring previous executions. DCFI is the first approach to

demonstrate CFI in the presence of dynamic code generation and/or

self-modifying code and is immune to recent variations on ROP attacks

that thwart previous CFI approaches. DCFI underapproximates the legal

executions of software applications and thus can potentially build

tighter constraints than static approaches. As DCFI's knowledge of a

program becomes more complete, it tightens its constraints on a

program's execution, making successful attacks progressively more

difficult.

We have implemented DCFI in DynamoRIO. Our experiences using DCFI

indicate that it can protect modern desktop applications with dynamic

code generation engines including the latest versions of Microsoft Word,

Microsoft Excel, Microsoft PowerPoint, Microsoft Outlook, Google Chrome,

and Adobe Acrobat. Experiments also show that DCFI effectively detects

known exploits.

Remote code execution (RCE) exploits are considered among the more destructive intrusions in today’s software security landscape because they allow the adversary to execute arbitrary code with the permissions of the victim process. Today’s leading software defense systems are able to eliminate significant portions of this attack surface, but many of these approaches such as control flow integrity (CFI) and intrusion detection systems (IDS) address a limited scope of attack vectors, while others like diversification have not received wide user adoption. Consequently, user applications remain vulnerable to RCE attacks. One limitation that is common among these approaches is an overcommitment to preventing the adversary’s takeover strategy. Since the domain of potential attack vectors may be infinite, the adversary may always be able to devise a new takeover strategy that cannot be detected or prevented by any of the existing takeover-oriented defenses. After an attack, current monitoring systems often do not provide sufficient information about how the adversary took control or what vulnerability was compromised. Forensic tools can derive this information from an instance of the attack, but it may take multiple days or even weeks to isolate an instance for analysis.

Motivated by the need for a program monitor that is equally effective against unforeseen takeover strategies as well as an exploit payload, Introspective Intrusion Detection (IID) combines the advantages of traditional intrusion detection and CFI by distinguishing anomalies in execution without making absolute judgments about malicious intent. This approach begins with a profiling phase that distills observed execution paths into a compact data representation called a trusted profile that constitutes a “ground truth” of safe application behavior. When deployed for online monitoring, IID reports any deviation from the Trusted Profile as a potential intrusion. Software developers can benefit from IID as a complement to deployed defenses by gaining visibility into unforeseen malicious behaviors or evasive variations of known attacks. Debugging of field failures and error reports can also benefit from the deep introspective logging provided by IID. Where deployed software has ample performance headroom and sufficient technical support, IID can also be deployed as a comprehensive realtime monitor to detect advanced persistent threats (APT) and other evasive intrusions.

Experimental evaluation of IID prototypes for x86 binary executables and PHP applications show that this technique (a) identifies unforeseen takeover strategies along with exploit payloads, (b) accurately distinguishes benign anomalies from those associated with real attacks, (c) incurs low overhead with minimal false positives during normal execution of server applications such as Microsoft IIS and web applications such as WordPress, and (d) incurs moderate overhead for desktop applications such as Microsoft Office, Google Chrome and Adobe PDF Reader with a false positive rate suitable for expert analysis.

Concurrent software is difficult to debug. C++ uses a relaxed memory model, so concurrent software written in C++ using atomics is extra difficult to debug. We built a smart fuzzer for concurrent C++ programs that implemented the relaxed memory model for C++ atomics. This paper presents an informal operational semantics of the C++20 memory model, along with a description of the work done to implement it in the fuzzer. Code is instrumented using a compiler pass to replace operations with calls into the fuzzer library which is preloaded into the program. The fuzzer intercepts the main function to take control of the program. We show that the fuzzer can find bugs in small demo programs created as unit tests for other tools. Unfortunately, our approach to program instrumentation is defeated by programming practices that are common to real-world code using C++ atomics. Additional limitations of our instrumentation approach are discussed, as well as other challenges we ran into when working with real-world code. We then propose an alternate instrumentation strategy that could be used to overcome all observed challenges for future work.

Persistent memory (PM) technologies offer performance close to DRAM with persistence. Persistent memory enables programs to directly modify persistent data through normal load and store instructions bypassing heavyweight OS system calls for persistency. Ensuring that these programs are crash-consistent (i.e., power failures) is a major challenge. Stores to persistent memory are not immediately made persistent --- they initially reside in processor cache and are only written to PM when a flush occurs due to space constraints or explicit flush instructions. It is more challenging to test crash consistency for PM than for disks given the PM's byte-addressability that leads to significantly more states. Most of the existing state-of-the-art testing tools require heavy user annotations, report violations that may not correspond to actual bugs, do not test the recovery procedure, and rely on a test suite to cover all test scenarios.

This dissertation describes three different testing tools to verify the crash consistency of persistent memory programs:1) Jaaru: a fully-automated and ultra-efficient model checker for PM programs. Key to Jaaru's efficiency is a new technique based on constraint refinement that can reduce the number of executions that must be explored by many orders of magnitude. This exploration technique effectively leverages commit stores, a common coding pattern, to reduce the model checking complexity from exponential in the length of program executions to quadratic. 2) PSan: a tool introducing robustness as a sufficient correctness condition to ensure that program executions are free from bugs resulting from missing flushes. PSan implements an algorithm for checking robustness. This tool can help developers both identify silent data corruption bugs and localize bugs in large traces to the problematic memory operations that are missing flush operations. 3) Yashme: a tool that can detect a novel class of crash consistency bugs for persistent memory programs, which we call persistency races. Persistency races can cause non-atomic stores to be made partially persistent. Persistency races arise due to the interaction of standard compiler optimizations with persistent memory semantics. A major challenge is that in order to detect persistency races, the execution must crash in a very narrow window between a store with a persistency race and its corresponding cache flush operation, making it challenging for naive techniques to be effective. Yashme overcomes this challenge with a novel technique for detecting races in executions that are prefixes of the pre-crash execution. This technique enables Yashme to effectively find persistency races even if the injected crashes do not fall into that window.

These testing frameworks were capable of finding many bugs in well-tested applications ranging from persistent data structures to real-world frameworks. These bugs are reported to the developers of these frameworks and most of them are confirmed and the corresponding fixes are available on their Github repositories.

Concurrent data structures often provide better performance on multi-core platforms, but are significantly more difficult to design and verify than their sequential counterparts. The C/C++11 standard introduced a weak language memory model supporting low-level atomic operations such as compare and swap (CAS). While these atomic operations can significantly improve the performance of concurrent data structures, programming at this level introduces non-intuitive behaviors that significantly increase the difficulty of developing code.

In this paper, we present CDSSPEC, a specification language checker that allows developers to write simple specifications for low-level concurrent data structures that make use of C/C++11 atomics and check the correctness of concurrent data structures against these specifications. We have evaluated CDSSPEC by annotating and checking several concurrent data structures.

Modern SAT solvers are extremely efficient at solving boolean satisfiability problems, enabling a wide spectrum of techniques for checking, verifying, and validating real-world programs. What remains challenging, though, is how to encode a domain problem (e.g. model checking) into a SAT formula because the same problem can have multiple distinct encodings, which can yield performance results that are orders-of-magnitude apart, regardless of the underlying solvers used. We develop Satune, a tool that can automatically synthesize SAT encoders for different problem domains. Satune employs a DSL that allows developers to express domain problems at a high level and a search algorithm that can effectively find efficient solutions. The search process is guided by observations made over example encodings and their performance for the domain and hence Satune can quickly synthesize a high-performance encoder by incorporating patterns from examples that yield good performance. A thorough evaluation with JMCR, SyPet, Dirk, Hexiom, Sudoku, and KillerSudoku demonstrates that Satune can easily synthesize high-performance encoders for different domains including model checking, synthesis, and games. These encodings generate constraint problems that are often several orders of magnitude faster to solve than the original encodings used by the tools.

In this work, we view smart home from 3 different sides: devices, platforms, and apps. We first attempt to better understand the problems on each side and later explore new methods and techniques to better guarantee security, privacy, and safety of smart homes.

On the devices side, we discovered that smart home devices are vulnerable to passive inference attacks based on network traffic, even in the presence of encryption. We first present this passive inference attack and our techniques that we developed to exploit this vulnerability on smart home devices. We created 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 home-automation systems. Furthermore, we also present our discussion and evaluation on existing techniques (e.g., packet padding) as possible defenses against passive inference attacks and their analyses.

On the platforms side, smart home platforms such as SmartThings enable homeowners to manage devices in sophisticated ways to save energy, improve security, and provide conveniences. Unfortunately, we discovered that smart home platforms contain vulnerabilities, potentially impacting home security and privacy. Aside from the traditional defense techniques to enhance the security and privacy of smart home devices, we also created Vigilia, a system that shrinks the attack surface of smart home IoT systems by restricting the network access of devices. As existing smart home systems are closed, we have created an open implementation of a similar programming and configuration model in Vigilia and extended the execution environment to maximally restrict communications by instantiating device-based network permissions. We have implemented and compared Vigilia with forefront IoT-defense systems; our results demonstrate that Vigilia outperforms these systems and incurs negligible overhead.

On the apps side, smart home platforms allow developers to write apps to make smart home devices work together to accomplish tasks, e.g., home security and energy conservation—smart home devices provide the convenience of remotely controlling and automating home appliances. A smart home app typically implements narrow functionality and thus to fully implement desired functionality homeowners may need to install multiple apps. These different apps can conflict with each other and these conflicts can result in undesired actions such as locking the door during a fire. We study conflicts between apps on Samsung SmartThings, the most popular platform for developing and deploying smart home IoT devices. By collecting and studying 198 official and 69 third-party apps, we found significant app conflicts in 3 categories: (1) close to 60% of app pairs that access the same device, (2) more than 90% of app pairs with physical interactions, and (3) around 11% of app pairs that access the same global variable. Our results suggest that the problem of conflicts between smart home apps is serious and can create potential safety risks. We then developed an automatic conflict detection tool that uses model checking to automatically detect up to 96% of the conflicts.

Eliminating so-called "out-of-thin-air" (OOTA) results is an open problem in many existing programming language memory models including Java, C, and C++. OOTA behaviors are problematic in that they break both formal and informal modular reasoning about program behavior. In spite of many years of research efforts, defining memory model semantics that are easily understood, allow existing optimizations, and forbid OOTA results remains an open problem. This dissertation explores two solutions to this problem that forbid OOTA results. The first solution is targeted towards Java-like languages in which all memory operations may create OOTA results, and the second solution is targeted towards C/C++-like memory models in which racing operations are explicitly labeled as atomic operations. Our solutions provide a per-candidate execution criterion that makes it possible to examine a single execution and determine whether the memory model permits the execution. We implemented and evaluated both solutions in the LLVM compiler framework. Our results show that on an ARMv8 processor the first solution has an average overhead of 3.1% and a maximum overhead of 17.6% on the SPEC CPU2006 C/C++ benchmarks, and that the second solution has no overhead on average and a maximum overhead of 6.3% on 43 concurrent data structures. The results indicate that these approaches to eliminating out-of-thin-air behaviors deserve further consideration.