/Co-InflowPrototype

Evaluation of Co-Inflow using IFSpec benchmark

Primary LanguageJavaMIT LicenseMIT

(Oakland 2021 Co-Inflow paper) Co-Inflow Prototype (for Java 8)

Paper

This repo contains a prototype implementation of our Oakland 2021 paper: Co-Inflow: Coarse-grained Information Flow Control for Java-like Languages.(link)

Overview

The directory of this repo is the following:

.
├── Co-Inflow.release       # Co-Inflow prototype release
├── Co-Inflow.demo          # The example used in the paper
├── IFSPEC                  # Core suite of IFSpec benchmark
├── IFSpec_harness          # Harness program for using Co-Inflow tool on the IFSpec benchmarks

Except for the IFSPEC, the other three are implemented as Eclispe projects. Project Co-Inflow.demo and IFSpec_harness depend on the project Co-Inflow.release to run. The projects can be exported to runnable jars. We may work on migrating the projects to maven later.

The current prototype doesn't focus on performance. It should have a great potential for improvement. We will make regular update to improve the tool.

Co-Inflow.release

The implementation relies on source code rewriting. The source code analysis tool Spoon is used to insert calls to Co-Inflow runtime in the source code. The resulting Java programs explicitly track the current label of containers and the field and object labels of objects, and constructs and destructs labeled values and opaque labeled values.

Structure

├── lbs.harvard.coinflow                     # User APIs, in particular, the CoInflowUserAPI.java
├── lbs.harvard.coinflow.compiler            # Co-Inflow compiler implementation. 
                                               The compiler is implemented as a series of Spoon processors.
                                               CoInflowCompiler.java is the main file.
├── lbs.harvard.coinflow.internal            # Co-Inflow runtime. IFCUtil.java is the main file. 
├── lbs.harvard.coinflow.lattice             # Lattice for Co-Inflow
├── lbs.harvard.coinflow.lattice.impl        # A graph implementation of the lattice
├── lbs.harvard.coinflow.lattice.principal   # Principal used for lattice, mostly reserved for future use
├── lbs.harvard.coinflow.util                # Helper classes. _Rewriter.java_ is the main file. 
├── lbs.harvard.coinflow.util.rifl           # RIFLParser.java parses rifl.xml (for IFSPEC benchmarking)

Co-Inflow.demo

The phone number example shown in the paper.

Usage

Run the CoInflowCompiler program with two arguments: (1) a source folder, and (2) a destination folder. For example,

  • From Eclipse, right click CoInflowCompiler.java -> "run as" -> "run configuration" -> "Argument" tab -> put source folder and output folder in the textbox;
  • From the command line: java CoInflowCompiler "../coinflow.demos/src/" "pathto/output/folder" (after java compilation)

This example has three files. The code alice.setPhoneNum(b1) in the file Main.java contains an information leak (from bob to alice). After Co-Inflow compilation, run the Main.java file with Co-Inflow runtime will display an exception. (It may be easy to create an Eclipse project for the output files produced by compilation, and add Co-Inflow project in its build path.)

IFSPEC

The core suite of the IFSPEC benchmarks (paper and download). It is a subset of the original benchmark suite: we delete the cases that Co-Inflow cannot correctly handle, e.g., reflections.

IFSpec_harness

This provides a program, IFSpecCompilation.java, that automatically compiles the IFSpec benchmark suites into Co-Inflow versions.

Usage

In the IFSpecCompilation program, specify the location of the IFSPEC folder, and the destination folder of the compiled Co-Inflow programs. Then run IFSpecCompilation to process the whole folder.

Compilation

The original benchmarks will be compiled into different packages named with the benchmark' names, i.e., a new package will be produced for each benchmark suite. Originial benchmarks specify source and sink channels in their corresponding rifl.xml files. The compilation process will read these files and insert label checks accordingly in the Co-Inflow versions.

Running the Co-Inflow version

A RunSample.java file will be created in every package. Running this program will (a) create a lattice specifed by the rifl.xml file, and (2) run the Co-Inflow version with the lattice.