Dans l'enseignement supérieur, les diaporamas sont abondamment utilisés pour faciliter la transmission de connaissances de l'enseignant vers les étudiants dans les cours magistraux. Dans ce contexte, les opportunités d'interactions avec l'enseignant (et entre étudiants) restent assez limitées et on assiste depuis plusieurs années à une augmentation croissante du nombre d'étudiants qui apportent en cours leur ordinateur portable, tablette ou Smartphone. Face aux nombreuses sources de distraction offertes par la présence de ces technologies, il apparaît aujourd’hui nécessaire de trouver des solutions pour les utiliser en créant de l’interactivité au service des apprentissages. En s’appuyant sur les pratiques pédagogiques habituelles des enseignants, comme celles qui consistent à transmettre des connaissances à partir de diaporamas, nous verrons comment créer de l’interactivité dans un cours magistral en offrant aux étudiants des opportunités d'interaction.
Key Escrow free Identity-based Cryptosystem.
Over the years, several identity-based cryptosystems using bilinear pairings have been proposed. Many schemes, based on bilinear pairings, suffer from key escrow problems and require a secure channel for private key issuance. In this talk, we will discuss on a binding-blinding technique, which can be used for solving the problem of key escrow in identity-based cryptosystem and can help in eliminating the requirement of secure channel for the private key issuance.
Efficient Formally Secure Compilers to a Tagged Architecture.
Severe low-level vulnerabilities abound in today's computer systems, allowing cyber-attackers to remotely gain full control. This happens in big part because our programming languages, compilers, and architectures were designed in an era of scarce hardware resources and too often trade off security for efficiency. The semantics of mainstream low-level languages like C is inherently insecure, and even for safer languages, establishing security with respect to a high-level semantics does not guarantee the absence of low-level attacks. Secure compilation using the coarse-grained protection mechanisms provided by mainstream hardware architectures would be too inefficient for most practical scenarios.
This talk will present a new 5 year project aimed at leveraging emerging hardware capabilities for fine-grained protection to build the first, efficient secure compilers for realistic low-level programming languages (the C language, and Low* a safe subset of C embedded in F* for verification). These compilers will provide a secure semantics for all programs and will ensure that high-level abstractions cannot be violated even when interacting with untrusted low-level code. To achieve this level of security without sacrificing efficiency, our secure compilers target a tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules. We hope to experimentally evaluate and carefully optimize the efficiency of our secure compilers on realistic workloads and standard benchmark suites. We are also using use property-based testing and formal verification to provide high confidence that our compilers are indeed secure. Formally, we are constructing machine-checked proofs of fully abstract compilation and of a new property we call robust compilation, which implies the preservation of safety properties even against an adversarial context. These strong properties complement compiler correctness and ensure that no machine-code attacker can do more harm to securely compiled components than a component already could with respect to a secure source-level semantics
Complexity of automatic verification of cryptographic protocols
Many security properties are naturally expressed in terms of indistinguishability.
In symbolic protocol models the notion of indistinguishability can be expressed as trace equivalence in a cryptographic process calculus. Current automated verification tools are however limited even for a bounded number of sessions: they are either restricted to support only a particular set of cryptographic primitives, do not allow for protocols with else branches, or can only approximate trace equivalence, allowing for false attacks. Moreover, the complexity of these algorithms has never been studied.
In this work, we study the complexity of deciding equivalence properties, for several classes of protocols and several equivalences.