A Many-Sorted First-order Logic Theory generation for checking the necessity of authorization checks in enforcing Fine-Grained Access Control using SQL Security Injector.

The repository is structured as follows:

• config: the configuration (written in JSON) to run the Python script.
• dm2msfol: module handling model-to-text transformation from Data model to MSFOL theory.
• dmparser: module handling parsing Data model from JSON to Java objects.
• ocl2msfol: module handling model-to-text transformation from OCL expressions to MSFOL theory.
• oclparser: module handling parsing OCL expression from text to Java objects.
• output: the generated MSFOL theory folder.
  • header.smt2 the default header of the generated file.
  • theory.smt2 the generated file.
• result: the satisfiability result after solving the theory.
• scripts: the Python script to generate and solve the MSFOL theory.
• smparser: module handling parsing Security model from JSON to Java objects.
• solvers stores SMT solvers execution commands.
  • CVC4: the CVC4 solver.
  • CVC4fmf: the CVC4 solver, but using finite model finding mode.
  • Z3 : the Z3 solver.
• src a Java integration of the above modules.

• (required) Python 3.3 (or higher), can be downloaded from https://www.python.org/downloads/.
• (required) Maven 3 and Java 1.8 (or higher).

Note: to use any SMT solver, please create a corresponding folder with appropriate name in the parent folder solvers. Put your solver inside this created folder and create an solving.ini file, indicate how to run the solver.

• The data model and security model in JSON representation follows the definition in the thesis.
• Please store the models in the predefined folder, namely /src/main/resources.
• For example, consult a sample data model here and a sample security model here Note: Please remember to choose an entity as userClass.

• The configuration file is a JSON object contains the following fields:
  • DataModel: the filename of the data model in JSON, without the suffix.
  • SecurityModel: the filename of the security model in JSON, without the suffix.
  • Invariants: (optional) an array of OCL expressions, written as String.
  • Role: a role, as String.
  • Resource: a target resource to be act, either an attribute or an association.
  • Properties: (optional) an array of OCL expressions, written as String.
  • Solvers: an array of solvers, at the moment, we support CVC4 and Z3.
  • Timeout: (optional) a timeout value, as an integer.
• Please store the configuration in the /config folder.
• For example, consult a sample configuration here.

• Go to /script/run.py, change the content of line 15 to

CONFIG_FILENAME = '<config-file>.json'

where is the filename of the configuration you want to run.

• Run the script via command:

python run.py -bes

where -b is to build the Java project by Maven, -e is to execute the generation of MSFOL theory and -s is to solve the theory using solvers.

• The result is stored in the /results folder.