CRYSTAL mainly focuses on assessing the security aspects of Cyber-Physical Systems. In this project, we use Timed Rebeca and model checker Afra to specify and verify the behavior of CPS components against CPS-related attacks. We analyze architecture of CPS design to recognize where the potential attacks can successfully lead the system to security violation.
A model of attack is proposed for both attacks on CPS communication and components. Also, we utilize the STRIDE model (a model of threats is used at Microsoft for identifying computer security threats) as a reference for classifying the attacks. Currently, we are extending our work to analyze mitigation strategies against CPS-related attacks and also verifying security of the system using run-time verification.
Fereidoun Moradi, Sara Abbaspour Asadollah, Ali Sedaghatbaf, Aida Causevic, Marjan Sirjani, Carolyn Talcott: An Actor-based Approach for Security Analysis of Cyber-Physical Systems, FMICs, 2020 PDF
Fereidoun Moradi, Maryam Bagheri, Hanieh Rahmati, Hamed Yazdi, Sara Abbaspour Asadollah, Marjan Sirjani, Monitoring Cyber-Physical Systems using a Tiny Twin to Prevent Cyber-Attacks, 28th International Symposium on Model Checking of Software (SPIN), 2022 PDF