@TECHREPORT{HKM+06tr,
ABSTRACT = {Security-typed languages promise to be a powerful tool with which provably
secure software applications may be developed. Programs written in these
languages enforce a strong, global policy of noninterference for all their
data. Unfortunately, real programs almost always require the use of
noninterference-violating flows introduced by declassification. This
causes the global policy to break down and obscures the meaning of security
labels. These languages suffer from the lack of an alternative, global policy
which can handle declassifications. In this paper, we present
a security-typed, object-oriented language which allows
trusted declassifications based on a global policy. We prove
the
soundness of our language as well as a modified form of noninterference, which
we call noninterference modulo trusted declassification. We implement our declassification mechanism and
global security policy in Jif and provide some examples which motivate its
use.},
ADDRESS = {Department of Computer Science, Pennsylvania State University},
AUTHOR = {Boniface Hicks and Dave King and Patrick McDaniel and Michael Hicks},
DATE-ADDED = {2006-09-27 17:02:16 -0400},
DATE-MODIFIED = {2006-09-27 17:02:16 -0400},
INSTITUTION = {Networking and Security Research Center},
MONTH = {March},
NUMBER = {NAS-TR-0033-2006},
PDF = {papers/hicks06trustedDeclass.pdf},
TITLE = {Trusted Declassification: High-level policy for a security-typed language},
YEAR = {2006}
}
@INPROCEEDINGS{HAM06,
ABSTRACT = {Security-typed languages are an evolving tool for implementing
systems with provable security guarantees. However,
to date, these tools have only been used to build simple
"toy" programs. As described in this paper, we have developed
the first real-world, security-typed application: a secure
email system written in the Java language variant Jif.
Real-world policies are mapped onto the information flows
controlled by the language primitives, and we consider the
process and tractability of broadly enforcing security policy
in commodity applications. We find that while the language
provided the rudimentary tools to achieve low-level security
goals, additional tools, services, and language extensions
were necessary to formulate and enforce application
policy. We detail the design and use of these tools. We also
show how the strong guarantees of Jif in conjunction with
our policy tools can be used to evaluate security. This work
serves as a starting point--we have demonstrated that it is
possible to implement real-world systems and policy using
security-typed languages. However, further investigation of
the developer tools and supporting policy infrastructure is
necessary before they can fulfill their considerable promise
of enabling more secure systems.},
ADDRESS = {Miami, Fl},
AUTHOR = {Boniface Hicks and Kiyan Ahmadizadeh and Patrick McDaniel},
BOOKTITLE = {22st Annual Computer Security Applications Conference (ACSAC)},
DATE-ADDED = {2006-09-27 17:02:13 -0400},
DATE-MODIFIED = {2006-09-27 17:02:13 -0400},
MONTH = {December},
PDF = {papers/hicks-acsac06jpmail.pdf},
TITLE = {Understanding Practical Application Development in Security-typed Languages},
YEAR = {2006}
}
@INPROCEEDINGS{SHT+06,
ABSTRACT = {This paper presents RX, a new security-typed programming
language with features intended to make the management
of information-flow policies more practical. Security
labels in RX, in contrast to prior approaches, are
defined in terms of owned roles, as found in the RT rolebased
trust-management framework. Role-based security
policies allows flexible delegation, and our language RX
provides constructs through which programs can robustly
update policies and react to policy updates dynamically.
Our dynamic semantics use statically verified transactions
to eliminate illegal information flows across updates, which
we call transitive flow. Because policy updates can be observed
through dynamic queries, policy updates can potentially
reveal sensitive information. As such, RX considers
policy statements themselves to be potentially confidential
information and subject to information-flow metapolicies.
},
AUTHOR = {Nikhil Swamy and Michael Hicks and Stephen Tse and Steve Zdancewic},
BOOKTITLE = {Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW'06)},
DATE-ADDED = {2006-04-05 14:52:24 -0400},
DATE-MODIFIED = {2006-04-05 16:29:35 -0400},
LOCAL-URL = {file://localhost/Users/phicks/cs/eclipse/jpmail-web/WebContent/jpmail/papers/swamy06rx.pdf},
MONTH = {July},
NOTE = {to appear},
PDF = {papers/swamy06rx.pdf},
READ = {Yes},
TITLE = {Managing Policy Updates in Security-Typed Languages},
YEAR = {2006}
}
@CONFERENCE{HKM+06,
ABSTRACT = {Security-typed languages promise to be a powerful tool with which
provably secure software applications may be developed. Programs
written in these languages enforce a strong, global policy of nonin-
terference which ensures that high-security data will not be observ-
able on low-security channels. Because noninterference is typically
too strong a property, most programs use some form of declassifi-
cation to selectively leak high security information, e.g. when per-
forming a password check or data encryption. Unfortunately, such
a declassification is often expressed as an operation within a given
program, rather than as part of a global policy, making reasoning
about the security implications of a policy more difficult.
In this paper, we propose a simple idea we call trusted declas-
sification in which special declassifier functions are specified as
part of the global policy. In particular, individual principals declar-
atively specify which declassifiers they trust so that all informa-
tion flows implied by the policy can be reasoned about in absence
of a particular program. We formalize our approach for a Java-
like language and prove a modified form of noninterference which
we call noninterference modulo trusted methods. We have imple-
mented our approach as an extension to Jif and provide some of
our experience using it to build a secure e-mail client.},
ADDRESS = {Ottawa, Canada},
AUTHOR = {Boniface Hicks and Dave King and Patrick McDaniel and Michael Hicks},
BOOKTITLE = {ACM SIGPLAN Workshop on Programming Languages and Analysis for Security},
DATE-ADDED = {2006-04-05 14:52:14 -0400},
DATE-MODIFIED = {2006-04-05 16:16:36 -0400},
LOCAL-URL = {file://localhost/Users/phicks/cs/eclipse/jpmail-web/WebContent/jpmail/papers/plas06.pdf},
MONTH = {June 10},
NOTE = {To appear},
PDF = {papers/plas06.pdf},
TITLE = {Trusted Declassification: High-level policy for a security-typed language},
YEAR = {2006}
}
@INPROCEEDINGS{HTH+05,
ABSTRACT = {Applications that manipulate sensitive information should ensure end-to-end security by satisfying two
properties: sound execution and some form of noninterference. By the former, we mean the program should
always perform actions in keeping with its current policy, and by the latter we mean that these actions should
never cause high-security information to be visible to a low-security observer. Over the last decade, security-
typed languages have been developed that exhibit these properties, increasingly improving so as to model
important features of real programs. No current security-typed language, however, permits general changes
to security policies in use by running programs. This paper presents a simple information flow type system
for that allows for dynamic security policy updates while ensuring sound execution and a relaxed form of
noninterference we term noninterference between updates. We see this work as an important step toward using
language-based techniques to ensure end-to-end security for realistic applications.
},
AUTHOR = {Michael Hicks and Stephen Tse and Boniface Hicks and Steve Zdancewic},
BOOKTITLE = {Proceedings of the Foundations of Computer Security Workshop (FCS '05)},
DATE-ADDED = {2006-04-05 14:52:03 -0400},
DATE-MODIFIED = {2006-04-05 16:16:23 -0400},
LOCAL-URL = {file://localhost/Users/phicks/cs/eclipse/jpmail-web/WebContent/jpmail/papers/dynUpdatingInfoFlow.pdf},
MONTH = {March},
PDF = {papers/dynUpdatingInfoFlow.pdf},
TITLE = {Dynamic Updating of Information-Flow Policies},
YEAR = {2005}
}
This file has been generated by bibtex2html 1.75