Christian Skalka, Publications

Federated machine learning leverages edge computing to develop models from network user data, but privacy in federated learning remains a major challenge. Techniques using differential privacy have been proposed to address this, but bring their own challenges- many require a trusted third party or else add too much noise to produce useful models. Recent advances in secure aggregation using multiparty computation eliminate the need for a third party, but are computationally expensive especially at scale. We present a new federated learning protocol that leverages a novel differentially private, malicious secure aggregation protocol based on techniques from Learning With Errors. Our protocol outperforms current state-of-the art techniques, and empirical results show that it scales to a large number of parties, with optimal accuracy for any differentially private federated learning scheme

Host-based Intrusion Detection Systems (HIDS) automatically detect events that indicate compromise by adversarial applications. HIDS are generally formulated as analyses of sequences of system events such as bash commands or system calls. Anomaly-based approaches to HIDS leverage models of normal (a.k.a. baseline) system behavior to detect and report abnormal events and have the advantage of being able to detect novel attacks. In this article, we develop a new method for anomaly-based HIDS using deep learning predictions of sequence-to-sequence behavior in system calls. Our proposed method, called the ALAD algorithm, aggregates predictions at the application level to detect anomalies. We investigate the use of several deep learning architectures, including WaveNet and several recurrent networks. We show that ALAD empowered with deep learning significantly outperforms previous approaches. We train and evaluate our models using an existing dataset, ADFA-LD, and a new dataset of our own construction, PLAID. As deep learning models are black box in nature, we use an alternate approach, allotaxonographs, to characterize and understand differences in baseline vs. attack sequences in HIDS datasets such as PLAID.

Keywords: deep learning, system calls, Host-based intrusion detection systems

Background: Knee extensor muscle performance is reduced after lower extremity trauma and orthopedic surgical interventions. At-home use of neuromuscular electrical stimulation (NMES) may improve functional recovery, but adherence to at-home interventions is low. Greater benefits from NMES may be realized with closer monitoring of adherence to at-home prescriptions and more frequent patient-provider interactions. Objective: This study aimed to develop a cyber-physical system to monitor at-home adherence to NMES prescription and facilitate patient-provider communications to improve adherence in near real time. Methods: The RehabTracker cyber-physical system was developed to accomplish this goal and comprises four components: (1) hardware modifications to a commercially available NMES therapy device to monitor device use and provide Bluetooth functionality; (2) an iPhone Operating System--based mobile health (mHealth) app that enables patient-provider communications in near real time; (3) a clinician portal to allow oversight of patient adherence with device use; and (4) a back-end server to store data, enable adherence analysis, and send automated push notifications to the patient. These four elements were designed to be fully compliant with the Health Insurance Portability and Accountability Act. The system underwent formative testing in a cohort of patients following anterior cruciate ligament rupture (n=7) to begin to assess face validity. Results: Compared with the NMES device software--tracked device use, the RehabTracker system recorded 83% (40/48) of the rehabilitation sessions, with 100% (32/32) of all sessions logged by the system in 4 out of 7 patients. In patients for whom tracking of automated push notifications was enabled, 100% (29/29) of the push notifications sent by the back-end server were received by the patient. Process, hardware, and software issues contributing to these inaccuracies are detailed. Conclusions: RehabTracker represents a promising mHealth app for tracking and improving adherence with at-home NMES rehabilitation programs and warrants further refinement and testing.

Keywords: device use tracking; internet of things; neuromuscular electrical stimulation; exercise; smart devices; mHealth; rehabilitation; mobile health; digital health

Authorization hooks are access control checks that prevent unauthorized principals from interacting with some protected resource, and are used extensively in critical software such as operating systems, middleware, and server programs. They are often intended to mediate information flow between subjects (e.g., file owners), but typically in an ad-hoc manner. In this paper we present a static type and effect system for detecting whether authorization hooks in programs properly defend against undesired information flow between subjects. A significant novelty of our approach is an integrated abstract interpretation-based tool that guides system clients through the information flow consequences of access control policy decisions.

Dynamic taint analysis is often used as a defense against low-integrity data in applications with untrusted user interfaces. An important example is defense against XSS and injection attacks in programs with web interfaces. Data sanitization is commonly used in this context, and can be treated as a precondition for endorsement in a dynamic integrity taint analysis. However, sanitization is often incomplete in practice. We develop a model of dynamic integrity taint analysis for Java that addresses imperfect sanitization with an in-depth approach. To avoid false positives, results of sanitization are endorsed for access control (aka prospective security), but are tracked and logged for auditing and accountability (aka retrospective security). We show how this heterogeneous prospective/retrospective mechanism can be specified as a uniform policy, separate from code. We then use this policy to establish correctness conditions for a program rewriting algorithm that instruments code for the analysis. These conditions synergize our previous work on the semantics of audit logging with explicit integrity which is an analogue of noninterference for taint analysis. A technical contribution of our work is the extension of explicit integrity to a high-level functional language setting with structured data, vs. previous systems that only address low level languages with unstructured data. Our approach considers endorsement which is crucial to address sanitization. An implementation of our rewriting algorithm is presented that hardens the OpenMRS medical records software system with in-depth taint analysis, along with an empirical evaluation of the overhead imposed by instrumentation. Our results show that this instrumentation is practical.

