skalka-pubs.bib


@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. }
}


@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 = 2011,
  ADDRESS = {Edinburgh, Scotland},
  NOTE = {Accepted for Publication.},
  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{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 has been generated by bibtex2html 1.54