Microservice architectures are inherently plagued by "authorization blindspots"–divergent security policies across independent services that create undetectable downstream security drifts. As systems evolve, these invisible vulnerabilities leave applications highly susceptible to privilege escalation and catastrophic data breaches. To eliminate these blindspots, we introduce a novel, fully automated framework that bridges the precision of formal static analysis with the adaptiveness of Generative AI. By extracting a policy-enriched Intermediate Representation of the microservice system, our approach deterministically guides GPT-5 to synthesize executable, downstream-aware policy test suites targeting specific policy inconsistencies. Evaluation on the Train-Ticket benchmark denotes that our method outperforms state-of-the-art tools such as EvoMaster and EvoSuite by generating 100% semantically valid authorization policy tests. Further, this research provides vital empirical validation for formal methods. By producing 97.4% error-free drift validation tests, our approach systematically neutralizes static analysis noise. Ultimately, these results establish a rigorous, highly effective pathway for hybridizing formal structures with Large Language Models to definitively verify complex, distributed authorization policies.
Md Arfan Uddin, Shakthi Weerasinghe, Connor Wojtak et al.· International Symposium on S...· 0 citations
Microservice-based systems evolve continuously through API changes, service splits and merges, dependency churn, and deployment-topology drift driven by DevOps practices. This rapid evolution erodes the assumptions encoded in formal models, test suites, and architectural descriptions, leaving practitioners with limited guidance on how to keep verification artifacts aligned with evolving implementations. Prior surveys cover microservices design, deployment, performance, and isolated verification techniques, but, to our knowledge, none consolidate the intersection of evolution and formal/rigorous verification, nor map how repository-derived signals and CI/CD pipelines support continuous verification of microservice-based systems. This paper addresses that gap through a systematic literature review (SLR). Following the Kitchenham et al. guidelines and PRISMA-style reporting, we defined a review protocol with four research questions covering (i) formal modeling and verification approaches, (ii) the impact of architectural and API evolution on verifiability, (iii) repository-derived signals for updating formal artifacts, and (iv) continuous and incremental verification in CI/CD pipelines. Structured searches in IEEE Xplore, ACM Digital Library, SpringerLink, and Scopus returned 1187 records, which were screened in seven stages and reduced to 18 included studies (13 primary studies that supply evidence and five background studies retained for transparency and framing) through inclusion/exclusion criteria and a weighted 15-item quality-assessment instrument. We synthesized the included studies thematically and compared them along five dimensions: verification technique, evolution dimension, automation level, empirical evidence, and tool/artifact availability. The synthesis shows that actor-based model checking, TLA+ control-plane verification, static code analysis, continuous certification, and runtime/self-adaptive testing form five complementary clusters, but empirical evaluation is dominated by small academic case studies, only a minority of approaches automate model updates from repository signals, and few are integrated end-to-end into CI/CD. We discuss methodological limitations of the body of work, including a lack of industrial-scale validation and shared datasets, contrast intrinsic (build-time, model-driven) and extrinsic (recovery-based) verification strategies, and outline a research agenda toward repository-aware, pipeline-integrated verification for evolving microservices. The present synthesis distils a set of immediate, evidence-based actions for practitioners together with a focused agenda of open research challenges.
R. Gómez, Ebeid Elsayed, Enrique R. Zarate et al.· Software· 0 citations