A formal approach to derive an aspect oriented programming-based implementation of a secure access control filter

Context: Nowadays, Information Systems (IS) are at the heart of most companies and constitute then a critical element that needs an adequate attention regarding security issues of sensitive data it manages. Objective: This paper presents a formal approach for the development of a filter to secure access to sensitive resources of information systems. Method: The proposed approach consists of three complementary steps. Designers start by modeling the functionalities of the system and its security requirements using dedicated UML diagrams. These diagrams are then automatically translated into a formal B specification suitable not only for reasoning about data integrity checking but also for the derivation of a trustworthy implementation. Indeed, a formal refinement process is applied on the generated B specification to obtain a relational-like B implementation which is then translated into an AspectJ implementation, connected to a SQL Server (release 2014) relational database system. Such a generation is performed following the aspect oriented programming paradigm which permits a separation of concerns by making a clear distinction between functional and security aspects. Results: A systematic formal approach to derive a secure filter that regulates access to the sensitive data of an information system. The filter considers both static and dynamic access rules. A tool that supports the proposed approach is also provided. Conclusion: The approach has been applied on several case studies that demonstrate that the development of a tool permits to free the developers from tedious and error-prone tasks since they have just to push a button to generate the AspectJ code of an application.