Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Connor Wojtak, Darek Gajewski, Tomas Cerny

TL;DR

The paper introduces an extensible methodology for application-layer formal verification in microservice systems by reverse-engineering code into a formal intermediate model and deriving SMT constraints for cross-cutting concerns, with a focus on architecture. It details a three-stage process (intermediate model, SMT constraint generation, and consistency verification) and formal proofs of constraint soundness for key architectural properties like no intra-service remote calls, bounded hub-like dependencies, and absence of cycles. The approach supports extensions to authorization and other concerns, and discusses extraction challenges and scalability considerations, including potential optimization strategies. The work aims to reduce governance burden, testing costs, and verification time in complex microservice deployments, while offering a rigorous foundation for future empirical evaluation and expansion to additional concerns.

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.

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

TL;DR

The paper introduces an extensible methodology for application-layer formal verification in microservice systems by reverse-engineering code into a formal intermediate model and deriving SMT constraints for cross-cutting concerns, with a focus on architecture. It details a three-stage process (intermediate model, SMT constraint generation, and consistency verification) and formal proofs of constraint soundness for key architectural properties like no intra-service remote calls, bounded hub-like dependencies, and absence of cycles. The approach supports extensions to authorization and other concerns, and discusses extraction challenges and scalability considerations, including potential optimization strategies. The work aims to reduce governance burden, testing costs, and verification time in complex microservice deployments, while offering a rigorous foundation for future empirical evaluation and expansion to additional concerns.

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.

Paper Structure

This paper contains 22 sections, 7 equations, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Background and Related Work
  3. Methodology
  4. Intermediate Model Encoding
  5. Model Definition
  6. Model Representation
  7. SMT Constraint Model Generation
  8. No Intraservice Remote Calls Constraint
  9. No Hub-like Dependencies Constraint
  10. No Cyclic Dependencies Constraint
  11. Constraints for Other Concerns
  12. Consistency Verification
  13. Formal Reasoning and Soundness
  14. Intermediate Model Soundness
  15. Extracting Model Information
  16. ...and 7 more sections

Figures (1)

  • Figure 1: An overview of the verification process, starting with the creation of an intermediate model from which various constraint sets can be generated. These sets form a constraint model that can be supplied to a solver to verify the microservice system.