Security Seminar at LORIA

Security Seminar at LORIA

If you want to receive annoucements for future seminars, feel free to subscribe to the mailing-list.
A link to an ical file is available, for your digital calendars.

Talks 2017 – 2018

Friday September 15 2017

David Basin (ETH Zurich)
Verified Secure Routing: The Verified Scion Project
Amphi C, 13:30
This talk is part of LORIA's colloquium series.

Tuesday November 21 2017

Jean-Louis Lanet (Inria Rennes)
How Secure Containers in a Secure Element are Secure?
A008, 13:30
Retrieving assets inside a secure element is a challenging task. The most attractive assets are the cryptographic keys stored into the Non Volatile Memory (NVM) area but also the algorithms executed. Thus, the condentiality of binary code embedded in that device in the Read Only Memory (ROM) must be protected. In some of the secure elements, a part of the instruction set is unknown and dynamically translated during the loading phase. We present a new approach for reversing a binary program when the Instruction Set Architecture (ISA) is partially unknown. Then, we discover many of the native functions that bypass several security checks accessing directly the resources leading to retrieve in plain text the assets. We demonstrate the ability to use them at the Java level to retrieve sensitive assets whatever the protections are like the firewall. Then, we suggest several possibilities to mitigate these attacks.

Tuesday December 5 2017

Deepak Garg (MPI Saarbrücken)
Robust and Compositional Verification of Object Capability Patterns
A008, 13:30
In scenarios such as web programming, where code is linked together from multiple sources, object capability patterns (OCPs) provide an essential safeguard, enabling programmers to protect the private state of their objects from corruption by unknown and untrusted code. However, the benefits of OCPs in terms of program verification have never been properly formalized. In this paper, we develop OCPL, the first program logic for compositionally specifying and verifying OCPs (in a language with closures and mutable state). The key idea of OCPL is to account for the interface between verified and untrusted code by adopting a well-known idea from the literature on security protocol verification, namely robust safety. Programs that export only properly wrapped values to their environment can be proven robustly safe, meaning that their untrusted environment cannot violate their internal invariants. We use OCPL to give the first general, compositional, and machine-checked specs for several commonly-used OCPs—including the dynamic sealing, membrane, and caretaker patterns—which can then be used to verify robust safety for client code.
© 2013 - 2017 Pierrick Gaudry, Marion Videau and Emmanuel Thomé ; XHTML 1.0 valide, CSS valide