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