Active Policy Safety Analysis Through Typing
Building a reflective security architecture is attractive
from an object-oriented programming perspective.
However, such a system raises practical analysis and performance concerns that require
study. In particular, we seek analysis tools to show
that given security policies can operate safely within the wider context of
a dynamic security system. The proposed solution to
this issue is addressed through type theory.
We also seek to ensure that the resulting system is not too slow to be of
practical use. The solution this time is to provide a scheme whereby
key components of the
system can be optimized without compromising the overall architecture.
Security Policies and Subtyping
We seek to utilize
Java's inheritance (subclassing) mechanism to ensure the safety
of dynamic security policies.
In so doing, we expect to be able to apply the results of various
type theories to
the security policies.
Well-founded type theories offer a wealth of machinery if they
can be applied to reason
about the operation of security
agents; in particular, type theories offer the prospect of proving
certain properties about the security model.
One motivation for applying type theories to security policies
is to maintain type safety (i.e. to ensure that there are no
runtime violations of type restrictions).
For example, type safety can ensure that a particular active agent
cannot modify the access rights it is given to use a particular resource
in the reference monitor.
However, our desire to utilize inheritance
for subtyping requires us to address an issue that is subject to
much debate in the programming language community---covariant specialization
vs. contravariant substitutivity.
Subclassing is a fundamental mechanism of object-oriented
languages that permits new
objects to be defined in terms of existing base
objects, with the new objects
inheriting properties of the base objects.
The original intent of inheritance was to permit specialization, in
which the base class
and the derived class share some operations and data, but
where the derived class implements additional operations and data.
However, it was quickly realized that inheritance could also serve as
a vehicle for subtyping, which incorporates the notion of
substitutivity, in which a property that is true of a supertype should
also be true when its subtype is substituted.
In terms of the proposed security system, classes describing
active capabilities will be subclassed to add specializations (for example,
a revocation technique.) Revocable capabilities should be usable as
substitutes
for active capabilities. Thus, revocable capabilities would form a subtype
of an active capability. To verify the safety of our dynamic security system,
we need to reason about the safety of such substitutions.
The perceived practical
need to treat binary operators as subtypes has led
to widespread adoption of the covariant rule, despite the type safety problems
that it presents.
Such a solution appears to be unsuitable for our needs. Therefore, we would
look to alternative solutions that researchers have proposed.
Abadi and Cardelli introduce Protocols
as a mechanism for overcoming these difficulties.
Matching captures that concept,
and can be interpreted as either
F-bounded subtyping or as higher-order subtyping.
Whether matching is a suitable replacement for subtyping remains an open issue.
Castagna has argued that the subtyping difficulties
of the contravariant rule can be overcome, with covariance and
contravariance each having a proper place in object-oriented theory.
Two additional approaches to subtyping are
Liskov and Wing's extension subtype and constraint
subtype mechanisms, and there
is a similarity between extension
subtyping and
Castagna's formalism.
An interesting result of Castagna's approach is
that record-based object-oriented
type theories are shown to be extendible to include multiple-dispatching.
We believe that one or more of these approaches will be satisfactory for
our needs. We will investigate whether there is sufficient richness in
any of the formal theories for our purposes. Alternatively, we might find that
a limited form of multiple-dispatch would serve our needs---perhaps
effected through reflective system calls that could vary depending on their
parameters.
In summary, the goal of examining our system from the type theory perspective
is to determine if existing type theories exist to simplify reasoning about
dynamic security policies in the architecture.
We shall investigate:
- Whether security policies can be modeled by existing formal theories.
- Whether efficient single-dispatch object-oriented languages (like
Java) are capable of supporting the necessary theories.
- What properties of security policies cannot be modeled by existing theories.
- What properties of security policies cannot be supported by Java-like
subclassing mechanisms.
- What extensions/modifications must be made to Java's subclassing mechanism
to support security policies, and how efficiently can such extensions be made.
- Whether reflective calls can be used to effect a limited form of
multiple-dispatch that is sufficient to overcome difficulties in type theory.
Reliable High-Performance Compilation
Our approach makes heavy use of Java to perform security authentication
and access control.
We wish to investigate whether it is possible to identify certain
libraries of code that can be optimized so that security tasks
can be performed very efficiently.
If this is possible, then the code generated by compilers would be minimal
(involving simple library calls), and it would be easier to verify
that such code is secure.
An example of one such optimization is that of cryptographic algorithms.
The use of cryptographic techniques is central to encryption,
authentication, signatures, and other security algorithms. Typical
cryptographic algorithms make extensive use of modular
arithmetic on very large integers.
The Intel MMX instruction set is designed to speed up such
computation, so it would be advantageous to
recast existing cryptographic algorithms to take advantage of the MMX
architecture. In addition, certain cryptographic
algorithms may permit parallel computation, further exploiting the MMX
SIMD architecture.
We shall investigate:
- Whether large integer multiplication and modulo arithmetic can be made
to utilize the MMX instruction set.
- Whether cryptographic algorithms involving large integer exponentiation
can be parallelized to take further advantage of the MMX SIMD architecture.
- Whether it is advantageous to embed such cryptographic functions in
the kernel of a security system.
Please send comments and suggestions to Tin Qian
Last modified: Tue Jul 1 14:13:14 CDT