Grant: Strategic Projects Supplemental Competition

Information systems are prevalent in today's economy. Nowadays, they are intensively distributed and accessible over the Internet. To facilitate their construction, deployment, maintenance and improve their accessibility, they are now constructed as web services which may be invoked over the Internet from arbitrary locations. These information systems convey private, valuable information which must be only accessed by authorized personnel. Several domains like financial systems and patient records are subject to strict regulations like Sarbane-Oxley, HIPAAA, and PIPEDA. Security and privacy are addressed using several technology like authentication, encryption and secure communication protocols. We are targeting another aspect of security, which we call functional security. It describes the security rules that are at the business requirements level. For instance, the investment account of a customer should only be accessible to its broker and his manager; the health record of a patient should only be available to its treating doctor or limited information could be made available for a limited time period to consulting specialists. There are various levels at which functional security can be specified : data attributes, atomic services (actions) and business process (a complex ordering of atomic services). This project will: i) propose a specification method for functional security policies for web systems at these three levels; ii) define synthesis algorithms to automatically implement functional security policies into a security kernel, within the context of a service-oriented architecture. Functional security policies will be specified separately from functional requirements, in order to facilitate their maintenance and implementation. The security kernel implementing these policies will be separated from the implementation of the functional requirements, enabling online modification of security rules without having to modify the implementation of the services. Our approach is based on formal methods, enabling the use of formal verification techniques to ensure the consistency and adequacy of security policies.