Tech Reports in Computer Science and Engineering

Permanent URI for this communityhttp://hdl.handle.net/1903/5

The technical reports collections in this community are deposited by the Library of the Computer Science department. If you have questions about these collections, please contact library staff at library@cs.umd.edu

Browse

Filters

2003 - 2009132010 - 201413

Settings

Author: search.filters.author.Hicks, Michael

Search Results

Now showing 1 - 10 of 26
  • Thumbnail Image
    Item
    Automating Efficient RAM-Model Secure Computation
    (2014-03-13) Liu, Chang; Huang, Yan; Shi, Elaine; Katz, Jonathan; Hicks, Michael
    RAM-model secure computation addresses the inherent limitations of circuit-model secure computation considered in almost all previous work. Here, we describe the first automated approach for RAM-model secure computation in the semi-honest model. We define an intermediate representation called SCVM and a corresponding type system suited for RAM-model secure computation. Leveraging compile-time optimizations, our approach achieves order-of-magnitude speedups compared to both circuit-model secure computation and the state-of-art RAM-model secure computation.
  • Thumbnail Image
    Item
    Wysteria: A Programming Language for Generic, Mixed-Mode Multiparty Computations
    (2014-03-14) Rastogi, Aseem; Hammer, Matthew A.; Hicks, Michael
    In a Secure Multiparty Computation (SMC), mutually distrusting parties use cryptographic techniques to cooperatively compute over their private data; in the process each party learns only explicitly revealed outputs. In this paper, we present Wysteria, a high-level programming language for writing SMCs. As with past languages, like Fairplay, Wysteria compiles secure computations to circuits that are executed by an underlying engine. Unlike past work, Wysteria provides support for mixed-mode programs, which combine local, private computations with synchronous SMCs. Wysteria complements a standard feature set with built-in support for secret shares and with wire bundles, a new abstraction that supports generic n-party computations. We have formalized Wysteria, its refinement type system, and its operational semantics. We show that Wysteria programs have an easy-to-understand single-threaded interpretation and prove that this view corresponds to the actual multi-threaded semantics. We also prove type soundness, a property we show has security ramifications, namely that information about one party's data can only be revealed to another via (agreed upon) secure computations. We have implemented Wysteria, and used it to program a variety of interesting SMC protocols from the literature, as well as several new ones. We find that Wysteria's performance is competitive with prior approaches while making programming far easier, and more trustworthy.
  • Thumbnail Image
    Item
    Adapton: Composable, Demand-Driven Incremental Computation
    (2013-07-12) Hammer, Matthew A.; Phang, Khoo Yit; Hicks, Michael; Foster, Jeffrey S.
    Many researchers have proposed programming languages that support incremental computation (IC), which allows programs to be efficiently re-executed after a small change to the input. However, existing implementations of such languages have two important drawbacks. First, recomputation is oblivious to specific demands on the program output; that is, if a program input changes, all dependencies will be recomputed, even if an observer no longer requires certain outputs. Second, programs are made incremental as a unit, with little or no support for reusing results outside of their original context, e.g., when reordered. To address these problems, we present lambdaCDDIC, a core calculus that applies a demand-driven semantics to incremental computation, tracking changes in a hierarchical fashion in a novel demanded computation graph. lambdaCDDIC also formalizes an explicit separation between inner, incremental computations and outer observers. This combination ensures lambdaCDDIC programs only recompute computations as demanded by observers, and allows inner computations to be composed more freely. We describe an algorithm for implementing lambdaCDDIC efficiently, and we present AdaptOn, a library for writing lambdaCDDIC-style programs in OCaml. We evaluated AdaptOn on a range of benchmarks, and found that it provides reliable speedups, and in many cases dramatically outperforms prior state-of-the-art IC approaches.
  • Thumbnail Image
    Item
    Expositor: Scriptable Time-Travel Debugging with First Class Traces
    (2013-02-24) Khoo, Yit Phang; Foster, Jeffrey S.; Hicks, Michael
    We present Expositor, a new debugging environment that combines scripting and time-travel debugging to allow programmers to automate complex debugging tasks. The fundamental abstraction provided by Expositor is the execution trace, which is a time-indexed sequence of program state snapshots or projections thereof. Programmers can manipulate traces as if they were simple lists with operations such as map and filter. Under the hood, Expositor efficiently implements traces as lazy, sparse interval trees whose contents are materialized on demand. Expositor also provides a novel data structure, the edit hash array mapped trie, which is a lazy implementation of sets, maps, multisets, and multimaps that enables programmers to maximize the efficiency of their debugging scripts. In our micro-benchmarks, Expositor scripts are faster than the equivalent non-lazy scripts for common debugging scenarios. We have also used Expositor to debug a stack overflow, and to unravel a subtle data race in Firefox. We believe that Expositor represents an important step forward in improving the technology for diagnosing complex, hard-to-understand bugs.
  • Thumbnail Image
    Item
    Memory Trace Oblivious Program Execution
    (2013-02-06) Liu, Chang; Hicks, Michael; Shi, Elaine
    Cloud computing allows users to delegate data and computation to cloud service providers, at the cost of giving up physical control of their computing infrastructure. An attacker (e.g., insider) with physical access to the computing platform can perform various physical attacks, including probing memory buses and cold-boot style attacks. Previous work on secure (co-)processors provides hardware support for memory encryption and prevents direct leakage of sensitive data over the memory bus. However, an adversary snooping on the bus can still infer sensitive information from the memory access traces. Existing work on Oblivious RAM (ORAM) provides a solution for users to put all data in an ORAM; and accesses to an ORAM are obfuscated such that no information leaks through memory access traces. This method, however, incurs significant memory access overhead. In this work, we are among the first to leverage programming language techniques to offer efficient memory-trace oblivious program execution, while providing formal security guarantees. We first formally define the notion of memory-trace obliviousness, and provide a type system for verifying that a program satisfies this property. We then design a compiler that transforms a program into one that satisfies memory trace obliviousness. To achieve optimal efficiency, our compiler aims to minimize the usage of ORAM whenever possible, and would partition variables in smaller ORAM banks (which are faster to access than larger ORAM banks) without risking security. We use several example programs to demonstrate the efficiency gains our compiler achieves in comparison with the naive method of placing all variables in the same ORAM.
  • Thumbnail Image
    Item
    Kitsune: Efficient, General-purpose Dynamic Software Updating for C
    (2012-03-28) Hayden, Christopher M.; Smith, Edward K.; Denchev, Michail; Hicks, Michael; Foster, Jeffrey S.
    Dynamic software updating (DSU) systems allow programs to be updated while running, thereby allowing developers to add features and fix bugs without downtime. This paper introduces Kitsune, a new DSU system for C whose design has three notable features. First, Kitsune’s updating mechanism updates the whole program, not individual functions. This mechanism is more flexible than most prior approaches and places no restrictions on data representations or allowed compiler optimizations. Second, Kitsune makes the important aspects of updating explicit in the program text, making its semantics easy to understand while keeping programmer work to a minimum. Finally, the programmer can write simple specifications to direct Kitsune to generate code that traverses and transforms old-version state for use by the new code; such state transformation is often necessary, and is significantly more difficult in prior DSU systems. We have used Kitsune to update five popular, open-source, single- and multi-threaded programs, and find that few program changes are required to use Kitsune, and that it incurs essentially no performance overhead.
  • Thumbnail Image
    Item
    Specifying and Verifying the Correctness of Dynamic Software Updates
    (2011-11-15) Hayden, Christopher M.; Magill, Stephen; Hicks, Michael; Foster, Nate; Foster, Jeffrey S.
    Dynamic software updating (DSU) systems allow running programs to be patched on-the-fly to add features or fix bugs. While dynamic updates can be tricky to write, techniques for establishing their correctness have received little attention. In this paper, we present the first methodology for automatically verifying the correctness of dynamic updates. Programmers express the desired properties of an updated execution using client-oriented specifications (CO-specs), which can describe a wide range of client-visible behaviors. We verify CO-specs automatically by using off-the-shelf tools to analyze a merged program, which is a combination of the old and new versions of a program. We formalize the merging transformation and prove it correct. We have implemented a program merger for C, and applied it to updates for the Redis key-value store and several synthetic programs. Using Thor, a verification tool, we could verify many of the synthetic programs; using Otter, a symbolic executor, we could analyze every program, often in less than a minute. Both tools were able to detect faulty patches and incurred only a factor-of-four slowdown, on average, compared to single version programs.
  • Thumbnail Image
    Item
    Evaluating Dynamic Software Update Safety Using Systematic Testing
    (2011-09-22) Hayden, Christopher M.; Smith, Edward K.; Hardisty, Eric A.; Hicks, Michael; Foster, Jeffrey S.
    Dynamic software updating (DSU) systems patch programs on the fly without incurring downtime. To avoid failures due to the updating process itself, many DSU systems employ timing restrictions. However, timing restrictions are theoretically imperfect, and their practical effectiveness is an open question. This paper presents the first significant empirical evaluation of three popular timing restrictions: activeness safety (AS), which prevents updates to active functions; confreeness safety (CFS), which only allows modifications to active functions when doing so is provably type-safe; and manual identification of the event-handling loops during which an update may occur. We evaluated these timing restrictions using a series of DSU patches to three programs: OpenSSH, vsftpd, and ngIRCd.We systematically applied updates at each distinct update point reached during execution of a suite of system tests for these programs to determine which updates pass and which fail. We found that all three timing restrictions prevented most failures, but only manual identification allowed none. Further, although CFS and AS allowed many more update points, manual identification still supported updates with minimal delay. Finally, we found that manual identification required the least developer effort. Overall, we conclude that manual identification is most effective.
  • Thumbnail Image
    Item
    MultiOtter: Multiprocess Symbolic Execution
    (2011-05-26) Turpie, Jonathan; Reisner, Elnatan; Foster, Jeffrey S.; Hicks, Michael
    Symbolic execution can be an effective technique for exploring large numbers of program paths, but it has generally been applied to programs running in isolation, whose inputs are files or command-line arguments. Programs that take inputs from other programs---servers, for example---have been beyond the reach of symbolic execution. To address this, we developed a multiprocess symbolic executor called MultiOtter, along with an implementation of many of the POSIX functions, such as socket and select, that interactive programs usually rely on. However, that is just a first step. Next, we must determine what symbolic inputs to feed to an interactive program to make multiprocess symbolic execution effective. Providing completely unconstrained symbolic values causes symbolic execution to spend too much time exploring uninteresting paths, such as paths to handle invalid inputs. MultiOtter allows us to generate inputs that conform to a context-free grammar, similar to previous work, but it also enables new input generation capabilities because we can now run arbitrary programs concurrently with the program being studied. As examples, we symbolically executed a key-value store server, redis, and an FTP server, vsftpd, each with a variety of inputs, including symbolic versions of tests from redis's test suite and wget as a client for vsftpd. We report the coverage provided by symbolic execution with various forms of symbolic input, showing that different testing goals require different degrees of symbolic inputs.
  • Thumbnail Image
    Item
    Dynamic Enforcement of Knowledge-based Security Policies
    (2011-04-05) Mardziel, Piotr; Magill, Stephen; Hicks, Michael; Srivatsa, Mudhakar
    This paper explores the idea of knowledge-based security policies, which are used to decide whether to answer a query over secret data based on an estimation of the querier's (possibly increased) knowledge given the result. Limiting knowledge is the goal of existing information release policies that employ mechanisms such as noising, anonymization, and redaction. Knowledge-based policies are more general: they increase flexibility by not fixing the means to restrict information flow. We enforce a knowledge-based policy by explicitly tracking a model of a querier's belief about secret data, represented as a probability distribution. We then deny any query that could increase knowledge above a given threshold. We implement query analysis and belief tracking via abstract interpretation using a novel domain we call probabilistic polyhedra, whose design permits trading off precision with performance while ensuring estimates of a querier's knowledge are sound. Experiments with our implementation show that several useful queries can be handled efficiently, and performance scales far better than would more standard implementations of probabilistic computation based on sampling.