Grande Region Security and Reliability Day 2013

April 12, 2013 – University of Luxembourg

logo logo logo logo
8:40 – 9:10 Registration coffee
9:10 – 9:15 Opening
9:15 – 10:15 Session 1
Marwane El Kharbili, Qin Ma, Pierre Kelsen and Elke Pulvermueller
CoReL: Compliance Representation Language
Peter Y.A. Ryan
An Enhancement to Authenticated QKD protocols
Michael Backes, Fabian Bendun, Matteo Maffei and Esfandiar Mohammadi
A Computationally Sound, Symbolic Abstraction for Malleable Zero-knowledge Proofs
10:15 – 10:25 Short break
10:25 – 11:25 Session 2
Ralf Küsters, Tomasz Truderung, Bernhard Beckert, Daniel Bruns, Jürgen Graf and Christoph Scheben
A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of Java Programs
Philippe De Ryck, Lieven Desmet, Frank Piessens and Wouter Joosen
Securing Web Applications with Browser Add-ons: an Experience Report
Dominique Schröder and Mark Simkin
Boosting Verifiable Data Streaming
11:25 – 11:50 Coffee break
11:50 – 12:35 Invited Lecture
Joost-Pieter Katoen
Towards Trustworthy Aerospace Systems using Formal Methods
Abstract:
Building modern aerospace systems is highly demanding. They should be extremely dependable. They must offer service without interruption for a very long time - typically years or decades. Whereas 'five nines' dependability, ie. a 99.999% availability, is satisfactory for most safety-critical systems, for on-board systems it is not. Faults are costly and may severely damage reputations. Dramatic examples such as Ariane 5 and Mars Pathfinder are known.

Rigorous design support and analysis techniques are called for. Bugs must be found as early as possible in the design process while performance and reliability guarantees need to be checked whenever possible. The effect of Fault Diagnosis, Isolation and Recovery (FDIR) measures must be quantifiable.

During the last five years, we have attempted to exploit concurrency theory and computer-aided verification to the engineering of aerospace systems. In this talk, we will present: - a general-purpose modeling formalism based on the AADL SAE standard - its formal semantics - sketch a rich palette of formal analysis and synthesis techniques - application to a satellite design at the European Space Agency.

12:35 – 14:15 Lunch at Porta Nova
14:15 – 15:15 Session 3
Oana Ciobotaru
Bridging Protocol Security and Game Theory
Tigran Avanesov, Yannick Chevalier, Michael Rusinowitch and Mathieu Turuani
Satisfiability of general intruder constraints - Application to distributed attacks
Michael Backes, Aniket Kate, Praveen Manoharan, Sebastian Meiser and Esfandiar Mohammadi
AnoA: A Framework For Analyzing Anonymous Communication Protocols
15:15 – 15:25 Short break
15:25 – 16:25 Session 4
Michael Backes, Dario Fiore and Esfandiar Mohammadi
Privacy-Preserving Accountable Computation
Naipeng Dong, Hugo Jonker and Jun Pang
Enforcing Privacy in the Presence of Others: Notions, Formalisations and Relations
Michael Backes, Jeremy Clark, Peter Druschel, Aniket Kate and Milivoj Simeonovski
Introducing Accountability to Onion Routing
16:25 – 16:45 Coffee break
16:45 – 17:45 Session 5
Ana Ferreira, Rosario Giustolisi, Jean-Louis Huynen and Gabriele Lenzini
On Tools for Socio-Technical Security Analysis
Tigran Avanesov, Yannick Chevalier, Michael Rusinowitch and Mathieu Turuani
Towards the orchestration of secured services under non-disclosure policies
Tim Muller
Quantifying information content of recommendations
17:45 – 17:55 Closing