| Hidden Process Models |
18 Dec 2009 |
190 pages |
| Authors:
Rebecca A Hutchinson; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
 | This thesis introduces Hidden Process Models (HPMs). HPMs are a probabilistic time series model for data assumed to be generated by a set of processes, where each process is characterized by a unique spatial-temporal signature and a probability distribution over its timing relative to a set of known timing landmarks. Research on HPMs has been inspired and motivated by the functional Magnetic Resonance Imaging (fMRI) domain, and this document presents, ... |
|
| Proof Theory for Authorization Logic and Its Application to a Practical File System |
Dec 2009 |
301 pages |
| Authors:
Deepak Garg; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| In most computer systems, users' access to resources is controlled using authorization policies. Logic is an appropriate medium for representing, understanding, and enforcing authorization policies, yet despite several years of pragmatic work on the subject, the foundations of relevant logics remain unexplored and poorly understood. It is in this realm that the work of this thesis lies; the thesis explores the theory of logics for expressing authorization policies as well ... |
|
| CZ: Multimethods and Multiple Inheritance Without Diamonds |
Dec 2009 |
49 pages |
| Authors:
Jonathan Aldrich; Donna Malayeri; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Multiple inheritance has long been plagued with the diamond inheritance problem, leading to solutions that restrict expressiveness, such as mixins and traits. Instead, we address the diamond problem directly, considering two difficulties it causes: ensuring a correct semantics for object initializers, and typechecking multiple dispatch in a modular fashion--the latter problem arising even with multiple interface inheritance. We show that previous solutions to these problems are either unsatisfactory or cumbersome, ... |
|
| Probabilistic Plan Management |
17 Nov 2009 |
215 pages |
| Authors:
Laura M Hiatt; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The general problem of planning for uncertain domains remains a difficult challenge. Research that focuses on constructing plans by reasoning with explicit models of uncertainty has produced some promising mechanisms for coping with specific types of domain uncertainties; however, these approaches generally have difficulty scaling. Research in robust planning has alternatively emphasized the use of deterministic planning techniques, with the goal of constructing a flexible plan (or set of plans) ... |
|
| PCAL: Language Support for Proof-Carrying Authorization Systems |
16 Oct 2009 |
33 pages |
| Authors:
Deepak Garg; Avik Chaudhuri; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| By shifting the burden of proofs to the user, a proof-carrying authorization (PCA) system can automatically enforce complex access control policies. Unfortunately, managing those proofs can be a daunting task for the user. In this paper we develop a Bash-like language, PCAL, that can automate correct and efficient use of a PCA interface. Given a PCAL script, the PCAL compiler tries to statically construct the proofs required for executing the ... |
|
| 300 Cities Virtual Experiment |
Sep 2009 |
28 pages |
| Authors:
Neal Altman; Kathleen M Carley; Michael K Martin; Jessica McGillen; Dawn Robertson; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This report provides an overview of the preparations required for the virtual experiment we will conduct for the IRS as part of the 300 cities subproject. We briefly describe the tax gap and taxpayer issues, our revised approach, the Construct framework and the models developed for the multi-agent simulation. Where appropriate, we provide references to other technical reports that describe in more detail the models for intentional and inadvertent taxpayer ... |
|
| Variables, Decisions, and Scripting in Construct |
Sep 2009 |
69 pages |
| Authors:
Kathleen M Carley; Brian R Hirshman; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Simulation designers benefit from a flexible system for creating scenarios that are easy to modify, expressive, and allow for more complex interventions to be assessed. This technical report introduces a C-like scripting language that can be used with Construct in order to support numeric variables as well as user-specified decisions. This scripting language can be used to specify outputs in a targeted manner, allowing the user to modify the type ... |
|
| Modeling Behavior and Variation for Crowd Animation |
Aug 2009 |
120 pages |
| Authors:
Manfred C ManLau; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The simulation of crowds of virtual characters is needed for applications such as films, games, and virtual reality environments. These simulations are difficult due to the large number of characters to be simulated and the requirement for synthesizing realistic human-like motion efficiently. This thesis focuses on two problems: how to search through and select motion clips of behaviors so that human-like motion can be generated for multiple characters interactively, and ... |
|
| A Logical Representation of Common Rules for Controlling Access to Classified Information |
19-Jun-2009 |
25 pages |
| Authors:
Frank Pfenning; Deepak Garg; Denis Serenyi; Brian Witten; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Official policies for controlling access to classified information in the U.S. are quite complex and often difficult to enforce. We present an encoding of a common core of these policies in an authorization logic, and describe their rigorous enforcement in PCFS, a file system implemented for such purposes. |
|
| Principal-Centric Reasoning in Constructive Authorization Logic |
14-Apr-2009 |
126 pages |
| Authors:
Deepak Garg; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We present an authorization logic DTL(o) that explicitly relativizes reasoning to beliefs of principals. The logic assumes that principals are conceited in their beliefs. We describe the natural deduction system, sequent calculus, Hilbert-style axiomatization, and Kripke semantics of the logic. We prove several meta-theoretic results including cut-elimination, and soundness and completeness for the Kripke semantics. Translations from several other authorization logics into DTL(o), as well as formal connections between DTL(o) ... |
|
| Trust Me: Design Patterns for Constructing Trustworthy Trust Indicators |
Apr-2009 |
259 pages |
| Authors:
Serge Egelman; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| In a world where making an incorrect online trust decision can mean giving away highly personal information to a con artist, Internet users need effective online trust indicators to help them make better trust decisions. In a perfect world, software could automatically detect all security threats and then block access to high risk web sites. Because there are many threats that we cannot detect with 100% accuracy and false positives ... |
|
| Simultaneous Placement and Scheduling of Sensors |
01-Oct-2008 |
33 pages |
| Authors:
Andreas Krause; Ram Rajagopal; Anupam Gupta; Carlos Guestrin; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We consider the problem of monitoring spatial phenomena, such as road speeds on a highway, using wireless sensors with limited battery life. A central question is to decide where to locate these sensors to best predict the phenomenon at the unsensed locations. However, given the power constraints, we also need to determine when to selectively activate these sensors in order to maximize the performance while satisfying lifetime requirements. Traditionally, these ... |
|
| Analysis and Defense of Vulnerabilities in Binary Code |
29-Sep-2008 |
156 pages |
| Authors:
David Brumley; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| In this thesis, we develop techniques for vulnerability analysis and defense that only require access to vulnerable programs in binary form. Our approach does not use or require source code. We focus on a binary-centric approach since everyone typically has access to the binary code for the programs they run. Thus, our approach is applicable to a wider audience than previous approaches that require or utilize source code. In addition, ... |
|
| Traffic Analysis for Network Security using Learning Theory and Streaming Algorithms |
Sep-2008 |
149 pages |
| Authors:
Shobha Venkataraman; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| A recurring problem in network traffic analysis is to automatically distinguish legitimate traffic from malicious or spurious traffic. This problem arises in several guises in network security (e.g., spam mitigation, worm detection), and is, at core, a machine learning or data mining problem. However, traffic analysis for network security has many fundamental challenges that are not present in typical machine learning or data mining problems, and a blackbox application of ... |
|
| Verification using Satisfiability Checking, Predicate Abstraction, and Craig Interpolation |
Sep-2008 |
297 pages |
| Authors:
Himanshu Jain; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Automatic verification of hardware and software implementations is crucial for computer systems. This thesis develops new techniques for building efficient decision procedures and adds new capabilities to existing decision procedures. Most SAT solvers require the input formula to be in Conjunctive Normal Form (CNF). However, typical formulas that arise in practice are not in CNF. Converting a general formula to CNF introduces overhead in the form of new variables and ... |
|
| Expandable Grids: A User Interface Visualization Technique and a Policy Semantics to Support Fast, Accurate Security and Privacy Policy Authoring |
01-Jul-2008 |
208 pages |
| Authors:
Robert W Reeder; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This thesis addresses the problem of designing user interfaces to support creating, editing, and viewing security and privacy policies. Policies are declarations of who may access what under which conditions. Creating, editing, and viewing in a word, authoring accurate policies is essential to keeping resources both available to those who are authorized to use them and secure from those who are not. User interfaces for policy authoring can greatly affect ... |
|
| Automap User's Guide 2008 |
01-Jul-2008 |
232 pages |
| Authors:
Jana Diesner; Kathleen M Carley; Dave Columbus; Matthew J DeReno; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| AutoMap is software for computer-assisted Network Text Analysis (NTA). NTA encodes the links among words in a text and constructs a network of the linked words. AutoMap subsumes classical Content Analysis by analyzing the existence, frequencies, and covariance of terms and themes. |
|
| ORA User's Guide 2008 |
01-Jul-2008 |
589 pages |
| Authors:
Jeff Reminga; Il-Chul Moon; Matt DeReno; Kathleen M Carley; Dave Columbus; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| ORA is a network analysis tool that detects risks or vulnerabilities of an organization's design structure. The design structure of an organization is the relationship among its personnel, knowledge, resources, and tasks entities. These entities and relationships are represented by the Meta-Matrix. Measures that take as input a Meta-Matrix are used to analyze the structural properties of an organization for potential risk. ORA contains over 100 measures which are categorized ... |
|
| Effective Motion Tracking Using Known and Learned Actuation Models |
06-Jun-2008 |
137 pages |
| Authors:
Yang Gu; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Robots need to track objects. We consider tasks where robots actuate on the target that is visually tracked. Object tracking efficiency completely depends on the accuracy of the motion model and of the sensory information. The motion model of the target becomes particularly complex in the presence of multiple agents acting on a mobile target. We assume that the tracked object is actuated by a team of agents, composing of ... |
|
| Checking Temporal Relations between Multiple Objects |
01-Jun-2008 |
29 pages |
| Authors:
Jonathan Aldrich; Ciera Jaspan; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Software frameworks contain constraints with unusual properties. The constraints frequently span multiple objects and classes, and they change according to the current context. Additionally, they may not be enforced at the same point where they were specified or broken, thus causing unexpected runtime errors. This paper describes a lightweight specification system to describe multi- object temporal constraints. It also provides a detailed description of a static analysis to check that ... |
|
| OraGIS and Loom: Spatial and Temporal Extensions to the ORA Analysis Platform |
01-Jun-2008 |
18 pages |
| Authors:
George B Davis; Jamie Olson; Kathleen M Carley; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Increasingly, data available to network analysts includes not only relationships between actors but measurements of entity attributes and relations through time and space. Integrating this information with existing dynamic network analysis techniques demands new models and tools. This paper introduces two extensions to the ORA dynamic network analysis platform intended to meet this need. The first, OraGIS, provides geospatial visualization and clustering algorithms. The second, Loom, assists in the analysis ... |
|
| Error Reporting Logic |
01-Jun-2008 |
22 pages |
| Authors:
Jonathan Aldrich; Ciera Jaspan; Trisha Quan; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| When a system fails to meet its specification, it can be difficult to find the source of the error and detenmue how to fix it. In this paper, we introduce error reporting logic (ERL), an algorithm and tool that produces succinct explanations for why a target system violates a specification expressed in first order predicate logic. ERL analyzes the specification to determine which parts contrbuted to the failure, and it ... |
|
| Relational Learning via Collective Matrix Factorization |
01-Jun-2008 |
27 pages |
| Authors:
Ajit P Singh; Geoffrey J Gordon; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Relational learning is concerned with predicting unknown values of a relation, given a database of entities and observed relations among entities. An example of relational learning is movie rating prediction, where entities could include users, movies, genres, and actors. Relations would then encode users' ratings of movies, movies' genres, and actors' roles in movies. A common prediction technique given one pairwise relation, for example a #users x #movies ratings matrix, ... |
|
| A Logic for Reasoning About Time-Dependent Access Control Policies |
20-May-2008 |
79 pages |
| Authors:
Henry DeYoung; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Allowing access to resources, including data and hardware, without compromising their security is a fundamental challenge in computer science. Because of the number and complexity of authorization policies in access control systems, it is clear that ad hoc methods for specifying and enforcing policies cannot inspire a high degree of trust. Authorization logics have been proposed as a theoretically sound alternative. However, for an authorization logic to be useful in ... |
|
| Data Analysis Project: Leveraging Massive Textual Corpora Using n-Gram Statistics |
01-May-2008 |
31 pages |
| Authors:
Ian Fette; Andrew Carlson; Tom M Mitchell; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We study methods of efficiently leveraging massive textual corpora through n-gram statistics. Specifically, we explore algorithms that use a database of frequency counts for sequences of tokens in a teraword Web corpus to correct spelling mistakes and to extract a list of instances of some category given only the name of the target category. For spelling correction, we use a novel correction algorithm and demonstrate high accuracy in correcting both ... |
|
| Conditional Random Fields for Activity Recognition |
01-Apr-2008 |
205 pages |
| Authors:
Douglas L Vail; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| To act intelligently in presence of others, robots must use information from their sensors to recognize behaviors and activities of other agents in their environment. We explore how to bridge the gap from noisy, continuous observations about the world to high-level, discrete activity labels. We contribute the use of conditional random fields (CRFs) for activity recognition in multirobot domains. We explore appropriateness of CRFs with an empirical comparison to hidden ... |
|
| Social Network Change Detection |
17-Mar-2008 |
27 pages |
| Authors:
Kathleen M Carley; Ian A McCulloh; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Changes in observed social networks may signal an underlying change within an organization, and may even predict significant events or behaviors. The breakdown of a team's effectiveness, the emergence of informal leaders, or the preparation of an attack by a clandestine network may all be associated with changes in the patterns of interactions between group members. The ability to systematically, statistically, effectively and efficiently detect these changes has the potential ... |
|
| Random Graph Standard Network Metrics Distributions in ORA |
01-Mar-2008 |
34 pages |
| Authors:
Kathleen M Carley; Eunice J Kim; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Networks, and the nodes within them, are often characterized using a series of metrics. Illustrative graph level metrics are the characteristic path length and the clustering co-efficient. Illustrative node level metrics are degree centrality, betweenness centrality, closeness centrality, and eigenvector centrality. A key issue in using these metrics is how to interpret the values; e.g., is a degree centrality of .2 high? With normalized values, we know that these metrics ... |
|
| Static Extraction of Object-Oriented Runtime Architectures |
Mar-2008 |
55 pages |
| Authors:
Jonathan Aldrich; Marwan Abi-Antoun; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| For many object-oriented systems, it is useful to have a runtime architecture, that shows networks of objects. But it is hard to statically extract runtime object graphs that provide architectural abstraction from an arbitrary program written in a general purpose language that follows common design idioms. Previous approaches extract low-level non-hierarchical object graphs that do not provide architectural abstraction, change the language too radically for many existing implementations, or use ... |
|
| An Authorization Logic with Explicit Time |
02 FEB 2008 |
96 pages |
| Authors:
Henry DeYoung; Deepak Garg; Frank Pfenning; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We present an authorization logic that permits reasoning with explicit time. Following a proof-theoretic approach, we study the meta-theory of the logic, including cut elimination. We also demonstrate formal connections to proof-carrying authorization's existing approach for handling time and comment on the enforceability of our logic in the same framework. Finally, we illustrate including those with complex interactions between time, authorization, and mutable state. |
|
| Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations |
FEB 2008 |
40 pages |
| Authors:
Himanshu Jain; Edmund M. Clarke; Orna Grumberg; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The use of Craig interpolants has enabled the development of powerful hardware and software model checking techniques. Efficient algorithms are known for computing interpolants in rational and real linear arithmetic. We focus on subsets of integer linear arithmetic. Our main results are polynomial time algorithms for obtaining proofs of unsatisfiability and interpolants for conjunctions of linear diophantine equations linear modular equations (linear congruences), and linear diophantine disequations. We show the ... |
|
| Computing Differential Invariants of Hybrid Systems as Fixedpoints |
FEB 2008 |
35 pages |
| Authors:
Andre Platzer; Edmund M. Clarke; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations that have right-hand sides that are polynomials in the state variables. In order to verify non-trivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in ... |
|
| From Indexed Lax Logic to Intuitionistic Logic |
07 JAN 2008 |
37 pages |
| Authors:
Deepak Garg; Michael C. Tschantz; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We present translations from a logic with indexed lax modalities to first-order intuitionistic logic and intuitionistic linear logic. These translations rely on a continuation passing style encoding for the lax modalities. We show that our translations preserve provability of formulas. |
|
| A Constraint Generation Approach to Learning Stable Linear Dynamical Systems |
JAN 2008 |
17 pages |
| Authors:
Sajid M. Siddiqi; Byron Boots; Geoffrey J. Gordon; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Stability is a desirable characteristic for linear dynamical systems, but it is often ignored by algorithms that learn these systems from data. We propose a novel method for learning stable linear dynamical systems: we formulate an approximation of the problem as a convex program, start with a solution to a relaxed version of the program, and incrementally add constraints to improve stability. Rather than continuing to generate constraints until we ... |
|
| An Online Algorithm for Maximizing Submodular Functions |
20 DEC 2007 |
40 pages |
| Authors:
Matthew Streeter; Daniel Golovin; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We consider the following two problems. We are given as input a set of activities and a set of jobs to complete. Our goal is to devise a schedule for allocating time to the various activities so as to achieve one of two objectives: minimizing the average time required to complete each job, or maximizing the number of jobs completed within a fixed time. Formally, a schedule is a sequence ... |
|
| Using Online Algorithms to Solve NP-Hard Problems More Efficiently in Practice |
DEC 2007 |
206 pages |
| Authors:
Matthew Streeter; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This thesis develops online algorithms that can be used to solve a wide variety of NP-hard problems more efficiently in practice. The common approach taken by all our online algorithms is to improve the performance of one or more existing algorithms for a specific NP-hard problem by adapting the algorithms to the sequence of problem instance(s) they are run on. We begin by presenting an algorithm for solving a specific ... |
|
| Checking and Measuring the Architectural Structural Conformance of Object-Oriented Systems |
DEC 2007 |
52 pages |
| Authors:
Marwan Abi-Antoun; Jonathan Aldrich; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The benefits of architectural analyses are only achieved if one can guarantee that the implementation conforms to the architecture. We propose an approach for checking and measuring the structural conformance of a software system's implementation to its execution architecture. In contrast to existing approaches, our approach uses static analyses, and works with existing Java-like programming languages, existing object-oriented designs and existing integrated development environments. We address the problem with a ... |
|
| Beyond Brain Blobs: Machine Learning Classifiers as Instruments for Analyzing Functional Magnetic Resonance Imaging Data |
DEC 2007 |
213 pages |
| Authors:
Francisco Pereira; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The thesis put forth in this dissertation is that machine learning classifiers can be used as instruments for decoding variables of interest from functional magnetic resonance imaging (fMRI) data. There are two main goals in decoding Showing that the variable of interest can be predicted from the data in a statistically reliable manner (i.e. there's enough information present). Shedding light on how the data encode the information needed to predict, ... |
|
| Actively Learning Specific Function Properties with Applications to Statistical Inference |
DEC 2007 |
214 pages |
| Authors:
Brent Bryan; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Active learning techniques have previously been shown to be extremely effective for learning a target function over an entire parameter space based on a limited set of observations. However, in many cases, only a specific property of the target function needs to be learned. For instance, when discovering the boundary of a region such as the locations in which the wireless network strength is above some operable level, we are ... |
|
| Improving Mobile Infrastructure for Pervasive Personal Computing |
NOV 2007 |
77 pages |
| Authors:
Ajay Surie; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The emergence of pervasive computing systems such as Internet Suspend/Resume has facilitated ubiquitous access to a user's personalized computing environment by layering virtual machine technology on top of distributed storage. This usage model poses several new challenges, such as establishing trust in unmanaged hardware that a user may access, and efficiently migrating virtual machine "VM" state across low-bandwidth networks. This document describes Trust-Sniffer, a tool that reduces the security risks ... |
|
| Free LittleDog!: Towards Completely Untethered Operation of the LittleDog Quadruped |
AUG 2007 |
67 pages |
| Authors:
Michael N. Dille; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| The LittleDog robot is a 12 degree-of-freedom quadruped developed by Boston Dynamics and selected for use in the DARPA Learning Locomotion program, in which machine learning is applied to develop controllers capable of navigating rocky terrain. Presently, it is typically constrained to operate within wireless range of a host desktop computer and within a fixed workspace surrounded by a motion capture system that globally localizes the robot and specially marked ... |
|
| An Approach to Measuring a System's Attack Surface |
AUG 2007 |
30 pages |
| Authors:
Pratyusa K. Manadhata; Kymie M. Tan; Roy A. Maxion; Jeannette M. Wing; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Practical software security measurements and metrics are critical to the improvement of software security. We propose a metric to determine whether one software system is more secure than another similar system with respect to their attack surface. We use a system's attack surface measurement as an indicator of the system's security; the larger the attack surface, the more insecure the system. We measure a system's attack surface in terms of ... |
|
| Specifying Agents in Construct |
25-Jul-2007 |
70 pages |
| Authors:
Kathleen M Carley; Brian R Hirshman; Michael J Kowalchuck; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Construct is a multi-agent simulation tool that is commonly used to investigate dynamic behavior in complex socio-cultural systems. This technical report describes the parameters necessary to specify agents in the simulation, focusing especially on the features which help describe agent behavior. It also introduces a number of pre-defined agent classes, stock-agents which can be used to quickly build up a simulation. This document is intended both as an introduction to ... |
|
| Coordinated Sampling: An Efficient, Network-Wide Approach for Flow Monitoring |
16 JUL 2007 |
30 pages |
| Authors:
Vyas Sekar; Michael K. Reiter; Walter Willinger; Hui Zhang; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We present Coordinated Sampling, a new technique for improved flow-level monitoring. Our approach derives from three key design decisions: flow sampling instead of uniform packet sampling; hash-based flow selection to achieve coordination between routers without needing explicit communication channels; and an approach for distributing responsibilities across routers to achieve network-wide monitoring objectives while taking into account resource constraints on each router. We demonstrate that Coordinated Sampling presents an attractive solution ... |
|
| A Formal Model for a System's Attack Surface |
JUL 2007 |
22 pages |
| Authors:
Pratysua K. Manadhata; Dilsun K. Kaynar; Jeannette M. Wing; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Practical software security metrics and measurements are essential to the development of secure software [18]. In this paper, we propose to use a software system's attack surface measurement as an indicator of the system's security; the larger the attack surface, the more insecure the system. We formalize the notion of a system's attack surface using an I/O automata model of the system [15] and define a quantitative measure of the ... |
|
| Is Host-Based Anomaly Detection + Temporal Correlation = Worm Causality |
06 MAR 2007 |
30 pages |
| Authors:
Vyas Sekar; Yinglian Xie; Michael K. Reiter; Hui Zhang; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| Epidemic-spreading attacks (e.g., worm and botnet propagation) have a natural notion of attack causality - a single network flow causes a victim host to get infected and subsequently spread the attack. This paper is motivated by a simple question regarding the diagnosis of such attacks - is it possible to establish attack-causality through network-level monitoring, without relying on signatures and attack-specific properties? Using the observation that communication patterns of normal ... |
|
| Modular Typestate Verification of Aliased Objects |
MAR 2007 |
51 pages |
| Authors:
Kevin Bierhoff; Jonathan Aldrich; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| A number of type systems have used typestates to specify and statically verify protocol compliance. Aliasing is a major challenge for these systems. This paper proposes a modular type system for a core object-oriented language that leverages linear logic for verifying compliance to more expressive protocol specifications than previously supported. The system improves reasoning about aliased objects by associating references with access permissions that systematically capture what aliases know about ... |
|
| Confidentiality Policies and Their Extraction from Programs |
09 FEB 2007 |
38 pages |
| Authors:
Michael C. Tschantz; Jeannette M. Wing; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| We examine a well known confidentiality requirement called noninterference and argue that many systems do not meet this requirement despite maintaining the privacy of its users. We discuss a weaker requirement called incident-insensitive noninterference that captures why these systems maintain the privacy of its users while possibly not satisfying noninterference. We extend this requirement to depend on dynamic information in a novel way. Lastly, we present a method based on ... |
|
| Real-Time Motion Planning and Safe Navigation in Dynamic Multi-Robot Environments |
15 DEC 2006 |
205 pages |
| Authors:
James R. Bruce; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| All mobile robots share the need to navigate, creating the problem of motion planning. In multi-robot domains with agents acting in parallel, highly complex and unpredictable dynamics can arise. This leads to the need for navigation calculations to be carried out within tight time constraints, so that they can be applied before the dynamics of the environment make the calculated answer obsolete. At the same time, we want the robots ... |
|
| Bayesian Mixed-Membership Models of Complex and Evolving Networks |
01-Dec-2006 |
234 pages |
| Authors:
Edoardo M Airoldi; CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
|
| This thesis provides a methodological framework for the statistical analysis of complex graphs and dynamic networks.1 In it, I develop probabilistic algorithms that generate, evolve and integrate a heterogeneous collection of graphs, I study the statistical models these algorithms implicitly specify, and I develop strategies for estimating the set of quantities on which they depend in the context of applications to social and biological networks. |
|
Reports by Corporate Author