Computer networks often serve as the first line of defense against malicious attacks. Although there are a growing number of software defined networking (SDN) tools for defining and enforcing security policies, most assume a single administrative domain and are unable to handle the challenges that arise in networks that could beneficially be programmed by multiple administrative domains. For example, consumers may want want to allow their home IoT networks to be configured by device vendors, which raises security and privacy concerns. In this paper we propose a framework called Proof Carrying Network Code (PCNC) for specifying and enforcing security in SDNs with interacting administrative domains. Like Proof Carrying Authorization (PCA), PCNC provides methods for authorization domains for network reprogramming, and like Proof Carrying Code (PCC), PCNC provides methods for enforcing desired behavior of network programs. We develop theoretical foundations for PCNC and evaluate it in simulated and real network settings, in a case study that considers security in IoT networks for at-home health monitoring.

A majority of adults in the United States are exposed to a potentially traumatic event but only a handful go on to develop impairing mental health conditions such as posttraumatic stress disorder (PTSD). Identifying those at elevated risk shortly after trauma exposure is a clinical challenge. The aim of this study was to develop computational methods to more effectively identify at-risk patients and, thereby, support better early interventions. We proposed machine learning (ML) induction of models to automatically predict elevated PTSD symptoms in patients 1 month after a trauma, using self-reported symptoms from data collected via smartphones. We show that an ensemble model accurately predicts elevated PTSD symptoms, with an area under the curve (AUC) of .85, using a bag of support vector machines, naive Bayes, logistic regression, and random forest algorithms. Furthermore, we show that only 7 self-reported items (features) are needed to obtain this AUC. Most importantly, we show that accurate predictions can be made 10 to 20 days posttrauma. These results suggest that simple smartphone-based patient surveys, coupled with automated analysis using ML-trained models, can identify those at risk for developing elevated PTSD symptoms and thus target them for early intervention.

PTSD is posited to develop in the acute posttrauma period. Few studies have examined psychopathology symptoms within this period due to the demands on individuals 10 in the first month after a trauma. Mobile devices can overcome these barriers. The feasibility of using mobile devices for this purpose, however, is unclear. The present study evaluated the acceptability of administering PTSD symptom assessments via a mobile application throughout the acute posttrauma period. The study suggests that using mobile devices to monitor mental health symptoms during the acute posttrauma period is feasible and acceptable. Strategies are needed to determine how to best take advantage of these data once collected.

Access control is a necessary defense to protect security-sensitive operations. Unfortunately, access control mechanisms are implemented manually in practice, which can lead to errors that can be exploited. Prior work aims to find such errors through static analysis, but the correctness of access control enforcement depends on runtime factors, such as the access control policies enforced and adversary control of the program inputs. As a result, we propose to apply provenance tracking to find flaws in access control enforcement. To do so, we track decisions made in deploying access control enforcement to enable detection of flaws. We have developed AutoProv, a Java bytecode analysis tool capable of retrofitting legacy Java applications with provenance hooks. We utilize AutoProv to add provenance hooks at all locations that either may require access control enforcement or may impact access control policy decisions. We evaluate our tool on OpenMRS, an open source medical record system,which is used across the globe to manage sensitive data for millions of patients.

While we have long had principles describing how access control enforcement should be implemented, such as the reference monitor concept, imprecision in access control mechanisms and access control policies leads to risks that may enable exploitation. In practice, least privilege access control policies often allow information ows that may enable exploits. In addition, the implementation of access control mechanisms often tries to balance security with ease of use implicitly (e.g., with respect to determining where to place authorization hooks) and approaches to tighten access control, such as accounting for program context, are ad hoc. In this paper, we define four types of risks in access control enforcement and explore possible approaches and challenges in tracking those types of risks. In principle, we advocate runtime tracking to produce risk estimates for each of these types of risk. To better understand the potential of risk estimation for authorization, we propose risk estimate functions for each of the four types of risk, finding that benign program deployments accumulate risks in each of the four areas for ten Android programs examined. As a result, we find that tracking of relative risk may be useful for guiding changes to security choices, such as authorized unsafe operations or placement of authorization checks, when risk differs from that expected.

Current frameworks for network programming assume that the network comprises a set of homogenous devices that can be rapidly reconfigured in response to changing policies and network conditions. Unfortunately, these assumptions are incompatible with the realities of modern networks, which contain legacy devices that offer diverse functionality and can only be reconfigured slowly. Additionally, network service providers need to walk a fine line between providing flexibility to users, and maintaining the integrity and reliability of their core networks. These issues are particularly evident in optical networks, which are used by ISPs andWANs and provide high bandwidth at the cost of limited flexibility and long reconfiguration times. This paper presents a different approach to implementing high-level policies, by pushing functionality to the edge and using the core merely for transit. Building on the NetKAT framework and leveraging linear programming solvers, we develop techniques for analyzing and transforming policies into configurations that can be installed at the edge of the network. Furthermore, our approach can be extended to incorporate constraints that are crucial in the optical domain, such as path constraints. We develop a working implementation using off-the-shelf solvers and evaluate our approach on realistic optical topologies.

