VeriFlow: A Framework for the Static Verification of Web Application Access Control via Policy-Graph Consistency

The evolution of industrial automation toward Industry 3.0 and 4.0 has driven the emergence of Industrial Edge-Cloud Platforms, which increasingly depend on web interfaces for managing and monitoring critical operational technology. This convergence introduces significant security risks, particularly from Broken Access Control (BAC)—a vulnerability consistently ranked as the top web application risk by the Open Web Application Security Project (OWASP). BAC flaws in industrial contexts can lead not only to data breaches but also to disruptions of physical processes. To address this urgent need for robust web-layer defense, this paper presents VeriFlow, a static verification framework for access control in web applications. VeriFlow reformulates access control verification as a consistency problem between two core artifacts: (1) a Formal Access Control Policy (P), which declaratively defines intended permissions, and (2) a Navigational Graph, which models all user-driven UI state transitions. By annotating the graph with policy P, VeriFlow verifies a novel Path-Permission Safety property, ensuring that no sequence of legitimate UI interactions can lead a user from an authorized state to an unauthorized one. A key technical contribution is a static analysis method capable of extracting navigational graphs directly from the JavaScript bundles of Single-Page Applications (SPAs), circumventing the limitations of traditional dynamic crawlers. In empirical evaluations, VeriFlow outperformed baseline tools in vulnerability detection, demonstrating its potential to deliver strong security guarantees that are provable within its abstracted navigational model. By formally checking policy-graph consistency, it systematically addresses a class of vulnerabilities often missed by dynamic tools, though its effectiveness is subject to the model-reality gap inherent in static analysis.