Uniting Bounded Verification and Transformer-Based Learning for Proactive IoT Security

The proliferation of Internet-of-Things (IoT) ecosystems has introduced sophisticated interaction threats that emerge from unintended coordination between multiple applications, evading traditional single-app analysis. While formal verification provides soundness guarantees for interaction threats detection, it suffers from scalability limitations when analyzing large-scale deployments with hundreds of interacting applications. We present VeriWeave, a framework that synergistically combines bounded exhaustive formal verification, automated dynamic validation, and specialized transformer-based machine learning to detect interaction threats across application boundaries. VeriWeave employs static analysis to extract behavioral models from applications, uses bounded model checking to exhaustively enumerate potential interaction threat scenarios, at a static-derived scope obtained directly from the extracted models, and automatically validates these scenarios in instrumented environments to generate high-precision ground-truth labels. The validated results train specialized transformer models to predict exploitable interaction threats directly from code, achieving millisecond-scale predictions compared to several hours or days for formal analysis. Our evaluation on 3,732 real-world IoT applications together with a held-out benchmark of 4,000 additional applications (7,732 in total) demonstrates that VeriWeave reduces analysis time by 92% compared to pure formal methods while maintaining superior interaction threats detection accuracy. We validate cross-platform applicability on different ecosystems, confirming generalization. VeriWeave represents the first framework to bridge formal methods rigor with machine learning efficiency for interaction threats detection, enabling proactive vulnerability detection at scale through specialized models trained on validated interaction patterns.