Toward Specifying and Validating Cross-Domain Policies
Toward Specifying and Validating Cross-Domain Policies
Files
Publication or External Link
Date
2007-04-17
Authors
Hicks, Michael
Swamy, Nikhil
Tsang, Simon
Advisor
Citation
DRUM DOI
Abstract
Formal security policies are extremely useful for two related reasons.
First, they allow a policy to be considered in isolation, separate
from programs under the purview of the policy and separate from the
implementation of the policy's enforcement. Second, policies can be
checked for compliance against higher-level security goals by using
automated analyses. By contrast, ad hoc enforcement mechanisms (for
which no separate policies are specified) enjoy neither benefit, and
non-formal policies enjoy the first but not the second.
We would like to understand how best to define
(and enforce) multi-level security policies when information must be
shared across domains that have varying levels of trust (the so-called
"cross domain" problem). Because we wish to show such policies meet
higher-level security goals with high assurance, we are interested in
specifying cross domain policies formally, and then reasoning about
them using automated tools. In this report, we briefly survey
work that presents formal security policies with cross-domain
concerns, in particular with respect to the problem of
downgrading. We also describe correctness properties for such
policies, all based on noninterference. Finally, we briefly
discuss recently-developed tools for analyzing formal security
policies; though no existing tools focus on the analysis of
downgrading-oriented policies, existing research points the way
to providing such support.