Information on the Program

General Info   Program   Application & Registration   Venue   Hotel   Social Event   Slides   Videos

Schedule

Titles and Abstracts

Prof. Jean-Claude Bajard: Useful Arithmetic for Cryptography

Most of the asymetric cryptographic protocols are based on mathematical objects defined on finite fields (or finite rings). 
We present an overview of different representations and algorithms for fundamental operations like the modular multiplication.
Some of them are particularly dedicated to hardware and embedded systems.
 

Prof. Gilles Barthe and Prof. Yassine Lakhnech: Computer-Aided Cryptographic Design and Analysis

Computer-aided cryptography aims to develop tools that support the design, analysis, and secure implementation of cryptographic constructions.  In this presentation, I will give an overview of EasyCrypt (www.easycrypt.info), an interactive framework for building and verifying cryptographic proofs. I will outline its design principles, and then introduce the relational program verification technique which it uses to capture common patterns of reasoning in provable security. Finally, I will report on some recent developments to extend EasyCrypt to reason about cryptographic implementations in C, and to connect with the CompCert verified compiler to generate provably secure assembly code for cryptographic algorithms.

Prof. Manfred Broy: Model Based Software and Systems Engineering: Elements of Seamless Development

The tutorial outlines a comprehensive integrated approach to the structured modeling, specification, design and implementation of discrete systems that offer a variety of functions for different purposes and use cases and that are implemented by a network of distributed components operating concurrently partly in a real time mode. It introduces a theory and first concepts of an engineering methodology for the structured modeling in terms of formal specification, design and model-based implementation by state machines. The key is the integration of the three views: interface, architecture, and state view and their seamless integrated usage in model based system development comprising functional specification, architecture design, and implementation. For functional specification, a context model and a function hierarchy describe the functionality of multifunctional systems in a structured way. Modes help to specify feature interactions and functional dependencies between functions. Logical component architectures serve for the hierarchical design of systems. Networks of sub-systems called components describe architectures. The behavior of the components as part of the architecture is captured by interface specifications. State machines provide implementations. The approach is based on the FOCUS theory for modeling interface behavior and system functionality.

Prof. Olivier Coutelou: Sensor Networks for industrial usage

Wireless sensors and sensor network becomes more and more important for Schneider Electric. After a short presentation of ZigBee Green Power, two examples will be described:

• Energy Monitoring of Machines in industrial factories.
•  Energy and Electrical measurements dedicated to MV/LV substation in a Smart Grid environment.

At the end of the presentation, two real demos will be done:

• One to show simple self powered sensors allowing energy estimation.
• The other to demonstrate the capability of more complex sensors which are wirelessly synchronized in order to allow accurate electrical measurements.

Prof. Alexandre David and Prof. Kim Larsen: Symbolic and Statistical Model-Checking in UPPAAL.

In these two talks we will cover the theory of timed automata, our fundamental modeling language underlying the verification tool UPPAAL.  Also, a number of extensions of this formalisms will be presented including timed games, priced timed automata and games, energy automata games, stochastic extensions of these as well as the most recently very expressive formalism of stochastic hybrid automata, which is particularly well-suited for modeling cyber-physical systems.  We will review a number of associated decision problems related to model-checking, refinement checking and optimal scheduling and synthesis for these models that are highly relevant for cyber-physical systems.

The lectures will also emphasize the substantial research effort in the design of algorithms and datastructures for efficient analysis of timed automata and its extensions as to be found in the verification tool UPPAAL and its various branches.  Also, substantial focus will be on the most recent statistical model checking engine of UPPAAL, where properties are settled up to user-specified level of confidence based on randomly generated simulation runs.

The lectures will include ample demonstration of UPPAAL and it extensions, in particular UPPAAL SMC, as well as applications to a range of real-time and cyber-physical examples including schedulability and performance evaluation of mixed criticality systems, modeling and analysis of biological systems, energy-aware wireless sensor networks, smart grid and energy aware buildings and battery scheduling.