Trauma exposure markedly increases risk for psychopathology including posttraumatic stress disorder (PTSD). Understanding the course by which PTSD develops after a traumatic event is critical to enhancing early intervention. Although prior work has explored the course of PTSD symptoms in the subsequent months, relatively few studies have explored the course of symptoms in the acute posttrauma period, defined as the 30 days after a traumatic event. A key challenge to conducting such studies is the lack of efficient means to collect data that does not impose significant burden on the participant during this time. The present study evaluated the use of a mobile phone application to collect symptom data during the acute posttrauma period. Data was obtained from 23 individuals who experienced a criterion A traumatic event and were recruited from the emergency department of a level-1 trauma center. Participants completed 44.93% of daily assessments across a 30-day period. Responses rates were uncorrelated with PTSD symptoms or depression symptoms at 1- and 3-month posttrauma. Participants reported that the surveys were moderately helpful and posed minimal burden. These findings suggest that mobile applications can be used to learn about the course of posttrauma recovery.

Dynamic taint analysis can be used as a defense against low-integrity data in applications with untrusted user interfaces. An important example is defense against XSS and injection attacks in programs with web interfaces. Data sanitization is commonly used in this context, and can be treated as a precondition for endorsement in a dynamic integrity taint analysis. However, sanitization is often incomplete in practice. We develop a model of dynamic integrity taint analysis for Java that addresses imperfect sanitization with an in-depth approach. To avoid false positives, results of sanitization are endorsed for access control (aka prospective security), but are tracked and logged for auditing and accountability (aka retrospective security). We show how this heterogeneous prospective/retrospective mechanism can be specified as a uniform policy, separate from code. We then use this policy to establish correctness conditions for a program rewriting algorithm that instruments code for the analysis. The rewriting itself is a model of existing, efficient Java taint analysis tools.

Satellite imagery and remote sensing provide explanatory variables at relatively high resolutions for modeling geospatial phenomena, yet regional summaries are often desirable for analysis and actionable insight. In this paper, we propose a novel method of inducing spatial aggregations as a component of the machine learning process, yielding regional model features whose construction is driven by model prediction performance rather than prior assumptions. Our results demonstrate that Genetic Programming is particularly well suited to this type of feature construction because it can automatically synthesize appropriate aggregations, as well as better incorporate them into regression models compared to other regression models we tested. In our experiments we consider a specific problem instance and real-world dataset relevant to predicting snow properties in high-mountain Asia.

In some wireless sensor network applications, multiple sensors can be used to measure the same variable, while differing in their sampling cost, for example in their power requirements. This raises the problem of automatically controlling heterogeneous sensor suites in wireless sensor network applications, in a manner that balances cost and accuracy of sensors. We apply genetic programming (GP) to this problem, considering two basic approaches. First, we construct a hierarchy of models, where increasing levels in the hierarchy use sensors of increasing cost. If a model that polls low cost sensors exhibits too much prediction uncertainty, the burden of prediction is automatically transferred to a higher level model using more expensive sensors. Second, we train models with cost as an optimization objective, called non-hierarchical models, that use conditionals to automatically select sensors based on both cost and accuracy. We compare these approaches in a setting where the available budget for sampling is considered to remain constant, and in a setting where the system is sensitive to a fluctuating budget, for example available battery power. We show that in both settings, for increasingly challenging datasets, hierarchical models makes predictions with equivalent accuracy yet lower cost than non-hierarchical models.

Retrospective security has become increasingly important to the theory and practice of cyber security, with auditing a crucial component of it. However, in systems where auditing is used, programs are typically instrumented to generate audit logs using manual, ad-hoc strategies. This is a potential source of error even if log analysis techniques are formal, since the relation of the log itself to program execution is unclear. This paper focuses on provably correct program rewriting algorithms for instrumenting formal logging specifications. Correctness guarantees that the execution of an instrumented program produces sound and complete audit logs, properties defined by an information containment relation between logs and the program's logging semantics. We also propose a program rewriting approach to instrumentation for audit log generation, in a manner that guarantees correct log generation even for untrusted programs. As a case study, we develop such a tool for OpenMRS, a popular medical records management system, and consider instrumentation of break the glass policies.

Victims of trauma are at high risk for mental health conditions such as posttraumatic stress disorder and depression. Regular assessment of mental health symptoms in the post-trauma period is necessary to identify those at greatest risk and provide treatment. The multiple demands of the acute post-trauma period present numerous barriers to such assessments. Mobile applications are a method by which to overcome these barriers in order to regularly assess symptoms, identify those at risk, and connect patients to needed services. The current study conducted a usability evaluation of a system to monitor mental health symptoms after a trauma. The system was developed to promote ease of use and facilitate quick transmission of data. The results of the current study indicate that a mobile application to monitor post- trauma mental health symptoms would be well received by victims. Personalized feedback to the user was identified as critical to promote the usability of the software.

