FRAMEWORK SYNTHESIS FOR SYMBOLIC EXECUTION OF EVENT-DRIVEN FRAMEWORKS

Symbolic execution is a powerful program analysis technique, but it is very challenging to apply to programs built using event-driven frameworks, such as Android. The main reason is that the framework code itself is too complex to symbolically execute. The standard solution is to manually create a framework model that is simpler and more amenable to symbolic execution. However, developing and maintaining such a model by hand is difficult and error-prone. We claim that we can leverage program synthesis to introduce a high-degree of automation to the process of framework modeling. To support this thesis, we present three pieces of work. First, we introduced SymDroid, a symbolic executor for Android. While Android apps are written in Java, they are compiled to Dalvik bytecode format. Instead of analyzing an app’s Java source, which may not be available, or decompiling from Dalvik back to Java, which requires significant engineering effort and introduces yet another source of potential bugs in an analysis, SymDroid works directly on Dalvik bytecode. Second, we introduced Pasket, a new system that takes a first step toward automatically generating Java framework models to support symbolic execution. Pasket takes as input the framework API and tutorial programs that exercise the framework. From these artifacts and Pasket's internal knowledge of design patterns, Pasket synthesizes an executable framework model by instantiating design patterns, such that the behavior of a synthesized model on the tutorial programs matches that of the original framework. Lastly, in order to scale program synthesis to framework models, we devised adaptive concretization, a novel program synthesis algorithm that combines the best of the two major synthesis strategies: symbolic search, i.e., using SAT or SMT solvers, and explicit search, e.g., stochastic enumeration of possible solutions. Adaptive concretization parallelizes multiple sub-synthesis problems by partially concretizing highly influential unknowns in the original synthesis problem. Thanks to adaptive concretization, Pasket can generate a large-scale model, e.g., thousands lines of code. In addition, we have used an Android model synthesized by Pasket and found that the model is sufficient to allow SymDroid to execute a range of apps.

Trace Oblivious Program Execution

The big data era has dramatically transformed our lives; however, security incidents such as data breaches can put sensitive data (e.g. photos, identities, genomes) at risk. To protect users' data privacy, there is a growing interest in building secure cloud computing systems, which keep sensitive data inputs hidden, even from computation providers. Conceptually, secure cloud computing systems leverage cryptographic techniques (e.g., secure multiparty computation) and trusted hardware (e.g. secure processors) to instantiate a “secure” abstract machine consisting of a CPU and encrypted memory, so that an adversary cannot learn information through either the computation within the CPU or the data in the memory. Unfortunately, evidence has shown that side channels (e.g. memory accesses, timing, and termination) in such a “secure” abstract machine may potentially leak highly sensitive information, including cryptographic keys that form the root of trust for the secure systems. This thesis broadly expands the investigation of a research direction called trace oblivious computation, where programming language techniques are employed to prevent side channel information leakage. We demonstrate the feasibility of trace oblivious computation, by formalizing and building several systems, including GhostRider, which is a hardware-software co-design to provide a hardware-based trace oblivious computing solution, SCVM, which is an automatic RAM-model secure computation system, and ObliVM, which is a programming framework to facilitate programmers to develop applications. All of these systems enjoy formal security guarantees while demonstrating a better performance than prior systems, by one to several orders of magnitude.

Predictors of Patient Activation Among Underserved Patients in a Nurse-managed Health Center: A Pilot Study

The concept of patient activation has gained traction as the term referring to patients who understand their role in the care process and have “the knowledge, skills and confidence” necessary to manage their illness over time (Hibbard & Mahoney, 2010). Improving health outcomes for vulnerable and underserved populations who bear a disproportionate burden of health disparities presents unique challenges for nurse practitioners who provide primary care in nurse-managed health centers. Evidence that activation improves patient self-management is prompting the search for theory-based self-management support interventions to activate patients for self-management, improve health outcomes, and sustain long-term gains. Yet, no previous studies investigated the relationship between Self-determination Theory (SDT; Deci & Ryan, 2000) and activation. The major purpose of this study, guided by the Triple Aim (Berwick, Nolan, & Whittington, 2008) and nested in the Chronic Care Model (Wagner et al., 2001), was to examine the degree to which two constructs– Autonomy Support and Autonomous Motivation– independently predicted Patient Activation, controlling for covariates. For this study, 130 nurse-managed health center patients completed an on-line 38-item survey onsite. The two independent measures were the 6-item Modified Health Care Climate Questionnaire (mHCCQ; Williams, McGregor, King, Nelson, & Glasgow, 2005; Cronbach’s alpha =0.89) and the 8-item adapted Treatment Self-Regulation Questionnaire (TSRQ; Williams, Freedman, & Deci, 1998; Cronbach’s alpha = 0.80). The Patient Activation Measure (PAM-13; Hibbard, Mahoney, Stock, & Tusler, 2005; Cronbach’s alpha = 0.89) was the dependent measure. Autonomy Support was the only significant predictor, explaining 19.1% of the variance in patient activation. Five of six autonomy support survey items regressed on activation were significant, illustrating autonomy supportive communication styles contributing to activation. These results suggest theory-based patient, provider, and system level interventions to enhance self-management in primary care and educational and professional development curricula. Future investigations should examine additional sources of autonomy support and different measurements of autonomous motivation to improve the predictive power of the model. Longitudinal analyses should be conducted to further understand the relationship between autonomy support and autonomous motivation with patient activation, based on the premise that patient activation will sustain behavior change.

EXISTENCE OF UNUSED MANAGED CAPACITY ON DEDICATED LANES AND AN ALTERNATIVE ON HOW TO SELL IT VIA AUCTIONS

This dissertation verifies whether the following two hypotheses are true: (1) High-occupancy/toll lanes (and therefore other dedicated lanes) have capacity that could still be used; (2) such unused capacity (or more precisely, “unused managed capacity”) can be sold successfully through a real-time auction. To show that the second statement is true, this dissertation proposes an auction-based metering (ABM) system, that is, a mechanism that regulates traffic that enters the dedicated lanes. Participation in the auction is voluntary and can be skipped by paying the toll or by not registering to the new system. This dissertation comprises the following four components: a measurement of unused managed capacity on an existing HOT facility, a game-theoretic model of an ABM system, an operational description of the ABM system, and a simulation-based evaluation of the system. Some other and more specific contributions of this dissertation include the following: (1) It provides a definition and a methodology for measuring unused managed capacity and another important variable referred as “potential volume increase”. (2) It proves that the game-theoretic model has a unique Bayesian Nash equilibrium. (3) And it provides a specific road design that can be applied or extended to other facilities. The results provide evidence that the hypotheses are true and suggest that the ABM system would benefit a public operator interested in reducing traffic congestion significantly, would benefit drivers when making low-reliability trips (such as work-to-home trips), and would potentially benefit a private operator interested in raising revenue.