Dr. Julien Francq: Hardware Trojans: Taxonomy and Detection Methods

Nowadays, for financial reasons, most of the Integrated Circuits (ICs) are designed, manufactured and tested in foreign countries. It is thus difficult to secure all the IC design flow: nothing can prevent from the insertion of any malicious and deliberate change to the IC (also called Hardware Trojans, HTs) that may cause unwanted effects and potentially damages in many sensitive applications (avionics, space, military devices, communication, industry, nuclear plants, etc.).

This presentation proposes first to show a taxonomy of the different HTs of the literature. We will see that this bestiary is very big. Then, we will detail the detection methods of the state-of-the-art with their limitations.

Destructive HT detection methods mainly consist in reverse-engineering ICs before deployment, which is very costly and does not guarantee 100% detection rate. Moreover, non-destructive HT detection methods (logic test, side-channel analysis, etc.) have also to face challenges (process variation noise, measurement noise, low controllability and observability of nodes, etc.). Finally, the speaker will show the French funded R&D project HOMERE (Hardware Trojans: Threats and Robustness of Integrated Circuits), which will try to progress beyond the state-of-the-art.

Dr. David Lesens: Modelling in an industrial context

Model Driven Engineering is the topic of numerous theoretical research projects. But what about its real use in the industry? The objective of this talk is to provide some elements of answer for the space domain. Several topics will be addressed:

• Objectives of modelling,
• Expected benefits / risks,
• Perimeter of modelling (system, software, hardware, mechanical...),
• Needs of guidelines,
• Training of development teams,
• Language's semantics,
• Automatic code generation.

These topics will be supported by feedbacks from operational uses. 

Prof. Peter Marwedel: Efficient Computing in Cyber-Physical Systems

Computing in cyber-physical systems has to reflect the context of the computations and, hence, has to be efficient in terms of a number of objectives. In particular, computing has to be (worst and average case) execution-time and energy efficient, while also being reliable. In this talk, we will consider optimization techniques targeting worst-case execution time (WCET) and energy efficiency.

In the first part, we will consider real-time constraints and WCETs. We do this by integrating compilers and WCET estimation. We will demonstrate how such integration opens the door to WCET-reduction algorithms. For example, an algorithm for mapping frequently accessed memory objects to scratch pad memories (SPMs) is able to reduce the WCET for an automotive application by about 50%. The need to seriously consider WCETs and time constraints also has an impact on applicable error correction techniques. We will demonstrate our approach for a flexible error handling in the presence of real-time constraints possibly prohibiting time consuming error corrections.

In the talk, we will also address the energy consumption of computing in cyber-physical systems. We will explain how scratch pad memories can be used to reduce the energy consumption of such systems. Also, we will demonstrate that graphic processing units (GPUs) provide another way of saving energy. The talk will finish with some remarks on cyber-physical system education. 

Prof. Doron Peled: Components based systems with probabilities

In the design of reliable complicated systems, one can benefit from a high level formalism that is close enough to the specification, and, on the other hand, automatically and efficiently translatable into the physical layer. Component-based systems can represent a collection of units working together, with an emphasis on the interactions, choices and concurrency among their actions. Adding the ability of making probabilistic choices in component-based systems is nontrivial since each component has its own view, which is partial to the global view of the entire system; maintaining a global view would just eliminate the concurrency. A solution for that is to precede each probabilistic choice by a phase where the local view of a component is locked in order to prepare for such a decision. In this lecture, I would present the mathematical concepts related to concurrent probabilistic systems, based on Markov Decision Processes. Then, a solution based on concurrent artifacts such as independence and confusion will be given. A simple and elegant implementation of component-based systems with probabilistic choices, using semaphores, will be described.

Prof. Pavithra Prabhakar: Formal Verification of Cyber-Physical Systems