Retrospective security is an important element of layered security systems. Auditing is central to the theory and practice of retrospective security, however, in systems where auditing is used, programs are typically instrumented to generate audit logs using manual, ad-hoc strategies. This is a potential source of error even if log auditing techniques are formal, since the relation of the log itself to program execution is unclear. This paper focuses on provably correct program rewriting algorithms for instrumenting formal logging specifications. Correctness guarantees that execution of an instrumented program produces sound and complete audit logs, properties defined by an information containment relation between logs and the program's logging semantics. As an application example, we consider auditing for break the glass policies, wherein authorization is replaced by auditing in emergency conditions.

Resource constrained sensor systems are an increasingly attractive option in a variety of environmental monitoring domains, due to continued improvements in sensor technology. However, sensors for the same measurement application can differ in terms of cost and accuracy, while fluctuations in environmental conditions can impact both application requirements and available energy. This raises the problem of automatically controlling heterogeneous sensor suites in resource constrained sensor system applications, in a manner that balances cost and accuracy of available sensors. We present a method that employs a hierarchy of model ensembles trained by genetic programming (GP): if model ensembles that poll low-cost sensors exhibit too much prediction uncertainty, they automatically transfer the burden of prediction to other GP-trained model ensembles that poll more expensive and accurate sensors. We show that, for increasingly challenging datasets, this hierarchical approach makes predictions with equivalent accuracy yet lower cost than a similar yet non-hierarchical method in which a single GP-generated model determines which sensors to poll at any given time. Our results thus show that a hierarchy of GP-trained ensembles can serve as a control algorithm for heterogeneous sensor suites in resource constrained sensor system applications that balances cost and accuracy.

Infrastructure for the automatic collection of single-point measurements of snow water equivalent (SWE) is well-established. However, because SWE varies significantly over space, the estimation of SWE at the catchment scale based on a single-point measurement is error-prone. We propose low-cost, lightweight methods for near-real-time estimation of mean catchment-wide SWE using existing infrastructure, wireless sensor networks, and machine learning algorithms. Because snowpack distribution is known to be highly nonlinear, we focus on genetic programming (GP), a nonlinear, white-box, inductive machine learning algorithm. Because we did not have access to near-real-time catchment-scale SWE data, we used available data as ground truth for machine learning in a set of experiments that are successive approximations of our goal of catchment-wide SWE estimation. First, we used a history of maritime snowpack data collected by manual snow courses as our ground truth estimate of mean catchment SWE. Second, we used distributed snow depth (SD) data collected automatically by wireless sensor networks. Thus SD served as an alternative to SWE. Because SD variability is significantly greater than density variability, the primary requirement for estimating SWE over an area is an understanding of SD. We compared the performance of GP against linear regression (LR), binary regression trees (BT), and a widely used basic method (BM) that naively assumes non-variable snowpack. In the first experiment set, GP and LR models predicted SWE with lower error than BM. In the second experiment set, GP had lower error than LR, but outperformed BT only when we applied a technique for determining training and testing datasets that specifically mitigated the possibility of over-fitting.

The computer security community has long advocated defense in depth, the concept of building multiple layers of defense to protect a system. Unfortunately, it has been difficult to realize this vision in practice, and software often ships with inadequate defenses, typically developed in an ad hoc fashion. Currently, programmers reason about security manually and lack tools to validate assurance that security controls provide satisfactory defenses. In this position paper, we propose STRATA---a holistic framework for defense in depth. We examine application of STRATA in the context of adding security controls to legacy code for authorization, containment, and auditing. The STRATA framework aims to support a combination of: (1) interactive techniques to develop retrofitting policies that describe the connection between program constructs and security policy and (2) automated techniques to produce optimal security controls that satisfy retrofitting policies. We show that by reasoning about defense in depth a variety of advantages can be obtained, including optimization, continuous improvement, and assurance across multiple security controls.

Public-use earth science datasets are a useful resource with the unfortunate feature that their provenance is easily disconnected from their content. “Fair-use policies” typically associated with these datasets require appropriate attribution of providers by users, but sound and complete attribution is difficult if provenance information is lost. To address this we introduce a technique to directly associate provenance information with sensor datasets. Our technique is similar to traditional watermarking but is intended for application to unstructured time-series datasets. Our approach is potentially imperceptible given sufficient margins of error in datasets, and is robust to a number of benign but likely transformations including truncation, rounding, bit-flipping, sampling, and reordering. We provide algorithms for both one-bit and blind mark checking, and show how our system can be adapted to various data representation types. Our algorithms are probabilistic in nature and are characterized by both combinatorial and empirical analyses. Mark embedding can be applied at any point in the data lifecycle, allowing adaptation of our scheme to social or scientific concerns.

We describe SpartanRPC, a secure middleware technology that supports cooperation between distinct security domains in wireless sensor networks. SpartanRPC extends nesC to provide a link-layer remote procedure call (RPC) mechanism, along with an enhancement of configuration wirings that allow specification of remote, dynamic endpoints. RPC invocation is secured via an authorization logic that enables servers to specify access policies, and requires clients to prove authorization. This mechanism is implemented using a combination of symmetric and public key cryptography. We report on benchmark testing of a prototype implementation, and on an application of the framework that supports secure collaborative use and administration of an existing WSN data gathering system.

