Invited Speakers

Irina Mariuca Asavoae & Markus Roggenbach – Software Model Checking for Mobile Security – Collusion Detection in K

Abstract: Cyber-security witnesses an ongoing expansion in various fields of research. This is due to the booming of cyber-physical systems and the necessity of evaluating and certifying their sustainability more efficiently. For example, until now security industry leaders, such as Intel Security, focused on malware analysis of only single applications. However, due to the highly collaborative app environment proposed by Android, the security evaluation needs to have more complex settings. This tutorial aims to define this security problem and to show how model checking can solve and/or alleviate it. Namely, we first focus on describing collusion–the property of an apps group of working together for producing malware. Secondly, we evaluate the exposure degree of the Android environment to the collusion problem. Thirdly, we present our proposal of employing model checking for collusion evaluation and the related work in formal methods for Android security. Finally, we discuss our view for future challenges and perspectives of formal methods in cybersecurity. This work represents a part of the App Collusion Detection project.

Irina Mariuca Asavoae is a guest researcher at Swansea University where, in 2015, she started working on Android security in the ACID project. She received her PhD in 2012 from A.I. Cuza University in Romania for the thesis “K Semantics for Abstractions”–part of a project in collaboration with Grigore Rosu’s group in University of Illinois Urbana-Champaign. Her work evolves from formal methods in programming languages, with emphasis on model checking and abstract interpretation, to applying these techniques in cybersecurity. As such, her current projects are: Android security, timing evaluation of embedded systems, and synthesis of program analyzers from formal language semantics.

Klaus Havelund & Doron Peled – Efficient Runtime Verification of First-Order Temporal Properties

Abstract: Runtime verification allows monitoring the execution of a system against a temporal property, raising an alarm if the property is violated. In this paper we present a theory and system for runtime verification of a first-order past time linear temporal logic. The first-order nature of the logic allows a monitor to reason about events with data elements. While runtime verification of propositional temporal logic requires only a fixed amount of memory, the first-order variant has to deal with a number of data values potentially growing unbounded in the length of the execution trace. This requires special compactness considerations in order to allow checking very long executions. In previous work we presented an efficient use of BDDs for such first-order runtime verification, implemented in the tool DejaVu. We first summarize this previous work. Subsequently, we look at the new problem of dynamically identifying when data observed in the past are no longer needed, allowing to reclaim the data elements used to represent them. We also study the problem of adding relations over data values. Finally, we present parts of the implementation, including a new concept of user defined property macros.

Klaus Havelund is a Senior Research Scientist (SRS) in the Laboratory for Reliable Software (LaRS) at NASA’s Jet Propulsion Laboratory (JPL), Pasadena, California USA. JPL is a Federally funded research and development center (FFRDC), managed by California Institute of Technology (Caltech), with the primary function to construct and operate planetary robotic spacecraft. He has worked in the field of formal methods for over three decades, in areas covering formal specification languages, theorem proving application, model checking, and runtime verification. He has a Ph.D in Computer Science from the University of Copenhagen (DIKU) and Aalborg University, Denmark, largely performed at Ecole Normale Supérieure (ENS) in Paris.

Doron Peled is a professor at Bar Ilan university. He graduated from the Technion, Israel
Institute of Science. Previously, he was a researcher at Bell Labs, and a professor at university of Texas at Austin, and University of Warwick in England. Doron’s research is focused on formal methods: testing, verification and synthesis of correct-by-design systems. He wrote the book “Software Reliability Methods” and coauthored the book “Model Checking” with Ed Clarke and Orna Grumberg. Doron is a recipient of the CAV award 2014 for his contribution of the partial order reduction for model checking.

Radu Iosif – Program Verification with Separation Logic

Abstract: In this talk Radu Iosif will introduce Separation Logic as a framework for the development of modular program analyses for sequential, inter-procedural and concurrent programs. Because program verification eventually boils down to deciding logical queries such as the validity of verification conditions, the core of the talk is dedicated to a survey of decision procedures for Separation Logic, that stem from either SMT, proof theory or automata theory. Incidentally I will address issues related to decidability and computational complexity of such problems, in order to expose certain sources of intractability.

Radu Iosif is a full-time researcher in the French National Research Center (CNRS) at the Verimag laboratory, since 2002. Previously, he obtained a PhD in Computer Science from Politecnico di Torino, Italy, and spent time as a Research Associate at Kansas State University, USA. His main interests are in program verification, mainly in applications of logic and automata theory to finding scalable techniques that can cope with real-life software systems.

Rémi Delmas – Applying Formal methods to Advanced Embedded Controllers

Abstract: This talk presents a sample of research work conducted by the French Aerospace Lab (ONERA) on tailoring and applying formal methods to advanced embedded controllers, at various phases of the development and verification process, illustrated by industrial projects and collaborations.
A first line of work, carried out in partnership with Airbus, Dassault and LAAS-CNRS, aims at going beyond simulation for validating advanced hybrid control laws, by leveraging bounded reachability analysis and robustness analysis from the early design phases. This requires to bridge the representation gap existing between hybrid dataflow formalisms used to model control laws (e.g. Simulink, Scade-Hybrid, …), and the automata-based formalisms used by most hybrid model-checkers (e.g. SpaceEx, Flow*, dReach, …) and robustness analysis frameworks. We discuss the steps taken to handle the complexity and size of typical industrial models.
A second line of work, carried out jointly with academic lab LRI (Paris-Sud, INRIA) and technology provider OcamlPro, addresses the sound combination of SMT-solvers and potentially unsound convex optimization engines to allow proving complex polynomial invariants on advanced control laws implementations. Such implementations are usually obtained by automatic time-discretization and code generation from a hybrid dataflow model. The proposed approach shows a notable performance improvement on controllers of interest with respect to earlier approaches based on interval arithmetic or purely symbolic methods such as cylindrical algebraic decomposition or virtual substitutions.
Last, we present research conducted in partnership with Liebherr Aerospace Toulouse and technology provider Systerel on leveraging model-checking techniques for unit-level test case generation for an air management system, taking into account the industrial setting and qualification constraints, following DO-178C and D0-333 guidelines.

Rémi Delmas is a research engineer in the Deptartment of Information Processing and Systems at ONERA. He received an aerospace engineering degree from ENSMA in 2000, and completed a PhD in theoretical computer science ONERA-Sup’Aero in 2004, on the topic of compositional
modelling and verification of intergated modular avionics systems. Between 2004 and 2009, he worked for Prover Technology, building SAT-based model checking solutions critical railway and train control systems. Back at ONERA since 2009, his research work focuses on adapting and using SAT and SMT-based techniques to solve various problems surrounding critical embedded software design and verification, ranging from safety assessment and fault-tolerant architecture synthesis to functional verification and automatic test case generation.