Jif Tools for Application Development

Software Engineering:
A Jif IDE using Eclipse

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 development.

IBM's Eclipse 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.

A high-level policy tool for Jif

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 themselves).
  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.

Distributed policy tools for Jif

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 distributed environment.

• 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. The 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.