Programming wireless embedded networks is challenging due to severe limitations on processing speed, memory, and bandwidth. Staged programming can help bridge the gap between high level code refinement techniques and efficient device level programs by allowing a first stage program to specialize device level code. Here we introduce a two stage programming system for wireless sensor networks. The first stage program is written in our extended dialect of Scala, called Scalaness, where components written in our type safe dialect of nesC, called nesT, are composed and specialized. Scalaness programs can dynamically construct TinyOS-compliant nesT device images that can be deployed to motes. A key result, called cross-stage type safety, shows that successful static type checking of a Scalaness program means no type errors will arise either during programmatic composition and specialization of WSN code, or later on the WSN itself. Scalaness has been implemented through direct modification and plug-in extension of the Scala compiler. Implementation of a staged public-key cryptography calculation shows the sensor memory footprint can be significantly reduced by staging.

Snowcloud is a data gathering system for snow hydrology field research campaigns conducted in harsh climates and remote areas. The system combines distributed wireless sensor network technology and computational techniques to provide data to researchers at lower cost and higher spatial resolution than ground-based systems using traditional “monolithic” technologies. Supporting the work of a variety of collaborators, Snowcloud has seen multiple Winter deployments in settings ranging from high desert to arctic, resulting in over a dozen node-years of practical experience. In this paper, we discuss both the system design and deployment experiences.

Staging is a powerful language construct that allows a program at one stage of evaluation to manipulate and specialize a program to be executed at a later stage. We propose a new staged language calculus, <ML>, which extends the programmability of staged languages in two directions. First, <ML> supports dynamic type specialization: types can be dynamically constructed, abstracted, and passed as arguments, while preserving decidable typechecking via a System F_<=-style semantics combined with a restricted form of λ_ω-style runtime type construction. With dynamic type specialization the data structure layout of a program can be optimized via staging. Second, <ML> works in a context where different stages of computation are executed in different process spaces, a property we term staged process separation. Programs at different stages can directly communicate program data in <ML> via a built-in serialization discipline. The language <ML> is endowed with a metatheory including type preservation, type safety, and decidability as demonstrated constructively by a sound type checking algorithm. While our language design is general, we are particularly interested in future applications of staging in resource-constrained and embedded systems: these systems have limited space for code and data, as well as limited CPU time, and specializing code for the particular deployment at hand can improve efficiency in all of these dimensions. The combination of dynamic type specialization and staging across processes greatly increases the utility of staged programming in these domains. We illustrate this via wireless sensor network programming examples.

Snow accumulated in mountainous areas is the source of water supply for much of the western United States. Expected amounts of annual discharge in rivers are based on snow water equivalence (SWE) measurements and regression models that have climate stability as an underlying assumption. Given climate change, estimates should change from statistical to physically-based models. The current data collection network for SWE provides sparse areal coverage. Inexpensive wireless sensor networks and simple estimation techniques could inexpensively extend the current network. We report results of deployment of a prototype wireless sensor network, Snowcloud, at the Sagehen Creek, CA experimental field station. The network reported snow depth and temperature from January.May, 2010. We extrapolated from an index site to estimate SWE with SD, based on the assumption of stability SWE/SD and predicted SWE with reasonable accuracy (average difference of +1.0 cm (0.4 in), standard deviation = 3.0 cm (1.2 in)). Regression analysis indicated significant associations (P<.05) between SWE and closure to the north, weekly total incoming solar radiation and monthly average temperature. These results indicate that wireless sensor networks measuring SD can be used to extend information from snow measurement sites to give estimates of water availability in snowpack.

In this paper we describe SpartanRPC, a secure middleware technology for wireless sensor network (WSN) applications supporting cooperation between distinct protection domains. The SpartanRPC system extends the nesC programming language to provide a link-layer remote procedure call (RPC) mechanism, along with an extension of nesC configuration wirings that allow specification of remote, dynamic endpoints. SpartanRPC also incorporates a capability-based security architecture for protection of RPC resources in a heterogeneous trust environment, via language-level policy specification and enforcement. We discuss an implementation of SpartanRPC based on program transformation and AES cryptography, and present empirical performance results.

Public-use sensor datasets are a useful scientific resource with the unfortunate feature that their provenance is easily disconnected from their content. To address this we introduce a technique to directly associate provenance information with sensor datasets. Our technique is similar to traditional watermarking but is intended for application to unstructured time-series data. Our approach is potentially imperceptible given sufficient margins of error in datasets, and is robust to a number of benign but likely transformations including truncation, rounding, bit-flipping, sampling, and reordering. We provide algorithms for both one-bit and blind mark checking. Our algorithms are probabilistic in nature and are characterized by a combinatorial analysis.

