PLC-Defuser

This repository contains the code and the dataset for the paper "PLC-Defuser: Detecting Hidden Ladder Logic Bombs in PLCs via Control Flow Graph and Model Checking".

Datasets

Currently, we developed three datasets of PLC logic controlling the following physical processes:

• Tennessee Eastman Process (GRFICS)
• Secure Water Treatment Plant (SWAT)
• Water Tank (Water_tank)

Code

Our work code is located in the project folder, which contains the following folders:

• malicious: it contains the formal model of the SWAT program, which includes a logic bomb
• legitimate: it contains the formal model of the original SWAT program, which doesn't include a logic bomb
• intrepyd: it contains the intrepyd libraries (https://github.com/formalmethods/intrepid)
• utils: it contains the scripts that check the model meets our paper's requirements

How to verify requirements of the SWAT program

git clone https://github.com/UniboSecurityResearch/PLC_Defuser.git
cd PLC_Defuser/project
docker build -t plc-defuser .
docker run plc-defuser

N.B. Docker checks the requirements of the malicious program by default. To check the requirements of the legitimate program, change the program to be executed in the Dockerfile: malicious/check_requirements.py to legitimate/check_requirements.py

Cite us

If you find this work interesting and use it in your academic research, please cite our paper!