MBIPV: a model-based approach for identifying privacy violations from software requirements

Nowadays, large-scale software systems in many domains, such as smart cities, involve multiple parties whose privacy policies may conflict with each other, and thus, data privacy violations may arise even without users being aware of it. In this context, identifying data security requirements and detecting potential privacy violations are crucial. In the area of model-based security requirements analysis, numerous research efforts have been done. However, few existing studies support automatic privacy violation identification from software requirements. To fill this gap, this paper presents MBIPV, a Model-Based approach for Identifying Privacy Violations from software requirements. First, this paper identifies six types of privacy violations in software requirements. Second, the MBIPV profile is proposed to support modeling software requirements using UML. Third, the MBIPV prototype tool is developed to generate formal models and corresponding privacy properties automatically. Then, the privacy properties are automatically verified by model checking. We evaluated the MBIPV method through case studies of four representative software systems from different domains: smart health, smart transportation, smart home, and e-commerce. The results show that MBIPV has high accuracy and efficiency in identifying the privacy violations from the software requirements. To the best of our knowledge, MBIPV is the first model-based approach that supports the automatic verification of privacy properties of UML software requirement models. The source code of the MBIPV tool and the experimental data are available online at https://github.com/YETONG1219/MBIPV.