Towards Secure IoT Deployments: A DSL and Digital Twin-Based Emulation Platform for Security Verification
The Internet of Things (IoT) is revolutionizing industries from healthcare to manufacturing by enabling smarter automation and decision-making, with billions of connected devices already deployed. Securing these systems presents various challenges due to resource constraints, lack of standardized security protocols, complex testing requirements, and device heterogeneity. Formal verification uses rigorous methods to prove that a system or protocol satisfies certain security properties. Nevertheless, current formal verification tools require specialized expertise and cannot guarantee the correct implementation of verified security protocols, creating a gap between design-time verification and runtime security assurance. IoT emulation platforms could enable developers to deploy the IoT system and perform verification of the implemented security protocols before deploying it to the real world. However, existing emulation platforms lack the necessary capabilities to efficiently deploy and test security protocols for IoT systems. To address these challenges, we propose a comprehensive framework that verifies security requirements throughout the entire IoT system lifecycle. Our approach introduces: (1) a Domain Specific Language (DSL) that enables security protocol designers to model and verify protocols at design time without requiring expertise in multiple verification tools, automatically translating models to ProVerif and Tamarin; (2) a container-based emulation platform using Kubernetes orchestration that enables pre-deployment testing by emulating IoT hardware and deploying actual software; and (3) integration of the emulation platform into a Digital Twin framework for runtime verification and anomaly detection. This framework addresses the critical need for standardized methodologies that bridge formal verification and practical IoT security implementation, providing a comprehensive solution for ensuring security properties hold throughout the entire IoT system lifecycle.
Tue 7 OctDisplayed time zone: Eastern Time (US & Canada) change
10:30 - 12:00 | |||
10:30 22mTalk | Towards Secure IoT Deployments: A DSL and Digital Twin-Based Emulation Platform for Security Verification Doctoral Symposium Leonard Tudorache Eindhoven University of Technology | ||
10:52 22mTalk | LLM-Based Generation of Low-Code Development Platforms Doctoral Symposium Bernhard Schenkenfelder Software Competence Center Hagenberg (SCCH) | ||
11:15 22mTalk | A Model-Driven Approach for CI/CD Doctoral Symposium Hugo da Gião University of Porto & HASLab/INESC TEC | ||
11:37 22mTalk | Towards Efficient Offline Incremental Model-to-Text Transformations Doctoral Symposium Adam Blanchet University of York | ||
