Formal Automated Verification of Microservices Tool (FAVM-T)

We used the TrainTicket repository found here: https://github.com/cloudhubs/train-ticket-aitest/tree/master. The master, first-inconsistency-injection, and second-inconsistency-injection branches contain the different scenarios tested.

We used a modified version of cimet-extract-lib (included in this package) to generate intermediate representations of the microservice system. The original version can be found here: https://github.com/cloudhubs/cimet.

We used the microservice indexer found here: https://github.com/arfan-rfn/microservice-index/tree/master to create indices of the microservice system.

Project Requirements

• Python and pip are required (confirmed working with Python 3.12.6).

Project Structure

• /cimet-extract-lib contains the code used to generate the intermediate representations.
• /data/aiat_auth_fault_injection contains all of the intermediate models used to complete the case study.
• /data/aiat_auth_fault_injection/models contains the generated system models that were used to generate constraints evaluated by the SMT solver.
• /data/aiat_auth_fault_injection/ms_indices contains indices of the microservice system.
• /data/aiat_auth_fault_injection/ms_irs contains the IRs of the microservice system.
• /data/aiat_auth_fault_injection/suggestions contains the detected faults when evaluated by the solver.
• /data/aiat_auth_fault_injection/AIAT Formal Methods Fault Injection Analysis.docx contains an analysis of all the results.
• /src contains the code used to generate intermediate models, generate constraints, and solve.
• /util contains various utility scripts.
• /validation contains the code used to trun the case study.

Running the Project

1. Run pip install -r requirements.txt to obtain the necessary requirements.
2. Run python -m validation.auth.aiat_fault_injection to run the fault injection study, which takes the provided IRs and indices (you can generate these yourself using the cimet-extract-lib and microservice indexer provided), creates SMT-friendly system models, runs the SMT solver on each model, and outputs the results to the /data/aiat_auth_fault_injection/ directories.