Formal Methods for Verifying Authorization Policy in Microservice Systems
Connor Wojtak · 2025
In microservice systems, decentralized development can lead to inconsistent authorization policy implementations across services, potentially allowing users to perform operations they should not be authorized to or blocking legitimate operations. Detecting such inconsistencies requires complex, distributed analysis. We introduce an automated methodology that applies formal methods on microservice system source code for detecting and fixing these errors, reducing developer burden. A prototype implementation shows promising accuracy when applied on a popular, mid-sized microservice system benchmark.