IoTrust Lab — University of Utah

Cyber-Physical Systems Security & Semantics

Semantics-driven hardening of legacy and modern CPS; symbolic recovery of logic; testbed-based security experimentation.

• SPHERE CPS Enclave: Reconfigurable Testbed for CPS • NSF Mid-Scale RI
• FMitF: Formal Verification & Implementation Stack for PLCs • NSF FMitF
• SMELL-CPS: Symbolic Math Expressions from Low-level Logic in Cyber-Physical Systems • DARPA

Digital Twins & Formal Verification

Formal and hybrid systems verification; fidelity-aware digital twins; verification-driven testbed design.

• SPHERE CPS Enclave: Reconfigurable Testbed for CPS • NSF Mid-Scale RI
• FMitF: Formal Verification & Implementation Stack for PLCs • NSF FMitF

IoT & Sensor Privacy

Privacy-preserving sensing and information flow for trustworthy ubiquitous systems, from edge to cloud.

Brain-Centered CPS / NeuroIoT

Human-in-the-loop CPS with neural & environmental sensing; multimodal fusion and memory-centric modeling.

• Neuroscience-in-the-Wild: Memory & Sensor Fusion • NIH
• NCS: Memory via Real-world Integration of Brain & IoT Perception • NSF NCS (NeurIoT)

Digital Twinning for Industrial Control Systems

This theme develops fidelity-aware digital twins that bridge engineered control code, physical process models, and experimental testbeds. Our work spans formal verification, real-system validation, and runtime conformance checking. We also leverage agentic testing frameworks for CPS that allow autonomous evaluation of system resilience, enabling verification and mitigation synthesis across realistic testbeds. Together, these efforts establish a principled foundation for trustworthy experimentation and security in cyber-physical infrastructure.

• SPHERE CPS Enclave: Reconfigurable Testbed for CPS • NSF Mid-Scale RI
• FMitF: Formal Verification & Implementation Stack for PLCs • NSF FMitF
• SMELL-CPS: Symbolic Math Expressions from Low-level Logic in Cyber-Physical Systems • DARPA