Formal Verification of Security Properties in Microservices: A Model Checking Approach
摘要
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.