Staging is a powerful language construct that allows a program at one stage to manipulate and specialize a program at the next. We propose <ML> as a new staged calculus designed with novel features for staged programming in modern computing platforms such as embedded systems. A distinguishing feature of <ML> is a model of process separation, whereby different stages of computation are executed in different process spaces. Our language also supports dynamic type specialization via type abstraction, dynamic type construction, and a limited form of type dependence. <ML> is endowed with a largely standard metatheory, including type preservation and type safety results. We discuss the utility of our language via code examples from the domain of wireless sensor network programming.

We prove type safety of the Hoare Type Theory (HTT), an extension of Separation Logic and Hoare Logic to higher-order functional programs. Our proof is rather simple and is based on subject reduction, unlike previous work on HTT by Birkedal et al., which uses nontrivial denotational semantics. Further, we formalized our proof in the Coq theorem prover. This formalization can be seen as a basis of a platform for verifying higher-order imperative programs that is alternative to Ynot, another implementation of HTT in Coq.

We describe a ground-based system that provides quasi real-time measurement and collection of snow-water equivalent (SWE) data in remote settings. The system is significantly cheaper and easier to deploy than current methods and is more robust to terrain and snow bridging effects. The system also enjoys several possible remote data recovery solutions. Compared to current infrastructure using existing technology, our system features will combine to allow more sites to be installed for the same cost and effort, in a greater variety of terrain, enabling data collection at improved spatial resolutions. The system integrates a new computational architecture with new sensor technologies. Our computational architecture is based on wireless sensor networks, comprised of programmable, low-cost, low-powered nodes capable of sophisticated sensor control and remote data communication. Our sensor technology works by measuring attenuation of electromagnetic radiation, an approach that is immune to snow bridging and significantly reduces sensor footprints.

Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. In this paper we develop a type and effect analysis for obtaining trace effects of Object Oriented programs in Featherweight Java. We observe that the analysis is significantly complicated by the interaction of trace behavior with inheritance and other Object Oriented features, particularly overridden methods, dynamic dispatch, and downcasting. We propose an expressive type and effect inference algorithm combining polymorphism and subtyping/subeffecting constraints to obtain a flexible trace effect analysis in this setting, and show how these techniques are applicable to Object Oriented features. We also extend the basic language model with exceptions and stack-based event contexts, and show how trace effects scale to these extensions by structural transformations.

Trust management systems are frameworks for authorization in modern distributed systems, allowing remotely accessible resources to be protected by providers. By allowing providers to specify policy, and access requesters to possess certain access rights, trust management automates the process of determining whether access should be allowed on the basis of policy, rights, and an authorization semantics. In this paper we survey modern state-of-the-art in trust management, focusing on features of policy and rights languages that provide the necessary expressiveness for modern practice. We characterize systems in light of a generic structure that takes into account components of practical implementations. We emphasize systems that have a formal foundation, since security properties of them can be rigorously guaranteed. Underlying formalisms are reviewed to provide necessary background.

This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher order programs. The properties verified are based on the ordered sequence of events that occur during program execution, so called event traces. Our type and effect systems infer conservative approximations of the event traces arising at run-time, and model-checking techniques are used to verify logical properties of these histories. Our language model is based on the λ-calculus. Technical results include a type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the trace effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms. A type safety result is proven for both unification and subtyping constraint versions of the type system, ensuring that statically well-typed programs do not contain trace event checks that can fail at run-time.

We develop a static analysis which distills first-order computational structure from higher-order functional programs. The analysis condenses higher-order programs into a first-order rule-based system, a nugget, that characterizes all value bindings that may arise from program execution. Theorem provers are limited in their ability to automatically reason about higher-order programs; nuggets address this problem, being inductively defined structures that can be simply and directly encoded in a theorem prover. The theorem prover can then prove non-trivial program properties, such as the range of values assignable to particular variables at runtime. Our analysis is flow- and path-sensitive, and incorporates a novel prune-rerun analysis technique to approximate higher-order recursive computations.

The Java JDK security model provides an access control mechanism for the JVM based on dynamic stack inspection. Previous results have shown how stack inspection can be enforced at compile time via whole-program type analysis, but features of the JVM present significant remaining technical challenges. For instance, dynamic dispatch at the bytecode level requires special consideration to ensure flexibility in typing. Even more problematic is dynamic class loading and linking, which disallow a purely static analysis in principle, though the intended applications of the JDK exploit these features. We propose an extension to existing bytecode verification, that enforces stack inspection at link time, without imposing new restrictions on the JVM class loading and linking mechanism. Our solution is more flexible than existing type based approaches, and establishes a formal type safety result for bytecode-level access control in the presence of dynamic class linking.

Distributed authorization takes into account several elements, including certificates that may be provided by non-local actors. While most trust management systems treat all assertions as equally valid up to certificate authentication, realistic considerations may associate risk with some of these elements, for example some actors may be less trusted than others. Furthermore, practical online authorization may require certain levels of risk to be tolerated. In this paper, we introduce a trust management logic that incorporates formal risk assessment. This formalization allows risk levels to be associated with authorization elements, and promotes development of a distributed authorization algorithm allowing tolerable levels of risk to be precisely specified and rigorously enforced.

Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. In this paper we develop a type and effect analysis for obtaining trace effects of Object Oriented programs in Featherweight Java. We observe that the analysis is significantly complicated by the interaction of trace behavior with inheritance and other Object Oriented features, particularly overridden methods, dynamic dispatch, and downcasting. We propose an expressive type and effect inference algorithm combining polymorphism and subtyping/subeffecting constraints to obtain a flexible trace effect analysis in this setting, and show how these techniques are applicable to Object Oriented features. We also extend the basic language model with exceptions and stack-based event contexts, and show how trace effects scale to these extensions by structural transformations.

