CIISE Distinguished Seminar: Formal and Automatic Enforcement of Security Policies

Dr. Mohamed Mejri,
Laval University

Date: Sept. 27 (4 pm)
Location: EV3.309

Abstract

Several techniques and tools have been developed in recent years to ensure that our information systems work without interruption while producing the expected results. Software testing and equipment duplication are among the most widely used techniques. However, without formal methods, nothing can be guaranteed and problems can arise at any time. In contrast, formal methods are not accessible to every programmer, including experienced ones, and their use remains subtle and complex even for specialists. In fact, the proof of a few lines of code may contain many pages that are difficult to read and understand. In the other side, the use of formal methods is no longer an option, particularly for our critical systems when the consequences of their bad behaviors can be disastrous. To reduce the complexity of developing correct systems and maintaining them, it is helpful to have approaches allowing to separate the different aspects of a system (security, real-time, error handling, etc.), to study and develop each of them separately and then they combine them correctly to get the final system. This talk aims to show how the use of aspect-oriented paradigm combined with the use of formal methods is a promising direction to automatically produce secure systems.

Biography

Mohamed Mejri received his Ph.D. on the specification and analysis of cryptographic protocols from Computer Science and Software Engineering Department of Laval University, Canada.
Currently he is a Full Professor in Computer Science and Software Engineering Department of Laval University, Canada. Her research topics cover computer security, formal methods and software engineering.