This is the README of the PLIF (pl/sql information flow) analysis framework.

PLIF is developed in the Institute of Artificial Intelligence of MIREA - Russian Technological University. This software is a RESEARCH PROTOTYPE and comes with NO WARRANTY.

For further details see publications related to PLIF ./publications

In case you find BUGS, feel free to report them through the GitHub bug tracker.

PLIF is based on many researches in the field of software security formal models.

What is PLIF

PLIF is a framework that can be used for information flow control (IFC) in oracle database environment. It is based on temporal logic of actions and model checking technology. We put Paralocks policy language at the core of our project.

Paralocks/Paragon

Though direct data retrieval (updating) is possible it is assumed that critical parts of a database is accessed via pl/sql program units.

The overall analysis process includes the following stages:

1. Translation of PL/SQL code into TLA+ specifications with plsql2tla utility.
2. Democrating the specifications accordinally with existent global access control policy rules (RBAC). On this step we add security policies to literals, formal arguments, exceptions, local variables etc.
3. Replaying the model with TLC or other model checker.
4. Correcting the model and instrumenting the source code of PL/SQL program units (changing the global access control policy rules) in case of security invariant violation.

INSTALLATION

The instrumental basis of the framework includes TLA+ toolbox, plsql2tla and plifparser utilities. The ideas for plsql2tla design were benefited from c2tla. plif_parser is in fact a customization of tla+ trace explorer.

INSTALLING TLA+ toolbox

To install TLA+ toolbox see [Tla+ toolbox]

INSTALLING plsql2tla

Copy plsql2tla folder to some location on your hard drive.

INSTALLING plifparser

Copy plifparser folder to some location on your hard drive.

Quick Start

Being an initial prototype plif platform has a number of limitations regarding PLSQL grammar. plsql2tla as well as the whole project currently supports just a short list of Oracle PL/SQL a and SQL statements and expressions including: select, insert, update, assign, arithmetic operators, comparison operators, logical operators, if, while, null, throw exception, when xxx an and some others. For more details see plsql2tla

It is assumed that before begining analysis we have a set of PL/SQL program units implementing the critical part of business logic (see /publications/... ) and predefined rules of the general access control policy (typically role-based) represented as grant/revoke statements.

1. To generate an initial set of TLA+ specifications modeling parallel user sessions in database environment change the current directory to the home directory of plsql2tla and run java plsql2tla.jar ..... As result new .tla files will be added to ./plsqlspecs folder.

2. Markup required parameters, variables, exception etc with respect to the general access control policy i.e. {<<x,<<[t_expire |-> {NONE}], [guest |-> {NONE}, reviewer |-> {NONE}, manager |-> {x}, organizer |-> {NONE}]>> >>} which essentually means that an actor x can only read labeled data iff the lock manager is open in his session. For more details see /publications/...

3. Create a new TLC model and set values for nessecary constants (more details see /publications/...) .

Replay the model accordinally to the algo described in (/publications/...).

4. In case of ParalocksInv violation explore the error trace with plifparser. To run it choose trace-explorer.html in plifparser home directory.

Fix the model and apply source code instrumentation or change the global policy if needed (see /publications/...).