Section: Overall Objectives

Highlights of the Year

As highlights of the year, we wish to mention four best paper awards.

Mounir Assaf PhD thesis focusses on the verification of security properties in C programs. While investigating the domain, Mounir Assaf has created a static analysis for programs written in an imperative language with pointer aliases whose objective is to verify a property called Terminating-Insensitive Non Interference (TINI). Briefly speaking, this property guarantees that the content of secret variables of a program do not leak into public ones. Hence, this property is of paramount importance for the security of some critical software components. This work has conducted to the publication of two articles. The first one appeared in (IFIP SEC 2013, a renowned international conference in the domain of security), while the second one has been published in [45] (SAR-SSI 2013), a national conference dedicated to the spreading of work in progress to the French speaking security community. Both papers received the best paper award.

Stephane Geller has proposed a language (namely BSPL) for specifying and composing information flow policies. Such policies detail how a piece of data owned by an application is allowed to disseminate in an operating system. Thomas Saliou, Radoniaina Andriatsimandefitra and Valerie Viet Triem Tong have experimented the relevance of this language. They have proposed a semi-automatic way to compute such policies. They have also show that when such policies are enforced it is possible to detect if an application is infected by a malware. This work has led to the publication of an article in an international conference of the security domain . This article received the best student paper award of the conference.

In , we propose an inference attack called the de-anonymization attack, by which an adversary tries to infer the identity of a particular individual behind a set of mobility traces. The implementation of this attack is based on a mobility model called Mobility Markov Chain (MMC), which is built out from the mobility traces observed during the training phase and is used to perform the attack during the testing phase. Experiments led on real datasets demonstrate that the attack is both accurate and resilient to sanitization mechanisms such as downsampling. This paper has received the IEEE best student paper award at the conference TrustCom 2013.

Best Papers Awards :

[27] Program Transformation for Non-interference Verification on Programs with Pointers in SEC.

M. Assaf, J. Signoles, F. Tronel, E. Totel.



[25] Information Flow Policies vs Malware in IAS - Information assurance and security - 2013.

R. Andriatsimandefitra, T. Saliou, V. Viet Triem Tong.



[31] De-anonymization attack on geolocated datasets in The 12th IEEE International Conference on Trust, Security and Privacy in Computing and Communications (IEEE TrustCom-13).

S. Gambs, M.-O. Killijian, M. Nunez Del Prado Cortez.