Jifclipse

Software Engineering:
A Jif IDE using Eclipse

Installation instructions at the bottom of this page.

Jif development is prohibitive for large applications, as some recent case studies 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, but also for LaTeX, web tools, AspectJ and many more. We are developing a new IDE for secure programming in Jif.

Security-typed languages such as Jif require the programmer to reason about security during the initial development process. Software that produces the correct results is no longer sufficient; it is also necessary to work out the information flows that will occur in the application. This requires the programmer to determine in advance 1) the entities (principals) that will handle data in the system, 2) the security policies (labels) that should govern individual program variables and 3) the interaction of variables throughout the application (information flows).

While principal determination must occur largely in the design phase (and can involve complicated interactions between PKIs, system labels and other data classifications), labeling data and resolving information flows occur iteratively during the coding phase in STL application development. Code that the programmer thought would respect secure data flows will often fail to compile and so the programmer must relabel variables as the compiler flags potential information leaks. To complicate matters, the information flow violations can be quite subtle and are not easily expressed by simple error messages. Even though the message may accurately describe an information leak, it may not clearly illuminate the source of the error. This is only further complicated when the language handles not only confidentiality policies, but also integrity policies, not only explicit data flows but also implicit control flows. Inferred and default labels, while important to reducing the programmer's burden in providing labels, also cloud the process of tracking down label conflicts. It is our position that error resolution is one of the key issues currently facing security-typed language development: without better tools for finding and fixing errors, using these languages will remain impractical.

Our plug-in provides a Jif programmer with additional tools to view hidden information generated by a Jif compilation, to suggest fixes for errors, and to get more specific information behind an error message. Better development tools are essential for making security-typed application development practical; Jifclipse is a first step in this process.

Visualization Tools

The Jif compiler must generate a large set of constraints for tracking explicit and implicit information flows. To make these constraints more understandable, Jifclipse provides two Views, the Constraint View and the PC Label View.
  1. Constraint View
    The Constraint View exposes all of the constraints associated with a piece of code and all of the constraints that share variables with that constraint.


  2. PC Label View
    The PC Label View shows the different values that the program counter takes on at different points in the code. If the programmer double-clicks on a displayed label, the system reports exactly why the program counter has been changed to this new value.


  3. Outline View

    If a Jif programmer does not give explicit security labels for data in his code, a default value is used. (The exception is local variables; these are inferred by the compiler.) Method headers have three important labels associated with them; the return value label, the return label, and the begin label. If not explicitly annotated, the return value and return labels default to the bottom label, while the begin label defaults to the top label. Method arguments, if unlabeled, default to the most restrictive security level.

    In order to reveal these implicit labelings, Jifclipse has an outline viewer. Jifclipse explicitly shows the programmer what the implicit labels are on their fields and methods. The Figure shows the outline view of a given class, with the labels for method headers made explicit.




Automation Tools

  1. Quick fixing label errors

    Many label errors in Jif result from the programmer incorrectly declaring the label on a variable. This is especially true for the declared labels on the upper bound of method arguments and the begin label. If a Jif program fails to compile, then Jifclipse examines each of the variables involved with the broken constraint and attempts to determine, using an advanced inference framework, what its label should be. Though this is a fairly simple approach, it gives good results in practice and can be augmented with more advanced techniques in the future.

    This is implemented through the "Quick Fix" framework in Eclipse. The Figure shows Jifclipse suggesting that the programmer change the explicit label on a variable declaration. In the code above, the programmer has incorrectly declared totalAlice, a variable keeping track of how many answers the student Alice has gotten correct, as having {Alice:} level security, when in fact this value needs to be modified using information that the Examiner has. Jifclipse suggests raising the variable totalAlice to its correct security level.

    Jifclipse can also suggest modifications to a method's begin label or labels on method arguments; we briefly describe the differences between the solver provided by the Jif compiler and our compiler in the following section.

  2. Quick fixing declassification

    Sometimes a security constraint is unsatisfiable because of a fundamental conflict between security requirements. In this case, Jif allows adding a declassifier to explicitly lower the sensitivity of a security level. To aid the programmer in this, Jifclipse provides a feature to automatically declassify an expression and the current program counter, if necessary.

    In the Figure, the programmer has written code that he believes will tell a Student their result, stored in totalValue and declared to have security label {Student:; Examiner:}. However, the Student interface (as presently written) expects that the result told to the student is owned wholly by the student, having label {Student:}. This causes a security violation, as we cannot lower the security label on totalValue just by passing it to a function. Jifclipse suggests adding an explicit declassifier to lower totalValue to the expected security level of the student. Other fixes suggested by the IDE may explicitly declassify the program counter as well or instead of the data, as necessary.

Installing Jifclipse

Jifclipse works with Eclipse 3.2. Installing Jifclipse requires two steps. First, the plugin must be updated via the eclipse update feature. Second, the Jif installation must be installed (from Cornell) and updated with our additions to the compiler.

  1. The plugin
    You can install the Jifclipse plugin by using the software updates feature provided in eclipse.
    1. select Help > Software Updates > Find and Install...
    2. Choose "Search for new features to install"
    3. Click "New remote site"
    4. Name: Jifclipse
      URL: http://siis.cse.psu.edu/jifclipse/update
    5. Click "Finish"
    6. Select check box for "Jifclipse" and click "Next"
    7. "Jifclipse feature 2.0.0" and read/accept license agreement
    8. click "Next" and "Finish"
    9. Restart Eclipse
  2. Updating the Jif compiler
    To work with our plugin, the Jif compiler must be updated to save additional information about each compilation (this will be integrated into an upcoming version of Jif, but for now the compiler must be updated by hand). To do this,
    1. Download the Jif compiler and follow the instructions provided to compile the Jif runtime (at least). Currently you must download Jif 3.0.0; we are working on integration of Jifclipse with more recent releases of Jif.
    2. Download our updated jif.jar and build file: Jif updates for Jifclipse.
    3. Unzip jifclipse-aux.zip into the Jif directory (the jifclipse-build.xml file should be in the main Jif directory--/usr/local/jif-3.0.0, e.g. and the jif.jar will be placed into /usr/local/jif-3.0.0/lib). You should be prompted whether you want to replace lib/jif.jar and you should answer "yes". Note: you MUST compile the Jif runtime before performing this update.
    4. (If you needed to edit the build.xml file for Jif to add the headers include directory, the same edit will be required for the Jifclipse build file.)
    5. Rebuild the Jif lib and sig jars by running ant:
      ant -f jifclipse-build.xml
    6. Start up Eclipse and use Project > New > Jif > Jif Project to create a new Jif Project
    7. When creating a new Jif project, it should be configured to point to the base directory of the Jif compiler. See the Startup Tutorial for a demonstration.

Tutorials

Some tutorial movies for getting started with Jifclipse and learning more about its features.
  1. Making a new project
    This tutorial goes through the steps of 1) creating a new project, 2) creating a simple file, 3) compiling it, and 4) using error messages and Quick Fixes to help it compile successfully. Download movie
  2. More to come soon...