Jif development is prohibitive for large applications, as two recent
case studies (including our own) have shown. If Jif programming is to
become practical, some tools are needed to aid in application
framework has been used for building various Integrated Development
Environments, notably for Java and C. We are developing a new IDE for
secure programming in Jif.
For more information, downloads and installation instructions,
see the Jifclipse page.
Jif lacks a policy management infrastructure. We developed
such an infrastructure consisting of two components:
a runtime policy store that provides dynamic
access to principals, and a policy compiler that automatically
generates principals. Our high-level policy tool is based on Trusted Declassification
- Policy store The policy store is a runtime
data structure and collection of methods that provide
for the dynamic look-up of Jif principals by name. The policy store contains
the collection of principals for a system; each principal contains its own
policy, (thus the name, "policy" store).
By initializing the policy store at the outset of a
program, we can impose a single policy on a whole
program, carefully regulating where (i.e. in which declassifiers), how and by
whom declassifications are allowed to take place.
Furthermore, we have easy access to a central store
of dynamic principals that can be applied to incoming
data. Finally, this policy store gives us a starting point
for building a distributed policy store that can govern
the policy on a distributed network of applications.
- Policy compiler The Jif tools lack utilities to specify high-level policy.
In particular, we desire to automatically generate Jif
policy infrastructure (code) from high level specifications.
To this end, we developed a simple policy language
and an accompanying compiler. Currently, the
policy language consists of only two types of policy
statements: delegations and declassifier-allowances
(implicitly, there is also the declaration of the principals
Policy is integrated into a Jif program by using the
policy compiler. The compiler interprets the policy
specification and generates the associated Jif code.
The created code provides functions for the creation
of principals (as identified in the specification) and for
their insertion in the policy store. The policy specification
also includes explicit authorizations of all the
declassifiers that the principals trust. Functions for
the policy initialization and principal delegations described
in the policy file are also created. Finally, this
automatically generated code is introduced into the Jif
application with a single line of Jif code. A diagram
of this process is given here.
For Jif-labeled data to pass outside a Jif application and retain its
policy, some special steps must be taken. We provide some tools for
extending an application's policy beyond the application itself. Since
most Jif applications (for the foreseeable future) will need to interact
with non-Jif components, there must be some reliable way to talk about
principals and policy outside of a Jif application. To do this, we
provide a policy store for mapping Strings to principals and some
cryptographic tools for maintaining principal identities in a
- Policy Store How should Jif labels and principals be
represented outside of Jif applications? We chose to represent
principals by using their name, stored in a String. When a principal
re-enters a Jif application, this name must be re-associated with the
corresponding Jif principal. The policy store maps (String) names to
Jif principals. The Jif principals, themselves, contain their policy
(allowed delegations and declassifications). This makes it possible to
send data outside a Jif application: it can be labeled with a String
and then on re-arrival in a Jif application, the label can be
re-associated with a Jif principal.
- KeyPrincipal In order to maintain the
consistency of principals between applications, each principal should
be associated with a public key and data which passes outside a Jif
application should be encoded with the public key for that principal.
KeyPrincipal class serves to associate a Jif principal
with a public key. These public keys are read from certificates which
have been signed by a trusted certificate authority (CA). In essence, a
distributed system of Jif applications should be parameterized by a
single CA to ensure principal consistency.
- "Logging in" This small extension to the Jif runtime system
allows a user to "log in" to a Jif program as a particular principal.
The authentication for this login is that the user can provide the
private key for the particular principal (certified by a particular CA,
stored in a local keystore). When the authentication is successful, the
runtime system can be safely labeled with this principal, including the
file system and stdin/stdout.
These distributed policy tools are still under construction. Currently,
the policy and certificates are stored in the local file system and must
be synchronized outside of a Jif application. In the future there will
be a distributed policy store from which principals' certificates and
policy can be loaded.