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

2005 - 2009132010 - 201515

Settings

Author: search.filters.author.Foster, Jeffrey S.Start date: 2000

Search Results

Now showing 1 - 10 of 28
  • Thumbnail Image
    Item
    Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution
    (2015-07-01) Micinski, Kristopher; Fetter-Degges, Jonathan; Jeon, Jinseong; Foster, Jeffrey S.; Clarkson, Michael R.
    Mobile apps can access a wide variety of secure information, such as contacts and location. However, current mobile platforms include only coarse access control mechanisms to protect such data. In this paper, we introduce interaction-based declassification policies, in which the user's interactions with the app constrain the release of sensitive information. Our policies are defined extensionally, so as to be independent of the app's implementation, based on sequences of security-relevant events that occur in app runs. Policies use LTL formulae to precisely specify which secret inputs, read at which times, may be released. We formalize a semantic security condition, interaction-based noninterference, to define our policies precisely. Finally, we describe a prototype tool that uses symbolic execution of Dalvik bytecode to check interaction-based declassification policies for Android, and we show that it enforces policies correctly on a set of apps.
  • 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
    SymDroid: Symbolic Execution for Dalvik Bytecode
    (2012-07-31) Jeon, Jinseong; Micinski, Kristopher K.; Foster, Jeffrey S.
    Apps on Google's Android mobile device platform are written in Java, but are compiled to a special bytecode language called Dalvik. In this paper, we introduce SymDroid, a symbolic executor that operates directly on Dalvik bytecode. SymDroid begins by first translating Dalvik into mu-Dalvik, a simpler language that has only 16 instructions, in contrast to Dalvik's more than 200 instructions. We present a formalism for SymDroid's symbolic executor, which can be described with a small number of operational semantics rules; this semantics may be of independent interest. In addition to modeling bytecode instructions, SymDroid also contains models of some key portions of the Android platform, including libraries and the platform's lifecycle control code. We evaluated SymDroid in two ways. First, we ran it on the Android Compatibility Test Suite, and found it passed all tests except ones that used library or system routines we have not yet implemented. On this test suite, SymDroid runs about twice as slow as the Dalvik VM, and about twice as fast as the Java VM. Second, we used SymDroid to discover the (path) conditions under which contacts may be accessed on an Android app, and found it was able to do so successfully. These results suggest that SymDroid, while still a prototype, is a promising first step in enabling direct, precise analysis of Android apps.
  • Thumbnail Image
    Item
    Troyd: Integration Testing for Android
    (2012-08-24) Jeon, Jinseong; Foster, Jeffrey S.
    We introduce Troyd, a new integration testing framework for Android apps. Troyd allows testers to write high-level scripts to drive the app under test as desired, e.g., clicking buttons on the screen, checking the contents of a text box, and so on. Troyd also provides a convenient recording mode, in which users construct Troyd scripts as the app is running; we have found that this interactivity is extremely useful in practice. Troyd is freely available as an open-source project.
  • Thumbnail Image
    Item
    Dr. Android and Mr. Hide: Fine-grained security policies on unmodified Android
    (2011-12-09) Jeon, Jinseong; Micinski, Kristopher K.; Vaughan, Jeffrey A.; Reddy, Nikhilesh; Zhu, Yixin; Foster, Jeffrey S.; Millstein, Todd
    Google’s Android platform includes a permission model that protects access to sensitive capabilities, such as Internet access, GPS use, and telephony. We have found that Android’s current permissions are often overly broad, providing apps with more access than they truly require. This deviation from least privilege increases the threat from vulnerabilities and malware. To address this issue, we present a novel system that can replace existing platform permissions with finer-grained ones. A key property of our approach is that it runs today, on stock Android devices, requiring no platform modifications. Our solution is composed of two parts: Mr. Hide, which runs in a separate process on a device and provides access to sensitive data as a service; and Dr. Android (Dalvik Rewriter for Android), a tool that transforms existing Android apps to access sensitive resources via Mr. Hide rather than directly through the system. Together, Dr. Android and Mr. Hide can completely remove several of an app’s existing permissions and replace them with finer-grained ones, leveraging the platform to provide complete mediation for protected resources. We evaluated our ideas on several popular, free Android apps. We found that we can replace many commonly used "dangerous" permissions with finer-grained permissions. Moreover, apps transformed to use these finer-grained permissions run largely as expected, with reasonable performance overhead.
  • 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.