The ubiquitous deployment of cyber-physical systems in safety critical applications such as aeronautics, automotive, medical devices, industrial process control and others, has pressurized the need for the development of automated analysis methods to aid the design of high-confidence systems. The lecture will focus on the application of formal methods for the verification of cyber-physical systems.

The focus of the lecture will be on the interaction of the discrete and the continuous dynamics exhibited by cyber-physical systems due to the interaction between a network of embedded processors and a physical world. Systems exhibiting mixed discrete-continuous behaviors are popularly referred to as hybrid systems. An overview of the state-of-the-art in hybrid systems verification will be provided. This will include an introduction to:

(1) Formal models of hybrid systems.

(2) Safety and stability properties.

(3) Computational difficulty of the analysis.

(4) Approximation algorithms.

(5) Software tools.

Dr. Emmanuel Prouff: Side Channel Analysis Based on Linear Regression: From Paper to Silicium

Since the preliminary works of Kocher et al. in the nineties, studying and enforcing the resistance of cryptographic implementations against Side Channel Analysis (SCA) is became a dynamic and prolific area of embedded security. Stochastic attacks, introduced by Schindler et al. at CHES 2005, form one of the main families of SCA and they offer a valuable alternative to template attacks which are known to be among the most efficient ones. However, stochastic attacks, as long as template  attacks, have been initially designed for adversaries with a perfect copy of the target device in hand. Such a prerequisite makes them a pertinent tool when studying the implementations resistance against the most powerful adversaries, but it limits their pertinence as a cryptanalytic technique. Indeed, getting open access to a copy of the device under attack is difficult in practice and, even when possible, it remains difficult to exploit templates acquired on one device to attack another one. In light of this observation, several papers have been published to adapt stochastic attacks for contexts where the above prerequisite is no longer needed. They succeeded in defining practical attacks against unprotected implementations but no work was published until now to explain how stochastic attacks can be applied against secure implementations. The proposed presentation aims at dealing  with this issue. I will first show haw to extend the previous analyses of stochastic attacks to highlight their core foundations. Then, I will explain how they can be generalized to defeat first-order masking techniques, which are the main SCA countermeasures. Eventually, I will illustrate the interest of the new attack by a series of experiments on simulated and real electro-magnetic measurement traces.

Prof. Oleg Sokolsky: Challenges in Medical CPS

Modern techniques for treating patients are very dependent on medical devices.  Medical devices include sensors, which provide vital information about patient state; actuators that effect treatment; and decision support systems that help clinical personnel in planning the treatment.  Increasingly, devices used in treating a patient are interconnected, forming a patient-centric cyber-physical system (CPS).  Medical CPS hold out the promise of improved patient care with fewer opportunities for human error and decreased treatment costs.  In particular, medical CPS enable the development of physiologically closed-loop approaches that automatically deploy safety measures in response to changes in the patient's condition.  At the same time, deployment of such medical CPS presents a variety of challenges.  This lecture will discuss design, deployment, and regulatory challenges and suggest possible ways to overcome then, motivated by several on-going projects at the University of Pennsylvania.  We will start with safety considerations for individual devices, such as infusion pumps and pacemakers; explore the implications of interoperability in collections of medical devices used in a treatment of a patient; and finally consider some of the clinical applications that are enabled by interconnecting medical devices.

Prof. Martin Törngren: Integrating Viewpoints in the Development of CPS

The development of CPS involves multiple stakeholders which have different viewpoints and therefore use different concepts, models and tools to deal with their concerns of interest. Successful development requires that relations between viewpoints are addressed. This lecture identifies that such relations exist at three levels: people, models and tools. We present solutions that formally and explicitly capture these relations at each of these three levels. Interrelation contracts are used to define the vocabulary, assumptions and constraints required for ensuring smooth communication between stakeholders (people level). Dependency models capture relations between product properties belonging to different viewpoints, and how such dependencies relate to predictions and decisions (model level). Tool integration models describe the relations between tools in terms of traceability, data exchange, invocation and notifications (tool level). An industrial robot case study is utilized to illustrate the challenges and solutions with respect to relations between viewpoints. We also provide an unification approach discussing how these solutions complement and can be used to support each-other.

