Auditorium (IMAG)
7 November 2016 - 14h00
Information Flow Security in Component Based Models: From Verification to Implementation (Phd Defense)
by Najah BEN SAID from Verimag, Grenoble Alpes University
Abstract: Security verification and its distributed implementation are heavy processes in general, advanced security skills are required since both security configuration and coding distributed systems are complex and error-prone. With the diverse security attacks leaded by the Internet advent, how can we be sure that distributed systems that we are building do satisfy the intended security property?
In this thesis, we propose a model-based design flow that ensures the non-interference property in an application software from its high-level model leading to decentralized secure implementation. We present the secureBIP framework that is an extension for the component-based modelBIP with multy-party interactions for security. Non-interference is guaranteed using two practical manners: (1) we annotate the entire variables and ports of the model and then according to a defined set of sufficient syntactic constraints we check the satisfaction of the property, (2) we partially annotate the model way and then by extracting its compositional dependency graphs we apply a synthesis algorithm that computes the less restrictive secure configuration of the model if it exists.
Once the information flow security is established on an high-level model of the system, we follow a practical automated method to build a secure distributed implementation. A set of transformations are applied on the abstract model to progressively transform it into low-level distributed models and finally to distributed implementation, while preserving information flow security. Model transformations replace high-level coordination using multiparty interactions by protocols using asynchronous Send/Receive message-passing. The distributed implementation is therefore proven ”secure-by-construction” that is, the final code conforms to the desired security policy. To show the usability of our method, we apply and experiment it on real case studies and examples from distinct application domains.
Prof. SADDEK BENSALEM - Directeur de these
Prof. AXEL LEGAY - Rapporteur
Prof. GILLES BARTHE - Rapporteur
Prof. JEAN-LOUIS LANET - Examinateur
Prof. CATALIN DIMA - Examinateur
Prof MARIE-LAURE POTET - Examinateur
Dr. MARIUS BOZGA - Co-directeur
Dr. ABDELLATIF TAKOUA - Co-encadreur
