Microservices architecture has transformed how large-scale applications are built and deployed, but ensuring their security remains a critical aspect. Testing methods, although useful, fail to provide a guarantee of microservices correctness. In contrast, model checking offers an exhaustive, formal verification technique capable of uncovering subtle security flaws. This paper introduces the importance of security in microservices, outlines the limitations of traditional testing, and demonstrates how model checking can address these shortcomings. We provide an overview of our structure, covering an introduction to the topic, an exploration of security properties, and a comparison of five model-checking tools across five security properties suited to microservice environments.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Formal Verification of Security Properties in Microservices: A Model Checking Approach

  • Khalid Meftah,
  • Ahmed El-Yahyaoui

摘要

Microservices architecture has transformed how large-scale applications are built and deployed, but ensuring their security remains a critical aspect. Testing methods, although useful, fail to provide a guarantee of microservices correctness. In contrast, model checking offers an exhaustive, formal verification technique capable of uncovering subtle security flaws. This paper introduces the importance of security in microservices, outlines the limitations of traditional testing, and demonstrates how model checking can address these shortcomings. We provide an overview of our structure, covering an introduction to the topic, an exploration of security properties, and a comparison of five model-checking tools across five security properties suited to microservice environments.