Prof. Jocelyne Troccaz: Medical CyberPhysical Systems in use: the example of Computer-Assisted Medical Interventions

Computer-Assisted Medical Intervention systems aim at providing assistance to clinicians for planning, simulating and executing safely, accurately and efficiently diagnostic or therapeutic actions. Such systems are based on a strong connection between digital data (patient images and signals, a priori information embedded in atlases, statistical models, biomechanical models, surgical protocols, etc.) and the real world where the clinician has to operate the patient. Collections of sensors may enable intra-operative data acquisition for refined decision making and action monitoring; actuators such as robots may be involved in the action itself with different levels of cooperation with a human operator. CAMI systems raise typical issues of CPS related to autonomy, security or dependability. In order to illustrate how these issues can be tackled in real applications, we will introduce the domain of CAMI and we will describe several examples from clinical end-user specifications to scientific and technological solutions we implemented. 

Prof. Thomas Watteyne: Standardizing the Internet of (Important) Things: IEEE802.15.4e Low-Power Mesh Technology and 6TSCH.

The Internet of Things revolution is at our doorstep and with it an epochal turnpoint in wireless network design. Major standardization bodies work on low-power wireless mesh networks, how they can operate reliably (WirelessHART, IEEE802.15.4e, IETF RPL) and how they integrate within the Internet (IETF 6LoWPAN, CoAP).
This talk will highlight the challenges faced by low-power wireless mesh networks, before showing how communication protocols and standards can address these.
Numerous use cases, examples and lessons learnt will be taken from open-source and commercial implementations, as well as from the recent work at the IETF 6TSCH group.

Alexandr Murahkin and Zubair Akhtar: Architecture modeling with variability and uncertainty

Traditional approaches of architectural modeling assume fully specified selection of components. We are currently exploring modeling with variability and uncertainty in the context of architecture modeling. The work involves creating the metamodel of AADL constructs in Clafer (a modeling language), and using that metamodel to create architectural models. The major advantage of this work is using the capabilities of Clafer on AADL models for expressing variability and uncertainty. Clafer Instance Generator & Optimizer will allow us to support design explorations of architectural models also in the presence of variability. Due to the limitations of Clafer, current challenges include tool scalability to support elaborate models, compilation time and complication in modelling of  some of the AADL constructs. Moreover, since Clafer does not support behavioral modelling, only the structural aspects of the an model are being considered for now.

Michele Lora: Modeling and Verification techniques for Cyber-Physical Systems design

The heterogeneity to Cyber-Physical Systems is nowadays tackled mainly by employing top-down approaches, often based on the concept of model-based design. Bottom-up approaches are limited to using cosimulation, which does not provide any formal assurance about the correctness of the integration.

In this talk UniverCM will be introduced. UniverCM is an automaton-based formalism that allows to model both analog and discrete behaviors, together with typical SW behaviors. The major advantage of this MoC is the possibility to map heterogenous systems into it and to represent them in a homogeneous environment allowing to easily integrate components coming from different domains. For these reasons, UniverCM is presented as the core representation used to develop a set of methodologies for highly heterogenous Cyber-Physical Systems design, by extending methodologies developed for homogeneous, purely digital, embedded systems.

Mengxuan Zhao: Supervisory controller for physical entities in Internet of Things and Smart Environments

New application domains of control, such as in the Internet of Things (IoT) and Smart Environments, require recourse generic control rules enabling the systematization and the automation of the controller synthesis. This work presents a generic architecture with supervisory controller as a service, as well as an automatic mechanism of synthesis of discrete controllers, in order to coordinate physical entities of various nature to respect generic control objectives in the Internet of Things and Smart Environments.