Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems

• URL: http://arxiv.org/abs/2509.02860v1
• Date: Tue, 02 Sep 2025 22:11:46 GMT
• Title: Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems
• Authors: Connor Wojtak, Darek Gajewski, Tomas Cerny,
• Abstract summary: Microservice systems are becoming increasingly adopted due to their scalability, decentralized development, and support for continuous integration and delivery.<n>We propose a novel methodology that statically reconstructs microservice source code into a formal system model.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Microservice systems are becoming increasingly adopted due to their scalability, decentralized development, and support for continuous integration and delivery (CI/CD). However, this decentralized development by separate teams and continuous evolution can introduce miscommunication and incompatible implementations, undermining system maintainability and reliability across aspects from security policy to system architecture. We propose a novel methodology that statically reconstructs microservice source code into a formal system model. From this model, a Satisfiability Modulo Theories (SMT) constraint set can be derived, enabling formal verification. Our methodology is extensible, supporting software verification across multiple cross-cutting concerns. We focus on applying the methodology to verify the system architecture concern, presenting formal reasoning to validate the methodology's correctness and applicability for this concern. Additional concerns such as security policy implementation are considered. Future directions are established to extend and evaluate the methodology.

Related papers

• Extending the Formalism and Theoretical Foundations of Cryptography to AI [18.724847875398435]
  Recent progress in (Large) Language Models has enabled the development of autonomous LM-based agents.<n>One emerging direction to mitigate security risks is to constrain agent behaviours via access control and permissioning mechanisms.<n>We first systematize the landscape by constructing an attack taxonomy tailored to language models.<n>We then develop a formal treatment of agentic access control by defining an AIOracle algorithmically and introducing a security-game framework.
  arXiv  Detail & Related papers  (2026-03-03T04:11:21Z)
• A Comprehensive Survey on Benchmarks and Solutions in Software Engineering of LLM-Empowered Agentic System [56.40989626804489]
  This survey provides the first holistic analysis of Large Language Models-powered software engineering.<n>We review over 150 recent papers and propose a taxonomy along two key dimensions: (1) Solutions, categorized into prompt-based, fine-tuning-based, and agent-based paradigms, and (2) Benchmarks, including tasks such as code generation, translation, and repair.
  arXiv  Detail & Related papers  (2025-10-10T06:56:50Z)
• Bridging the Mobile Trust Gap: A Zero Trust Framework for Consumer-Facing Applications [51.56484100374058]
  This paper proposes an extended Zero Trust model designed for mobile applications operating in untrusted, user-controlled environments.<n>Using a design science methodology, the study introduced a six-pillar framework that supports runtime enforcement of trust.<n>The proposed model offers a practical and standards-aligned approach to securing mobile applications beyond pre-deployment controls.
  arXiv  Detail & Related papers  (2025-08-20T18:42:36Z)
• Explainable AI Systems Must Be Contestable: Here's How to Make It Happen [2.5875936082584623]
  This paper presents the first rigorous formal definition of contestability in explainable AI.<n>We introduce a modular framework of by-design and post-hoc mechanisms spanning human-centered interfaces, technical processes, and organizational architectures.<n>Our work equips practitioners with the tools to embed genuine recourse and accountability into AI systems.
  arXiv  Detail & Related papers  (2025-06-02T13:32:05Z)
• Zero-Trust Foundation Models: A New Paradigm for Secure and Collaborative Artificial Intelligence for Internet of Things [61.43014629640404]
  Zero-Trust Foundation Models (ZTFMs) embed zero-trust security principles into the lifecycle of foundation models (FMs) for Internet of Things (IoT) systems.<n>ZTFMs can enable secure, privacy-preserving AI across distributed, heterogeneous, and potentially adversarial IoT environments.
  arXiv  Detail & Related papers  (2025-05-26T06:44:31Z)
• Vulnerability Detection: From Formal Verification to Large Language Models and Hybrid Approaches: A Comprehensive Overview [3.135279672650891]
  This paper focuses on state-of-the-art software testing and verification.<n>It focuses on three key approaches: classical formal methods, LLM-based analysis, and emerging hybrid techniques.<n>We analyze whether integrating formal rigor with LLM-driven insights can enhance the effectiveness and scalability of software verification.
  arXiv  Detail & Related papers  (2025-03-13T18:22:22Z)
• SoK: The Security-Safety Continuum of Multimodal Foundation Models through Information Flow and Game-Theoretic Defenses [58.93030774141753]
  Multimodal foundation models (MFMs) integrate diverse data modalities to support complex and wide-ranging tasks.<n>In this paper, we unify the concepts of safety and security in the context of MFMs by identifying critical threats that arise from both model behavior and system-level interactions.
  arXiv  Detail & Related papers  (2024-11-17T23:06:20Z)
• Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach [32.15663640443728]
  The integration of machine learning (ML) into cyber-physical systems (CPS) offers significant benefits. Existing verification and validation techniques are often inadequate for these new paradigms. We propose a roadmap to transition from foundational probabilistic testing to a more rigorous approach capable of delivering formal assurance.
  arXiv  Detail & Related papers  (2023-11-13T14:56:14Z)
• Formal Methods for Autonomous Systems [21.989467515686858]
  Formal methods have played a key role in establishing the correctness of safety-critical systems. Main building blocks of formal methods are models and specifications. We consider correct-by-construction synthesis under various formulations.
  arXiv  Detail & Related papers  (2023-11-02T14:18:43Z)
• A Domain-Agnostic Approach for Characterization of Lifelong Learning Systems [128.63953314853327]
  "Lifelong Learning" systems are capable of 1) Continuous Learning, 2) Transfer and Adaptation, and 3) Scalability. We show that this suite of metrics can inform the development of varied and complex Lifelong Learning systems.
  arXiv  Detail & Related papers  (2023-01-18T21:58:54Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• A Verification Framework for Certifying Learning-Based Safety-Critical Aviation Systems [6.168537302126847]
  We present a safety verification framework for design-time and run-time assurance of learning-based components in aviation systems. From the design-time assurance perspective, we propose offline mixed-fidelity verification tools that incorporate knowledge from different levels of granularity in simulated environments. From the run-time assurance perspective, we propose reachability- and statistics-based online monitoring and safety guards for a learning-based decision-making model.
  arXiv  Detail & Related papers  (2022-05-09T22:56:00Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.