We propose the monadic linear logic programming language LolliMon as a new foundation for the specification of distributed trust management systems, particularly the RT framework. LolliMon possesses features that make it well-suited to this application, including rigorous logical foundations, an expressive formula language, strong typing, and saturation as a proof resolution strategy. We specify certificate chain discovery in full RT for authorization in a distributed environment where certificates may be stored non-locally and selective retrieval is necessary. The uniform LolliMon specification of authorization and certificate chain discovery eases formal reasoning about the system, and scales to a rich collection of trust management features. The executable LolliMon specification also serves as a prototype implementation.

Through web service technology, distributed applications can be built in an open and flexible manner, bringing tremendous power to applications on the web. However, this flexibility poses significant challenges to security. Traditional access control for distributed systems is not flexible and efficient enough in such an environment; in particular, fully secure online authorization decisions may be too inefficient in practice, requiring simplifications which may have only an informal and unverifiable relation to fully secure authorization decisions. This paper introduces a trust-but-verify framework for web services authorization. In this framework, each web service maintains the usual access control policies, as well as a “trust transformation” policy, that formally specifies how to simplify full authorization into a more efficient form for online checking. This formalization allows certainty that offline checking verifies the trust relation between full security and online checking.

Distributed authorization takes into account several elements, including certificates that may be provided by non-local actors. While most trust management systems treat all assertions as equally valid up to certificate authentication, realistic considerations may associate risk with some of these elements; some actors may be less trusted than others, some elements may be more computationally expensive to obtain, and so forth. Furthermore, practical online authorization may require certain levels of risk to be tolerated. In this paper, we introduce a trust management logic that incorporates formal risk assessment. This formalization allows risk levels to be associated with authorization elements, and promotes development of a distributed authorization algorithm allowing tolerable levels of risk to be precisely specified and rigorously enforced.

Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. In this paper we develop a type and effect analysis for obtaining trace effects of Object Oriented programs in Featherweight Java. We observe that the analysis is significantly complicated by the interaction of trace behavior with inheritance and other Object Oriented features, particularly overridden methods, dynamic dispatch, and downcasting. We propose an expressive type and effect inference algorithm combining polymorphism and subtyping/subeffecting constraints to obtain a flexible trace effect analysis in this setting, and show how these techniques are applicable to Object Oriented features.

This paper describes a flexible type and effect inference system for Featherweight Java (FJ). The effect terms generated by static type and effect inference embody the abstract interpretation of program event sequences. Flexibility in the analysis is obtained by post-processing of inferred effects, allowing a modular adaptation to extensions of the language. Several example transformations are discussed, including how inferred effects can be transformed to reflect the impact of exceptions on FJ control flow.

The Java Security Architecture includes a dynamic mechanism for enforcing access control checks, the so-called stack inspection process. While the architecture has several appealing features, access control checks are all implemented via dynamic method calls. This is a highly non-declarative form of specification which is hard to read, and which leads to additional run-time overhead. This paper develops type systems which can statically guarantee the success of these checks. Our systems allow security properties of programs to be clearly expressed within the types themselves, which thus serve as static declarations of the security policy. We develop these systems using a systematic methodology: we show that the security-passing style translation, proposed by Wallach, Appel and Felten as a dynamic implementation technique, also gives rise to static security-aware type systems, by composition with conventional type systems. To define the latter, we use the general HM(X) framework, and easily construct several constraint- and unification-based type systems.

The confinement of object references is a significant security concern for modern programming languages. We define a language that serves as a uniform model for a variety of confined object reference systems. A use-based approach to confinement is adopted, which we argue is more expressive than previous communication-based approaches. We then develop a readable, expressive type system for static analysis of the language, along with a type safety result demonstrating that run-time checks can be eliminated. The language and type system thus serve as a reliable, declarative and efficient foundation for secure capability-based programming and object confinement.

Through web service technology, distributed applications can be built in a flexible manner, bringing tremendous power to applications on the web. However, this flexibility poses significant challenges to security. In particular, an end user (be it human or machine) may access a web service directly, or through a number of intermediaries, while these intermediaries may be formed on the fly for a particular task. Traditional access control for distributed systems is not flexible and efficient enough in such an environment. Indeed, it may be impossible for a web service to anticipate all possible access patterns, hence to define an appropriate access control list beforehand. Novel solutions are needed.

