CloudFORMAL is a prototype Scala tool to encode AWS CloudFormation Templates into Description Logic models. It maps the CFn Resource Specification files (from here) into Terminological Boxes, and the actual CFn Templates into Assertional Boxes, building a comprehensive model that is aware of the inter-connections among resources. Models are serialized in OWL2, using the OwlApi, and reasoned upon with the JFact inference engine. Expressivity of the models is that of the description logic ALCOIQ.

Samples of input infrastructures (actual templates found through GitHub advanced search) are in the Benchmarks folder. Their corresponding output models are in the BenchmarksOut folder. The *InfrastructureModel.owl files can be opened, navigated, and queried in Protégé. Models are automatically checked against common security best-practices, such as those recommended by tools like ScoutSuite and CloudConformity (re-implemented here). Reports of such checks are found in the _*Report.csv files.

To run the tool, Java and Maven are needed. To check if these are installed, run java -version and mvn -v on a terminal. If either one is not installed, try following the instructions here and/or here.

Once Java and Maven are working, run the install script with

source ./install.sh

The script will initialize the Maven project from pom.xml, compile it, and build an executable .jar. It will also create the volatile alias CloudFORMAL for the full command java -Xmx1G -jar target/ExecCloudFORMAL.jar. The alias is deleted when the terminal is closed (and won't work at all if the script is run without source).

Three main features are currently implemented:

A folder with all cfn specifications is available at src/main/resources/CloudFormationResourceSpecification (the latest version for N. Virginia region can be downloaded from here). To use this feature type one of the commands below.

CloudFORMAL -s src/main/resources/CloudFormationResourceSpecification/
CloudFORMAL -s pathToYourSpecFolder pathToYourSpecOutDir

The first argument is the input directory (the directory containing all the specification jsons), the second argument is the output directory. If not output directory is given, the default will be src/main/resources/terminology/resourcespecificationsOwl/.

The folder containing the sample inputs is Benchmarks. Each sample input folder must have a specific structure: parent folder > infrastructure folder > stackset folders > (template json files + descriptor files). Descriptor files are used to feed potential input parameters and pseudo-parameters to the template. See the Benchmarks folder for guidance. To run this feature type one of the following commands.

CloudFORMAL -m  Benchmarks/01_sqilup/
CloudFORMAL -m  Benchmarks/16_retailmenot/
CloudFORMAL -m  Benchmarks/04_stationeering/ pathToYourTemplateOutDir
CloudFORMAL -ma Benchmarks/
CloudFORMAL -ma Benchmarks/ pathToYourTemplateOutDir

The first three commands model one infrastructure at the time, the last two model all infrastructures under a given directory. If the output folder path is omitted, default will be BenchmarksOut. During this encoding, some terminology .owl models will be imported and saved in the final model directory.

Once the models have been created (e.g., in the BenchmarksOut directory), we can perform the reasoning. This step needs an *InfrastructureModel.owl file as input. To test, run one of the commands:

CloudFORMAL -r  BenchmarksOut/01_sqilup/01_sqilup_InfrastructureModel.owl
CloudFORMAL -ra BenchmarksOut/
CloudFORMAL -r  pathToYourTemplateOutDir/dirName/
CloudFORMAL -ra pathToYourTemplateOutDir/

The -r option reasons over one infrastructure, -ra reasons against all models in the given directory. Running this command will save a *Report.csv file in the corresponding output folder. This command doesn't need a second argument.