DRUM :: Browsing by Author "Hicks, Michael"

Browsing by Author "Hicks, Michael"

Now showing 1 - 20 of 27

Adapting Scrum to Managing a Research Group
(2010-09-18) Hicks, Michael; Foster, Jeffrey S.
Score is an adaptation of the Scrum agile software development methodology to the task of managing Ph.D. students in an academic research group. This paper describes Score, conceived in October 2006, and our experience using it. We have found that Score enables us---faculty and students---to be more efficient and thereby more productive, and enhances the cohesion of our research group.
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.
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.
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.
Automating NISQ Application Design with Meta Quantum Circuits with Constraints (MQCC)
(Association for Computer Machinery (ACM), 2023-04) Deng, Haowei; Peng, Yuxiang; Hicks, Michael; Wu, Xiaodi
Near-term intermediate scale quantum (NISQ) computers are likely to have very restricted hardware resources, where precisely controllable qubits are expensive, error-prone, and scarce. Programmers of such computers must therefore balance trade-offs among a large number of (potentially heterogeneous) factors specific to the targeted application and quantum hardware. To assist them, we propose Meta Quantum Circuits with Constraints (MQCC), a meta-programming framework for quantum programs. Programmers express their application as a succinct collection of normal quantum circuits stitched together by a set of (manually or automatically) added meta-level choice variables, whose values are constrained according to a programmable set of quantitative optimization criteria. MQCC’s compiler generates the appropriate constraints and solves them via an SMT solver, producing an optimized, runnable program. We showcase a few MQCC’s applications for its generality including an automatic generation of efficient error syndrome extraction schemes for fault-tolerant quantum error correction with heterogeneous qubits and an approach to writing approximate quantum Fourier transformation and quantum phase estimation that smoothly trades off accuracy and resource use. We also illustrate that MQCC can easily encode prior one-off NISQ application designs-–multi-programming (MP), crosstalk mitigation (CM)—as well as a combination of their optimization goals (i.e., a combined MP-CM).
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.
Contextual Effects for Version-Consistent Dynamic Software Updating and Safe Concurrent Programming
(2007-11-01) Neamtiu, Iulian; Hicks, Michael; Foster, Jeffrey S.; Pratikakis, Polyvios
This paper presents a generalization of standard effect systems that we call contextual effects. A traditional effect system computes the effect of an expression e. Our system additionally computes the effects of the computational context in which e occurs. More specifically, we compute the effect of the computation that has already occurred (the prior effect) and the effect of the computation yet to take place (the future effect). Contextual effects are useful when the past or future computation of the program is relevant at various program points. We present two substantial examples. First, we show how prior and future effects can be used to enforce transactional version consistency (TVC), a novel correctness property for dynamic software updates. TVC ensures that programmer-designated transactional code blocks appear to execute entirely at the same code version, even if a dynamic update occurs in the middle of the block. Second, we show how future effects can be used in the analysis of multi-threaded programs to find thread-shared locations. This is an essential step in applications such as data race detection.
Defeating Script Injection Attacks with Browser Enforced Embedded Policies
(2006-11-02) Trevor, Jim; Swamy, Nikhil; Hicks, Michael
Web sites that accept and display content such as wiki articles or comments typically filter the content to prevent injected script code from running in browsers that view the site. The diversity of browser rendering algorithms and the desire to allow rich content makes filtering quite difficult, however, and attacks such as the Samy and Yamanner worms have exploited filtering weaknesses. To solve this problem, this paper proposes a simple mechanism called Browser-Enforced Embedded Policies (BEEP). The idea is that a web site can embed a policy inside its pages that specifies which scripts are allowed to run. The browser, which knows exactly when it will run a script, can enforce this policy perfectly. We have added BEEP support to several browsers, and built tools to simplify adding policies to web applications. We found that supporting BEEP in browsers requires only small and localized modifications, modifying web applications requires minimal effort, and enforcing policies is generally lightweight.
Directed symbolic execution
(2011-04-07) Ma, Kin-Keung; Khoo, Yit Phang; Foster, Jeffrey S.; Hicks, Michael
In this paper, we study the problem of automatically finding program executions that reach a particular target line. This problem arises in many debugging scenarios, e.g., a developer might learn that a failure is possible on a particular line but might not know exactly how to reproduce the failure or even whether it is reproducible. This can happen particularly often for bug reports from static analysis tools, which can produce false positives. We propose two new directed symbolic execution strategies that aim to solve this problem: shortest-distance symbolic execution (SDSE) uses a distance metric in an interprocedural control flow graph to guide symbolic execution toward a particular target; and call-chain-backward symbolic execution (CCBSE) iteratively runs forward symbolic execution, starting in the function containing the target line, and then jumping backward up the call chain until it finds a feasible path from the start of the program. We also propose Mix- CCBSE, a strategy in which CCBSE is composed with another search strategy to yield a hybrid that is more powerful than either strategy alone. We compare SDSE, CCBSE, and Mix-CCBSE with several existing strategies from the literature. We find that, while SDSE performs extremely well in many cases, it sometimes fails badly. However, by mixing CCBSE with KLEE's search strategy, we obtain a strategy that has the best overall performance across the strategies we studied.
Directing JavaScript with Arrows (Functional Pearl)
(2008-08-02) Khoo, Yit Phang; Hicks, Michael; Foster, Jeffrey S.; Sazawal, Vibha
JavaScript, being a single-threaded language, makes extensive use of event-driven programming to enable responsive web applications. However, standard approaches to sequencing events are messy, and often lead to code that is difficult to understand and maintain. We have found that arrows, a generalization of monads, are an elegant solution to this problem. Arrows allow us to easily write asynchronous programs in small, modular units of code, and flexibly compose them in many different ways, while nicely abstracting the details of asynchronous program composition. In particular, we show how to use arrows to construct a variety of state machines, such as autoscrollers and drag-and-drop handlers.
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.
Dynamic Inference of Static Types for Ruby
(2010-07-19) An, Jong-hoon (David); Chaudhuri, Avik; Foster, Jeffrey S.; Hicks, Michael
There have been several efforts to bring static type inference to object-oriented dynamic languages such as Ruby, Python, and Perl. In our experience, however, such type inference systems are extremely difficult to develop, because dynamic languages are typically complex, poorly specified, and include features, such as eval and reflection, that are hard to analyze. In this paper, we introduce constraint-based dynamic type inference, a technique that infers static types based on dynamic program executions. In our approach, we wrap each run-time value to associate it with a type variable, and the wrapper generates constraints on this type variable when the wrapped value is used. This technique avoids many of the often overly conservative approximations of static tools, as constraints are generated based on how values are used during actual program runs. Using wrappers is also easy to implement, since we need only write a constraint resolution algorithm and a transformation to introduce the wrappers. The best part is that we can eat our cake, too: our algorithm will infer sound types as long as it observes every path through each method body—note that the number of such paths may be dramatically smaller than the number of paths through the program as a whole. We have developed Rubydust, an implementation of our algorithm for Ruby. Rubydust takes advantage of Ruby’s dynamic features to implement wrappers as a language library. We applied Rubydust to a number of small programs. We found it to be lightweight and useful: Rubydust discovered 1 real type error, and all other inferred types were correct, and readable.
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.
Existential Label Flow Inference via CFL Reachability
(2005-11-10T20:04:41Z) Pratikakis, Polyvios; Hicks, Michael; Foster, Jeffrey S.
Label flow analysis is a fundamental static analysis problem with a wide variety of applications. Previous work by Mossin developed a polynomial time subtyping-based label flow inference that supports Hindley-Milner style polymorphism with polymorphic recursion. Rehof et al have developed an efficient O(n^3) inference algorithm for Mossin's system based on context-free language (CFL) reachability. In this paper, we extend these results to a system that also supports existential polymorphism, which is important for precisely describing correlations among members of a structured type, even when values of that type are part of dynamic data structures. We first develop a provably sound checking system based on polymorphically-constrained types. As usual, we restrict universal quantification to the top level of a type, but existential quantification is first class, with subtyping allowed between existentials with the same binding structure. We then develop a CFL-based inference system. Programmers specify which positions in a type are existentially quantified, and the algorithm infers the constraints bound in the type, or rejects a program if the annotations are inconsistent.
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.
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.
Locksmith: Context-Sensitive Correlation Analysis for Race Detection
(2006-06) Pratikakis, Polyvios; Foster, Jeffrey S.; Hicks, Michael
One common technique for preventing data races in multi-threaded programs is to ensure that all accesses to shared locations are consistently protected by a lock. We present a tool called Locksmith for detecting data races in C programs by looking for violations of this pattern. We call the relationship between locks and the locations they protect consistent correlation, and the core of our technique is a novel constraint-based analysis that infers consistent correlation context-sensitively, using the results to check that locations are properly guarded by locks. We present the core of our algorithm for a simple formal language which we have proven sound, and discuss how we scale it up to an algorithm that aims to be sound for all of C. We develop several techniques to improve the precision and performance of the analysis, including a sharing analysis for inferring thread locality; existential quantification for modeling locks in data structures; and heuristics for modeling unsafe features of C such as type casts. When applied to several benchmarks, including multi-threaded servers and Linux device drivers, Locksmith found several races while producing a modest number of false alarms.
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.
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.
Path Projection for User-Centered Static Analysis Tools
(2008-08-01) Khoo, Yit Phang; Foster, Jeffrey S.; Hicks, Michael; Sazawal, Vibha
The research and industrial communities have made great strides in developing sophisticated defect detection tools based on static analysis. However, to date most of the work in this area has focused on developing novel static analysis algorithms, and neglected study of other aspects of static analysis tools, in particular user interfaces. In this work, we present a novel user interface toolkit called Path Projection that helps users visualize, navigate, and understand program paths, a common component of many static analysis tools’ error reports. We performed a controlled user study to measure the benefit of Path Projection in triaging error reports from Locksmith, a data race detection tool for C. We found that Path Projection improved participants’ time to complete this task, without affecting accuracy, and that participants felt Path Projection was useful.

Browsing by Author "Hicks, Michael"

Results Per Page

Sort Options