This paper introduces a trust-but-verify framework for web services authorization, and provides an implementation example. In the trust-but-verify framework, each web service maintains authorization policies. In addition, there is a global set of “trust transformation” rules, each of which has an associated transformation condition. These trust transformation rules convert complicated access patterns into simpler ones, and the transformation is done by a requester (the original requester or an intermediary) with the assumption that the requester can be trusted to correctly omit certain details. To verify authorization, the requester is required to document evidence that the associated transformation conditions are satisfied. Such evidence and support information can either be checked before access is granted, or can be verified after the fact in an offline mode, possibly by an independent third party.

This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher-order programs. The properties verified are based on the ordered sequence of events that occur during program execution---an event history. Our type and effect systems automatically infer conservative approximations of the event histories arising at run-time, and model-checking techniques are used to verify logical properties of these histories.

Our language model is based on the λ-calculus. Technical results include a powerful type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the history effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms.

We present pml_B, a programming language that includes primitive sets and associated operations. The language is equipped with a precise type discipline that statically captures dynamic properties of sets, allowing runtime optimizations. We demonstrate the utility of pml_B by showing how it can serve as a practical implementation language for higher-level programming language based security systems, and characterize pml_B by comparing the expressiveness of pml_B sets with enumerations.

The HM(X) framework is a constraint-based type framework with built-in let-polymorphism. This paper establishes purely syntactic type soundness for the framework, treating an extended version of the language containing state and recursive binding. These results demonstrate that any instance of HM(X), comprising a specialized constraint system and possibly additional functional constants and their types, enjoys syntactic type soundness.

The confinement of object references is a significant security concern for modern programming languages. We define a language that serves as a uniform model for a variety of confined object reference systems. A use-based approach to confinement is adopted, which we argue is more expressive than previous communication-based approaches. We then develop a readable, expressive type system for static analysis of the language, along with a type safety result demonstrating that run-time checks can be eliminated. The language and type system thus serve as a reliable, declarative and efficient foundation for secure capability-based programming and object confinement.

The Java JDK 1.2 Security Architecture includes a dynamic mechanism for enforcing access control checks, so-called stack inspection. This paper studies type systems which can statically guarantee the success of these checks. We develop these systems using a new, systematic methodology: we show that the security-passing style translation, proposed by Wallach and Felten as a dynamic implementation technique, also gives rise to static security-aware type systems, by composition with conventional type systems. To define the latter, we use the general HM(X) framework, and easily construct several constraint- and unification-based type systems. They offer significant improvements on a previous type system for JDK access control, both in terms of expressiveness and in terms of readability of type specifications.

A number of security systems for programming languages have recently appeared, including systems for enforcing some form of access control. The Java JDK 1.2 security architecture is one such system that is widely studied and used. While the architecture has many appealing features, access control checks are all implemented via dynamic method calls. This is a highly non-declarative form of specification which is hard to read, and which leads to additional run-time overhead. In this paper, we present a novel security type system that enforces the same security guarantees as Java Stack Inspection, but via a static type system with no additional run-time checks. The system allows security properties of programs to be clearly expressed within the types themselves. We also define and prove correct an inference algorithm for security types, meaning that the system has the potential to be layered on top of the existing Java architecture, without requiring new syntax.

The Actor Specification Diagram Language is a rigorously defined graphical specification language, with features for modelling concurrency and asynchronous communication. These features make the language appropriate for the formal analysis of distributed security protocols. The graphical nature of the language makes protocol descriptions easy to read and understand, vital properties for appeal to a wider user population. Proofs of protocol correctness can be given via graphical transformation, with each step of transformation justified by rigorous argument if desired. To illustrate the utility of a graphical specification language we analyze the well-known Needham-Schroeder Pubic Key protocol.

Programming language-based security provides applications programmers with greater control and flexibility for specifying and enforcing security policies. As computing environments distribute and diversify, and demands for program mobility increase, this power allows programmers to adapt software to developing needs, while still protecting resources. This thesis advocates the use of static type disciplines for expressing and enforcing programming language-based security. We develop type systems for two popular security models: the Access Control model with Stack Inspection, and the Object Confinement model. Type safety proofs demonstrate that these type systems reliably enforce security statically, and imply that certain run-time optimizations may be effected for programs. The declarative nature of our type terms also provide programmers with useful and understandable descriptions of security properties. To formally develop these type systems, a transformational approach is used, where source languages are embedded in a target language, containing sets of atomic elements and associated operations, which is pre-equipped with a sound type system. This target language and type system is developed using the type constraint framework HM(X). The transformational approach and HM(X) both allow the re-use of existing theory and implementations, easing proof effort, inspiring design, and providing greater confidence in the correctness of results.

The ML datasort declaration is an extension to Standard ML allowing the declaration of refinement types, which correspond to subsets of pre-existing ML datatypes. Refinement types provide the programmer with a more precise method of expressing data structure, can prevent the occurence of certain run -time exceptions, and assist in the expression and maintenance of some representation invariants. ML refinement types correspond to regular term and regular tree languages, except that refinement types are polymorphic. While algorithms have been defined which determine the emptiness, intersection and subset problems for regular terms, the corresponding problems for polymorphic regular terms have not been studied. This thesis formally describes a refinement type language, and defines algorithms relevant to these decision problems, which are proven correct. Along with theoretical interest, these algorithms have practical applications for refinement type checking.