A Data Security Formal Verification Framework for IoT Application Systems

This paper proposes a data security formal verification framework for IoT application systems, addressing security challenges in heterogeneous environments. The framework integrates static code analysis and runtime behavioral monitoring and implements dynamic data flow tracking enhanced by taint analysis via Aspect-Oriented Programming (AOP) and Java Agent mechanisms. By formalizing security requirements through data flow graph modeling via data behavior classifications, the framework establishes verifiable criteria for the detection of vulnerabilities and risks to data security. This research implements a prototype to demonstrate the methodology and verify the framework’s operational feasibility.