skalka-pubs.bib

@inproceedings{capobianco-etal-tapp17,
  author = {Frank Capobianco and Christian Skalka and Trent Jaeger},
  title = {\textcolor{navy}{Tracking the Provenance of Access Control Decisions}},
  booktitle = {International Workshop on Theory and Practice of Provenance (TaPP)},
  year = 2017,
  note = {To appear},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/capobianco-etal-tapp17.pdf},
  abstract = {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.}
}
@inproceedings{petracca-etal-sacmat17,
  author = {Giuseppe Petracca and Frank Capobianco and Christian Skalka and Trent Jaeger},
  title = {\textcolor{navy}{On Risk in Access Control Enforcement}},
  booktitle = {ACM Symposium on Access Control Models and Technologies (SACMAT)},
  year = 2017,
  note = {To appear},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/petracca-etal-sacmat17.pdf},
  abstract = {While we have long had principles describing how access
                  control enforcement should be implemented, such as
                  the reference moni- tor concept, imprecision in
                  access control mechanisms and access control
                  policies leads to risks that may enable
                  exploitation. In prac- tice, least privilege access
                  control policies oen allow information ows that may
                  enable exploits. In addition, the implementation of
                  access control mechanisms oen 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 dene 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
                  beer understand the potential of risk estimation for
                  authorization, we propose risk estimate functions
                  for each of the four types of risk, nding that
                  benign program deployments accumulate risks in each
                  of the four areas for ten Android programs
                  examined. As a result, we nd 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 diers from that expected.}
}
@inproceedings{basu-etal-ancs17,
  author = {Shrutarshi Basu and Nate Foster and Hossein Hojjat and Paparao Palacharla and Christian Skalka and Xi Wang},
  title = {\textcolor{navy}{Life on the Edge: Unraveling Policies into Configurations}},
  booktitle = {ACM/IEEE Symposium on Architectures for Networking and Communications Systems (ANCS)},
  year = 2017,
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/basu-etal-ancs17.pdf},
  abstract = {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.  }
}
@article{price-etal-jtbs17,
  author = {Price, M. and van Stolk-Cooke, K. and Ward., H. L. and O’Keefe, M. and Gratton, J. and Skalka, C. and Freeman, K. },
  title = {\textcolor{navy}{Tracking Post-Trauma Psychopathology Using Mobile Applications: A Usability Study}},
  journal = {Journal of Technology in Behavioral Science},
  year = 2017,
  pages = {1--8},
  issn = {2366-5963},
  doi = {10.1007/s41347-016-0008-9},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/price-etal-jtbs17.pdf},
  abstract = { 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.}
}
@inproceedings{amir-skalka-plas16,
  author = {Sepehr Amir-Mohammadian and Christian Skalka},
  title = {\textcolor{navy}{In-Depth Enforcement of Dynamic Integrity Taint Analysis}},
  booktitle = {ACM Programming Languages and Security Workshop (PLAS)},
  year = 2016,
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/amir-skalka-plas16.pdf},
  abstract = {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
                  \emph{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.}
}
@inproceedings{kriegman-etal-ppsn16.pdf,
  author = {Sam Kriegman and Marcin Szubert and Josh Bongard and Christian Skalka},
  title = {\textcolor{navy}{Evolving Spatially Aggregated Features From Satellite Imagery for Regional Modelin}},
  booktitle = {International Conference on Parallel Problem Solving from Nature (PPSN)},
  year = 2016,
  note = {Nominated for Best Paper Award.},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/kriegman-etal-ppsn16.pdf},
  abstract = { 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.  }
}
@incollection{yousefi-skalka-bongard-ciwsn16,
  author = {Afsoon Yousefi and Christian Skalka and Josh Bongard},
  title = {\textcolor{navy}{A Genetic Programming Approach to Cost-Sensitive Control in Wireless Sensor Networks}},
  booktitle = {Computational Intelligence in Wireless Sensor Networks: Recent Advances and Future Challenges},
  publisher = {Springer},
  year = 2016,
  publisher = {Springer International Publishing},
  pages = {1--31},
  isbn = {978-3-319-47715-2},
  doi = {10.1007/978-3-319-47715-2_1},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/yousefi-skalka-bongard-ciwsn16.pdf},
  abstract = { In some wireless sensor network applications, multiple
                  sensors can be used to measure the same variable,
                  while differing in their sampling \emph{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.  }
}
@inproceedings{amir-chong-skalka-post16,
  author = {Sepehr Amir-Mohammadian and Stephen Chong and Christian Skalka},
  title = {\textcolor{navy}{Correct Audit Logging: Theory and Practice}},
  booktitle = {Principles of Security and Trust (POST)},
  year = 2016,
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/amir-chong-skalka-post16.pdf},
  abstract = { 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.  }
}
@article{price-etal-jmir15,
  author = {Matthew Price and Tyler J. Sawyer and Madison Harris and Christian Skalka},
  title = {\textcolor{navy}{Usability Evaluation of a Mobile Monitoring System to Assess Symptoms After a Traumatic Injury: A Mixed Method Study.}},
  journal = {Journal of Medical Internet Research – Mental Health},
  year = {2016},
  month = {Jan},
  day = {11},
  volume = {3},
  number = {1},
  pages = {e3},
  doi = {10.2196/mental.5023},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/price-etal-jmir15.pdf},
  abstract = { 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.  }
}
@inproceedings{amir-chong-skalka-law15,
  author = {Sepehr Amir-Mohammadian and Stephen Chong and Christian Skalka},
  title = {\textcolor{navy}{Foundations for Auditing Assurance}},
  booktitle = {Layered Assurance Workshop (LAW)},
  year = 2015,
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/amir-chong-skalka-law15.pdf},
  abstract = { 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.  }
}
@inproceedings{zowj-bongard-skalka-gecco15,
  author = {Afsoon Yousefi Zowj and Joshua C Bongard and Christian Skalka},
  title = {\textcolor{navy}{A Genetic Programming Approach to Cost-Sensitive Control in Resource Constrained Sensor Systems}},
  booktitle = {ACM Genetic and Evolutionary Computation Conference (GECCO)},
  year = 2015,
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/zowj-bongard-skalka-gecco15.pdf},
  abstract = { 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.  }
}
@article{buckingham-skalka-bongard-jhydro15not,
  author = {David Buckingham and Christian Skalka and Joshua Bongard},
  title = {\textcolor{navy}{Inductive Learning of Snowpack Distribution Models for Improved Estimation of Areal Snow Water Equivalent}},
  journal = {Journal of Hydrology},
  year = 2015,
  volume = 524,
  pages = {311-325},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/buckingham-bongard-skalka-jhydro15.pdf},
  abstract = { 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.}
}
@inproceedings{ganapathy-jaeger-skalka-tan-law14,
  author = {Vinod Ganapathy and Trent Jaeger and Christian Skalka and Gang Tan},
  title = {\textcolor{navy}{Assurance for Defense in Depth via Retrofitting}},
  booktitle = {Layered Assurance Workshop},
  year = 2014,
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/ganapathy-jaeger-skalka-tan-law14.pdf},
  abstract = {The computer security community has long advocated
                  \textit{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 {\em 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. }
}
@article{chong-skalka-vaughan-jdiq14,
  author = {Stephen Chong and Christian Skalka and Jeffrey A. Vaughan},
  title = {\textcolor{navy}{Self-Identifying Data for Fair Use}},
  journal = {ACM Journal of Data and Information Quality},
  year = 2014,
  volume = 5,
  number = 3,
  pages = {Article 11},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/chong-skalka-vaughan-jdiq14.pdf},
  abstract = { 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.  }
}
@article{chapin-skalka-tissec14,
  author = {Peter Chapin and Christian Skalka},
  title = {\textcolor{navy}{{SpartanRPC}: Remote Procedure Call Authorization in Wireless Sensor Networks}},
  journal = {ACM Transactions on Information and System Security},
  year = 2014,
  volume = 17,
  number = 2,
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/chapin-skalka-tissec14.pdf},
  abstract = {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.
  }
}
@inproceedings{chapin-etal-gpce13,
  author = {Peter Chapin and Christian Skalka and Scott Smith and Michael Watson},
  title = {\textcolor{navy}{{Scalaness/nesT}: Type Specialized Staged Programming for Sensor Networks}},
  year = 2013,
  booktitle = {ACM Generic Programming: Concepts and Experiences (GPCE)},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/chapin-etal-gpce13.pdf},
  abstract = {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.}
}
@inproceedings{skalka-frolik-realwsn13,
  author = {Christian Skalka and Jeff Frolik},
  title = {\textcolor{navy}{Snowcloud: A Complete System for Snow Hydrology Research}},
  year = 2013,
  booktitle = {ACM Workshop on Real-World Wireless Sensor Networks (RealWSN)},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/skalka-frolik-realwsn13.pdf},
  abstract = {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.  }
}
@article{liu-skalka-smith-hosc11submitted,
  author = {Yu David Liu and Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{Type-Specialized Staged Programming with Process Separation}},
  journal = {Journal of Higher Order and Symbolic Computation},
  year = 2012,
  address = {Edinburgh, Scotland},
  volume = 24,
  number = 4,
  pages = {341-385},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/liu-skalka-smith-hosc11submitted.pdf},
  abstract = {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, , which extends the programmability of staged
  languages in two directions.
%
  First,  supports \emph{dynamic type specialization}: types
  can be dynamically constructed, abstracted, and passed as arguments,
  while preserving decidable typechecking via a System F$_\le$-style
  semantics combined with a restricted form of $\lambda_\omega$-style
  runtime type construction. With dynamic type specialization the data structure
  layout of a program can be optimized via staging.
%
  Second,  works in a context where different stages of
  computation are executed in different process spaces, a property we
  term \emph{staged process separation}.  Programs at different stages
  can directly communicate program data in  via a built-in
  serialization discipline.
%
  The language  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.
  }
}
@inproceedings{moeser-walker-skalka-frolik-wsc11,
  author = {C. David Moeser and Mark Walker and Christian Skalka and Jeff Frolik},
  title = {\textcolor{navy}{Application of a wireless sensor network for
distributed snow water equivalence estimation}},
  year = 2011,
  booktitle = {Western Snow Conference},
  docx = {http://www.cems.uvm.edu/~skalka/skalka-pubs/moeser-walker-skalka-frolik-wsc11.docx},
  abstract = {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 % canopy
              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. }
}
@inproceedings{chapin-skalka-mass10,
  author = {Peter Chapin and Christian Skalka},
  title = {\textcolor{navy}{SpartanRPC: WSN Middleware for Cooperating Domains}},
  year = 2010,
  booktitle = {IEEE Conference on Mobile and Ad-Hoc Sensor Systems},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/chapin-skalka-mass10.pdf},
  abstract = {
	          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.
	}
}
@inproceedings{chong-skalka-vaughan-ipsn10,
  author = {Stephen Chong and Christian Skalka and Jeffrey A. Vaughan},
  title = {\textcolor{navy}{Self-Identifying Sensor Data}},
  year = 2010,
  booktitle = {ACM Conference on Information Processing in Sensor Networks (IPSN)},
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/chong-skalka-vaughan-ipsn10.pdf},
  abstract = {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.}
}
@inproceedings{liu-skalka-smith-wgp09,
  author = {Yu David Liu and Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{Type-Specialized Staged Programming with Process Separation}},
  booktitle = {Workshop on Generic Programming (WGP09)},
  year = 2009,
  address = {Edinburgh, Scotland},
  note = {\emph{Note:} this version contains minor revisions to the article published
in WGP09 Proceedings. },
  pdf = {http://www.cems.uvm.edu/~skalka/skalka-pubs/liu-skalka-smith-wgp09.pdf},
  abstract = {Staging is a powerful language construct that allows a
              program at one stage to manipulate and specialize a
              program at the next.  We propose  as a new
              staged calculus designed with novel features for staged
              programming in modern computing platforms such as
              embedded systems.  A distinguishing feature of
               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.   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.  }
}
@techreport{makarov-skalka-techreport09,
  author = {Evgeny Makarov and Christian Skalka},
  title = {\textcolor{navy}{Formalized Proof of Type Safety of Hoare Type Theory}},
  institution = {The University of Vermont},
  year = 2009,
  number = {CS-09-01},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/makarov-skalka-tr09.pdf },
  abstract = {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.  }
}
@inproceedings{skalka-etal-issw08,
  author = {Christian Skalka and Jeff Frolik and Beverley Wemple},
  title = {\textcolor{navy}{A Distributed In Situ System for Snow Water Equivalence Measurement}},
  booktitle = {International Snow Science Workshop},
  year = 2008,
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-etal-issw08.pdf},
  abstract = {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.}
}
@article{skalka-hosc08,
  author = {Christian Skalka},
  title = {\textcolor{navy}{Types and Trace Effects for Object Orientation}},
  year = {2008},
  journal = {Journal of Higher Order and Symbolic Computation},
  volume = 21,
  number = 3,
  pages = {239-282},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-hosc08.pdf},
  abstract = {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.},
  note = {Extended version of \cite{skalka-ppdp05}.}
}
@article{chapin-skalka-wang-acmcs07,
  author = {Peter Chapin and Christian Skalka and X. Sean Wang},
  title = {\textcolor{navy}{Authorization in Trust Management: Features and Foundations}},
  volume = 40,
  number = 3,
  pages = {1-48},
  year = {2008},
  journal = {ACM Computing Surveys},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/chapin-skalka-wang-acmcs07.pdf},
  abstract = {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.}
}
@article{skalka-smith-vanhorn-jfp08,
  author = {Christian Skalka and Scott Smith and David Van Horn},
  title = {\textcolor{navy}{Types and Trace Effects of Higher Order
  Programs}},
  year = {2008},
  volume = 18,
  number = 2,
  pages = {179-249},
  journal = {Journal of Functional Programming},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-vanhorn-jfp07.pdf},
  abstract = {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 \emph{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
              $\lambda$-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 \emph{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.},
  note = {Extended version of \cite{skalka-smith-aplas04}}
}
@inproceedings{shroff-smith-skalka-aplas07,
  author = {Paritosh Shroff and Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{The Nuggetizer: Abstracting Away Higher Orderness for Program Verification.}},
  year = {2007},
  booktitle = {Proceedings of the Asian Programming Languages Symposium},
  pdf = {http://www.cs.jhu.edu/~scott/pll/papers/nuggetizer-aplas07.pdf},
  abstract = {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 \emph{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 \emph{prune-rerun} analysis
              technique to approximate higher-order recursive
              computations.}
}
@inproceedings{skalka-ppdp07,
  author = {Christian Skalka},
  title = {\textcolor{navy}{Type Safe Dynamic Linking for {JVM} Access Control}},
  year = {2007},
  booktitle = {Proceedings of the ACM Symposium on Principles and Practice
of Declarative Programming},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-ppdp07.pdf},
  abstract = {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.}
}
@article{skalka-wang-chapin-jcs07,
  author = {Christian Skalka and X. Sean Wang and Peter Chapin},
  title = {\textcolor{navy}{Risk Management for Distributed Authorization}},
  year = {2007},
  volume = 15,
  number = 4,
  pages = {447-489},
  journal = {Journal of Computer Security},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-wang-chapin-jcs07.pdf},
  abstract = {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.},
  note = {Extended version of \cite{chapin-skalka-wang-fmse05}}
}
@article{skalka-hosc06submitted,
  author = {Christian Skalka},
  title = {\textcolor{navy}{Types and Trace Effects for Object Orientation}},
  year = {2007},
  journal = {Journal of Higher Order and Symbolic Computation},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-hosc06submitted.pdf},
  abstract = {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.},
  note = {Extended version of \cite{skalka-ppdp05}.}
}
@inproceedings{polakow-skalka-plas06,
  author = {Jeff Polakow and Christian Skalka},
  title = {\textcolor{navy}{Specifying Distributed Trust Management in {LolliMon}}},
  booktitle = {Proceedings of the ACM Workshop on Programming Languages and Analysis for Security},
  year = {2006},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/polakow-skalka-plas06.pdf},
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/polakow-skalka-plas06.ps},
  abstract = {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.}
}
@article{skalka-wang-csse06,
  author = {Christian Skalka and X. Sean Wang},
  title = {\textcolor{navy}{Trust but Verify: Authorization for Web Services}},
  journal = {Journal of Computer Systems Science and Engineering},
  year = {2006},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-wang-csse06.pdf},
  abstract = {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.}
}
@inproceedings{chapin-skalka-wang-fmse05,
  author = {Peter Chapin and Christian Skalka and X. Sean Wang},
  title = {\textcolor{navy}{Risk Assessment in Distributed Authorization}},
  booktitle = {Proceedings of the ACM Workshop on Formal Methods in Security Engineering},
  year = 2005,
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/chapin-skalka-wang-fmse05.pdf},
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/chapin-skalka-wang-fmse05.ps},
  abstract = {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.}
}
@inproceedings{skalka-ppdp05,
  author = {Christian Skalka},
  title = {\textcolor{navy}{Trace Effects and Object Orientation}},
  booktitle = {Proceedings of the ACM Conference on Principles and Practice of Declarative Programming},
  year = 2005,
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-ppdp05.pdf},
  abstract = {\emph{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.}
}
@inproceedings{skalka-smith-vanhorn-aiool05,
  author = {Christian Skalka and Scott Smith and David Van Horn},
  title = {\textcolor{navy}{A Type and Effect System for Flexible Abstract Interpretation of Java}},
  booktitle = {Proceedings of the ACM Workshop on Abstract Interpretation of Object Oriented Languages},
  year = 2005,
  series = {Electronic Notes in Theoretical Computer Science},
  month = {January},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-vanhorn-aiool05.pdf},
  abstract = {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.}
}
@article{pottier-skalka-smith-toplas05,
  author = {François Pottier and Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{A Systematic Approach to Static Access Control}},
  journal = {ACM Transactions on Programming Languages and Systems},
  year = {2005},
  volume = 27,
  number = 2,
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/fpottier-skalka-smith-toplas03.pdf},
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/fpottier-skalka-smith-toplas03.ps},
  abstract = {The Java Security Architecture includes a dynamic mechanism for
              enforcing access control checks, the so-called
              \emph{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
              \emph{dynamic} implementation technique, also gives rise
              to \emph{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.}
}
@article{skalka-smith-ijis05,
  author = {Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{Static Use-Based Object Confinement}},
  journal = {Springer International Journal of Information Security},
  year = {2005},
  volume = {4},
  number = {1-2},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-ijis05.pdf},
  abstract = {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
              \emph{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.}
}
@inproceedings{skalka-wang-sws04,
  author = {Christian Skalka and X. Sean Wang},
  title = {\textcolor{navy}{Trust but Verify: Authorization for Web Services}},
  booktitle = {ACM Workshop on Secure Web Services},
  year = 2004,
  month = {October},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-wang-sws04.pdf},
  abstract = {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.}
}
@inproceedings{skalka-smith-aplas04,
  author = {Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{History Effects and Verification}},
  booktitle = {Asian Programming Languages Symposium},
  month = {November},
  year = 2004,
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-aplas04.pdf},
  abstract = {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 \emph{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 $\lambda$-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 \emph{history effects} inferred by the type
              inference algorithm, allowing static enforcement of
              history- and stack-based security mechanisms.}
}
@article{skalka-smith-entcs03,
  author = {Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{Set Types and Applications}},
  year = {2003},
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-entcs03.ps},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-entcs03.pdf},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {75},
  abstract = {We present $\mathrm{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
              $\mathrm{pml}_B$ by showing how it can serve as a practical
              \emph{implementation} language for higher-level
              programming language based security systems, and
              characterize $\mathrm{pml}_B$ by comparing the expressiveness of
              $\mathrm{pml}_B$ sets with enumerations.}
}
@article{skalka-pottier-entcs03,
  author = {Christian Skalka and François Pottier},
  title = {\textcolor{navy}{Syntactic Type Soundness for HM$(X)$}},
  year = {2003},
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-pottier-entcs03.ps},
  pdf = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-pottier-entcs03.pdf},
  journal = {Electronic Notes in Theoretical Computer Science},
  volume = {75},
  abstract = {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.}
}
@inproceedings{skalka-smith-fcs02,
  author = {Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{Static Use-Based Object Confinement}},
  booktitle = {Proceedings of the Foundations of Computer Security Workshop (FCS
'02)},
  month = {July},
  year = {2002},
  address = {Copenhagen, Denmark},
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-fcs02.ps},
  abstract = {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
              \emph{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.}
}
@inproceedings{pottier-skalka-smith-esop01,
  author = {François Pottier and Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{A Systematic Approach to Static Access Control}},
  booktitle = {Proceedings of the 10th European Symposium on
                 Programming (ESOP'01)},
  editor = {David Sands},
  publisher = {Springer Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {2028},
  pages = {30--45},
  month = apr,
  year = {2001},
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/fpottier-skalka-smith-esop01.ps},
  springer = {http://link.springer.de/link/service/series/0558/tocs/t2028.htm},
  abstract = {The Java JDK 1.2 Security Architecture includes a
                  dynamic mechanism for enforcing access control
                  checks, so-called \emph{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 \emph{dynamic}
                  implementation technique, also gives rise to
                  \emph{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.}
}
@inproceedings{skalka-smith-icfp00,
  author = {Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{Static Enforcement of Security with Types}},
  booktitle = {Proceedings of the the Fifth {ACM} {SIGPLAN}
                 International Conference on Functional Programming
                 (ICFP'00)},
  month = sep,
  year = {2000},
  pages = {34--45},
  address = {Montréal, Canada},
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-icfp00.ps},
  abstract = {A number of security systems for programming languages
               have recently appeared, including systems for enforcing
               some form of \emph{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 \textit{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.}
}
@techreport{skalka-smith-specdiag02,
  author = {Christian Skalka and Scott Smith},
  title = {\textcolor{navy}{Diagrammatic Verification of Security Protocols}},
  institution = {The Johns Hopkins University},
  year = 2002,
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-smith-specdiag02.ps},
  abstract = {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.  }
}
@phdthesis{skalka-phd-thesis,
  author = {Christian Skalka},
  title = {\textcolor{navy}{Types for Programming Language-Based Security}},
  school = {The Johns Hopkins University},
  year = {2002},
  month = aug,
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-phd-thesis.ps},
  abstract = {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 \emph{Access Control}
               model with \emph{Stack Inspection}, and the
               \emph{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.}
}
@mastersthesis{skalka-ms-thesis,
  author = {Christian Skalka},
  title = {\textcolor{navy}{Some Decision Problems for {ML} Refinement Types}},
  school = {Carnegie Mellon University},
  year = 1997,
  ps = {http://www.cs.uvm.edu/~skalka/skalka-pubs/skalka-ms-thesis.ps},
  abstract = {The ML \texttt{datasort} declaration is an extension to
              Standard ML allowing the declaration of \emph{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.}
}

This file was generated by bibtex2html 1.97.