Automata-Enforced Dynamic Constraint Proofs: Blockchain-Based Verifiable Security for Cloud Data Management

This paper introduced a constraint-theoretic framework that reframes cloud data security as a verifiable, automaton-governed transition system rather than a static policy-checking problem. By modeling each data operation as a transition in a register automaton with data dependencies, encoding non-deterministic choices as existential witnesses, and enforcing mutable-state integrity through evidenced frames and linear realisability, the framework produces polynomial-size certificates for accepted operation traces. Compiling these certificates into recursive zero-knowledge proofs enables succinct on-chain verification against committed state, ensuring that dynamic, history-dependent policies are enforced without exposing data or predicates. The substitution morphism preserves conventional security semantics, allowing existing storage, processing, and audit layers to integrate without architectural disruption. Experimental results demonstrate that the approach remains practical on permissioned blockchains, with verification time and proof size comparable to incrementally verifiable computation baselines while additionally detecting replay and state duplication that those baselines accept. The ablation study confirms that evidenced frames, linear realisability, and the dependency relation each address distinct attack classes, and that their combination is necessary for comprehensive dynamic-state protection. The framework thus shifts cloud data security from a trust-based model to a trustless, verifiable paradigm, offering a principled foundation for multi-tenant environments where dynamic delegation and resource-sensitive evidence handling are essential. Future work will extend the predicate language to bounded aggregates, mechanize the semantic preservation proof, and validate the approach on production cloud workloads.

1.       K. Grolinger, W. Higashino, A. Tiwari, et al., “Data management in cloud environments: NoSQL and NewSQL data stores,” Journal of Cloud Computing: Advances, Systems and Applications, 2013. 2.       L. Zhu, Y. Wu, K. Gai, and K. Choo, “Controllable and trustworthy blockchain-based cloud data management,” Future generation computer systems, 2019. 3.       P. Wei, D. Wang, Y. Zhao, S. Tyagi, et al., “Blockchain data-based cloud data integrity protection mechanism,” Future Generation Computer Systems, 2020. 4.       M. Isberner, F. Howar, and B. Steffen, “Learning register automata: From languages to program structures,” Machine Learning, 2014. 5.       R. Baldoni, E. Coppa, D. D’elia, C. Demetrescu, et al., “A survey of symbolic execution techniques,” ACM Computing Surveys, 2018. 6.       M. Sørensen and P. Urzyczyn, “Lectures on the curry-howard isomorphism,” books.google.com, 2006. 7.       T. Chen, H. Lu, T. Kunpittaya, and A. Luo, “A review of zk-snarks,” arXiv preprint arXiv:2202.06877, 2022. 8.       M. Bellés-Muñoz, M. Isabel, et al., “Circom: A circuit description language for building zero-knowledge applications,” in IEEE international symposium on dependable, autonomic and secure computing, 2022. 9.       P. Valiant, “Incrementally verifiable computation or proofs of knowledge imply time/space efficiency,” in Theory of cryptography conference, 2008. 10.    E. Hildenbrandt, M. Saxena, N. Rodrigues, et al., “Kevm: A complete formal semantics of the ethereum virtual machine,” in 2018 IEEE 31st computer security foundations symposium (CSF), 2018.