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

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.