-
Notifications
You must be signed in to change notification settings - Fork 11
CorC for Information Flow
CorC for information flow is an extension of CorC. CorC is a tool for an refinement-based approach allowing to specify information flow policies first and to create programs which comply to these policies by construction.
To install the CorC tool, you can use the update site or install the plugins in this repository. Eclipse Modeling Tools in the version Neon or newer is required https://www.eclipse.org/downloads/eclipse-packages/.
- Check out the de.tu_bs.cs.isf.ccorc.tool.update plugin in the CCorC branch
- In Eclipse Help > Install new software > Add... > Local > Navigate to the update site
- Select all features and continue the installation
-
Check out all plugins in the CCorC branch
-
In de.tu-bs.cs.isf.cbc.model and in de.tu-bs.cs.isf.taxonomy.model
Open File cbcmodel.genmodel
Generate Model, Edit and Editor code -
Install dependencies manually:
In Eclipse Help > Install new software
Search and install Graphiti SDK Plus
In Eclipse Help > Eclipse Marketplace
Search and install JaMoPP
Search and install Eclipse Xtext
Visit https://www.key-project.org/download/ and follow the introductions to install KeY (KeY-Based Eclipse Projects) -
Create a second Eclipse Application configuration to use the editor
Instead of 3. the Installation with update site can be used, but only select the feature DependenciesFeature
New graphical editor files can be created by right clicking in the explorer New > Other > CorC > new CorC File > Next > CorC diagram and [name] and [path] > Finish
New textual editor files can be created by right clicking in the explorer New > Other > CorC > new CorC File > Next > CorC textual and [name] and [path] > Finish
The CorC functionality of the editor can be seen in the following screencasts:
In this video, a linear search algorithm is constructed and proven in the graphical editor
https://raw.githubusercontent.com/TUBS-ISF/CorC/master/Screencasts/GraphicalLinearSearch.mp4
If this is to long, a smaller example is shown here.
https://raw.githubusercontent.com/TUBS-ISF/CorC/master/Screencasts/GraphicalSimpleExample.mp4
To prove a program in the graphical editor, you have to right click the concrete statement, a repetition statement, or a selection statement and choose Verify > Verify.... The shown helper.key file has to be created manually to specify specific predicates. Instead of predicates, Java methods can also be used in specification and code in the editor. The Java class has to be in the src-folder of the project. https://raw.githubusercontent.com/TUBS-ISF/CorC/master/Screencasts/GraphicalProve.mp4
To use the information flow functionaly, you can create new secure variables by adding Variables and Variable from the palette, and using these variables in the program. For example, a private variables x can be introduced by writing private in the Confidentiality column.