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

Start date: 2000End date: 2009

Search Results

Now showing 1 - 10 of 462
  • Thumbnail Image
    Item
    SCanDroid: Automated Security Certification of Android
    (2009-11-20) Fuchs, Adam P.; Chaudhuri, Avik; Foster, Jeffrey S.
    Android is a popular mobile-device platform developed by Google. Android’s application model is designed to encourage applications to share their code and data with other applications. While such sharing can be tightly controlled with permissions, in general users cannot determine what applications will do with their data, and thereby cannot decide what permissions such applications should run with. In this paper we present SCANDROID, a tool for reasoning automatically about the security of Android applications. SCanDroid’s analysis is modular to allow incremental checking of applications as they are installed on an Android device. It extracts security specifications from manifests that accompany such applications, and checks whether data flows through those applications are consistent with those specifications. To our knowledge, SCanDroid is the first program analysis tool for Android, and we expect it to be useful for automated security certification of Android applications.
  • Thumbnail Image
    Item
    An Analysis of Derived Belief Strategy’s Performance in the 2005 Iterated Prisoner’s Dilemma Competition
    (2006-02-19) Au, Tsz-Chiu
    This report analyze the performance of the Derived Belief Strategy (DBS) in the 2005 Iterated Prisoner’s Dilemma Competition [1]. Our technique is to remove the participants from the computation of the average scores, as if they have never participated in the competition.
  • Thumbnail Image
    Item
    Appendix to CMod: Modular Information Hiding and Type-Safe Linking for C
    (2007-06-30) Srivastava, Saurabh; Hicks, Michael; Foster, Jeffrey S.
    This brief note is an appendix to the paper "CMod: Modular Information Hiding and Type-Safe Linking for C." It consists of the proof of soundness for the formal language presented in that paper.
  • Thumbnail Image
    Item
    Cmod: Modular Information Hiding and Type-Safe Linking for C
    (2006-07-31) Srivastava, Saurabh; Hicks, Michael; Foster, Jeffrey S.
    This paper presents CMod, a novel tool that provides a sound module system for C. CMod works by enforcing a set of four rules that are based on principles of modular reasoning and on current programming practice. CMod's rules flesh out the convention that .h header files are module interfaces and .c source files are module implementations. Although this convention is well-known, developing CMod's rules revealed there are many subtleties in applying the basic pattern correctly. We have proven formally that CMod's rules enforce both information hiding and type-safe linking. We evaluated CMod on a number of benchmarks, and found that most programs obey CMod's rules, or can be made to with minimal effort, while rule violations reveal brittle coding practices including numerous information hiding violations and occasional type errors.
  • Thumbnail Image
    Item
    Compressing Kinetic Data From Sensor Networks
    (2009-09-14) Friedler, Sorelle A.; Mount, David M.
    We introduce a framework for storing and processing kinetic data observed by sensor networks. These sensor networks generate vast quantities of data, which motivates a significant need for data compression. We are given a set of sensors, each of which continuously monitors some region of space. We are interested in the kinetic data generated by a finite set of objects moving through space, as observed by these sensors. Our model relies purely on sensor observations; it allows points to move freely and requires no advance notification of motion plans. Sensor outputs are represented as random processes, where nearby sensors may be statistically dependent. We model the local nature of sensor networks by assuming that two sensor outputs are statistically dependent only if the two sensors are among the k nearest neighbors of each other. We present an algorithm for the lossless compression of the data produced by the network. We show that, under the statistical dependence and locality assumptions of our framework, asymptotically this compression algorithm encodes the data to within a constant factor of the information-theoretic lower bound optimum dictated by the joint entropy of the system. In order to justify our locality assumptions, we provide a theoretical comparison with a variant of the kinetic data structures framework. We prove that the storage size required by an optimal system operating under our locality assumptions is on the order of the size required by our variant. Additionally, we provide experimental justification for our locality assumptions.
  • Thumbnail Image
    Item
    Learning and Verification of Safety Parameters for Airspace Deconfliction
    (2009-11-30) Rebguns, Antons; Green, Derek; Levine, Geoffrey; Kuter, Ugur; Spears, Diana
    We present a Bayesian approach to learning flexible safety constraints and subsequently verifying whether plans satisfy these constraints. Our approach, called the Safety Constraint Learner/Checker (SCLC), is embedded within the Generalized Integrated Learning Architecture (GILA), which is an integrated, heterogeneous, multi-agent ensemble architecture designed for learning complex problem solving techniques from demonstration by human experts. The SCLC infers safety constraints from a single expert demonstration trace, and applies these constraints to the solutions proposed by the agents in the ensemble. Blame for constraint violations is then transmitted to the individual learning/planning/reasoning agents, thereby facilitating new problem-solving episodes. We discuss the advantages of the SCLC and demonstrate empirical results on an Airspace Planning and Deconfliction Task, which was a benchmark application in the DARPA Integrated Learning Program.
  • Thumbnail Image
    Item
    A Testing Based Empirical Study of Dynamic Software Update Safety Restrictions
    (2009-10-16) Hayden, Christopher M.; Hardisty, Eric A.; Hicks, Michael; Foster, Jeffrey S.
    Recent years have seen significant advances in dynamic software updating (DSU) systems, which allow programs to be patched on the fly. Most DSU systems employ automatic safety checks to avoid applying a patch if doing so may lead to incorrect behavior. This paper presents what we believe is the first comprehensive empirical evaluation of the two most significant DSU safety checks: activeness safety (AS), which disallows patches that modify functions on the stack, and con-freeness safety (CFS), which allows modifications to active functions, but only when doing so will be type safe. To measure the checks' effectiveness, we tested them against three years of updates to Open-SSH and vsftpd. We performed this testing using a novel DSU testing methodology that systematically applies updates throughout the execution of a test suite. After testing updates to both applications in this way, we tracked how often the safety checks allow updates and which updates result in test failures. We found that updating without safety checks produced many failures, and that both AS and CFS dramatically reduced, but did not fully eliminate, these failures. CFS yielded more failures than AS, but AS was more restrictive than CFS, disallowing far more successful updates. Our results suggest that neither AS nor CFS is likely suitable for general-purpose DSU on its own. Indeed, we found that selecting update points manually could avoid all failures while still permitting sufficient updates. Our results present a challenge and important insights for future work: to discover safe and sufficient update points fully automatically.
  • Thumbnail Image
    Item
    Extending Phrase-Based Decoding with a Dependency-Based Reordering Model
    (2009-12-23) Hunter, Tim; Resnik, Philip
    Phrase-based decoding is conceptually simple and straightforward to implement, at the cost of drastically oversimplified reordering models. Syntactically aware models make it possible to capture linguistically relevant relationships in order to improve word order, but they can be more complex to implement and optimise. In this paper, we explore a new middle ground between phrase-based and syntactically informed statistical MT, in the form of a model that supplements conventional, non-hierarchical phrase-based techniques with linguistically informed reordering based on syntactic dependency trees. The key idea is to exploit linguistically-informed hierarchical structures only for those dependencies that cannot be captured within a single flat phrase. For very local dependencies we leverage the success of conventional phrase-based approaches, which provide a sequence of target-language words appropriately ordered and ready-made with the appropriate agreement morphology. Working with dependency trees rather than constituency trees allows us to take advantage of the flexibility of phrase-based systems to treat non-constituent fragments as phrases. We do impose a requirement --- that the fragment be a novel sort of "dependency constituent" --- on what can be translated as a phrase, but this is much weaker than the requirement that phrases be traditional linguistic constituents, which has often proven too restrictive in MT systems.
  • Thumbnail Image
    Item
    Using Symbolic Evaluation to Understand Behavior in Configurable Software Systems
    (2009-12-12) Reisner, Elnatan; Song, Charles; Ma, Kin-Keung; Foster, Jeffrey S.; Porter, Adam
    Many modern software systems are designed to be highly configurable, which increases flexibility but can make programs hard to test, analyze, and understand. We present an initial empirical study of how configuration options affect program behavior. We conjecture that, at certain levels of abstraction, configuration spaces are far smaller than the worst case, in which every configuration is distinct. We evaluated our conjecture by studying three configurable software systems: vsftpd, ngIRCd, and grep. We used symbolic evaluation to discover how the settings of run-time configuration options affect line, basic block, edge, and condition coverage for our subjects under a given test suite. Our results strongly suggest that for these subject programs, test suites, and configuration options, when abstracted in terms of the four coverage criteria above, configuration spaces are in fact much smaller than combinatorics would suggest and are effectively the composition of many small, self-contained groupings of options.
  • Thumbnail Image
    Item
    Scaling Single-Program Performance on Large-Scale Chip Multiprocessors
    (2009-11-25) Wu, Meng-Ju; Yeung, Donald
    Due to power constraints, computer architects will exploit TLP instead of ILP for future performance gains. Today, 4-8 state-of-the-art cores or 10s of smaller cores can fit on a single die. For the foreseeable future, the number of cores will likely double with each successive processor generation. Hence, CMPs with 100s of cores-so-called large-scale chip multiprocessors (LCMPs)-will become a reality after only 2 or 3 generations. Unfortunately, simply scaling the number of on-chip cores alone will not guarantee improved performance. In addition, effectively utilizing all of the cores is also necessary. Perhaps the greatest threat to processor utilization will be the overhead incurred waiting on the memory system, especially as on-chip concurrency scales to 100s of threads. In particular, remote cache bank access and off-chip bandwidth contention are likely to be the most significant obstacles to scaling memory performance. This paper conducts an in-depth study of CMP scalability for parallel programs. We assume a tiled CMP in which tiles contain a simple core along with a private L1 cache and a local slice of a shared L2 cache. Our study considers scaling from 1-256 cores and 4-128MB of total L2 cache, and addresses several issues related to the impact of scaling on off-chip bandwidth and on-chip communication. In particular, we find off-chip bandwidth increases linearly with core count, but the rate of increase reduces dramatically once enough L2 cache is provided to capture inter-thread sharing. Our results also show for the range 1-256 cores, there should be ample on-chip bandwidth to support the communication requirements of our benchmarks. Finally, we find that applications become off-chip limited when their L2 cache miss rates exceed some minimum threshold. Moreover, we expect off-chip overheads to dominate on-chip overheads for memory intensive programs and LCMPs with aggressive cores.