Invited Speakers of VECoS 2018
Parosh Aziz Abdulla, Uppsala University, Sweden
Fault injection, from software to hardware and reversed
Axel Legay, Inria Rennes, France
Abstract: Fault injection is a well known method to test the robustness and security vulnerabilities of software. Fault injections can be explored by simulations (cheap but not validated) and hardware experiments (true, but very expensive). Recent simulation works have started to apply formal methods to the detection, analysis, and prevention of fault injection attacks to address verifiability. However, these approaches are ad-hoc and extremely limited in architecture, fault model, and breadth of application. Further, there is very limited connection between simulation results and hardware experiments. Recent work has started to consider broad spectrum simulation approaches that can cover many fault models and relatively large programs. Similarly the connection between these broad spectrum simulations and hardware experiments is being validated to bridge the gap between the two approaches. This presentation highlights the latest developments in applying formal methods to fault injection vulnerability detection, and validating software and hardware results with one another.
Short Bio: Axel Legay is a researcher at the Institut national de recherche en informatique et en automatique (INRIA Rennes, France). He received his Ph.D. in Computer Science from the University of Liège, Belgium. His main research interests are in formal verification and cyber security. He is a major contributor of statistical model checking which he recently used for fault-injection analysis. Axel is also a referee for top journals and conferences. He has organized several international conferences such as ATVA, TACAS, or RV.
Automated Black-box verification of Networking Systems
Alexandra Silva, University College London, UK
Abstract: Our society is increasingly reliant on complex networking systems, consisting of several components that operate in a distributed/concurrent fashion, exchange data that may be highly sensitive, and are implemented with a mix of open and closed-source code. In this talk, we will present a broad overview of techniques and tools to automate the modelling and verification of networking software systems. We will focus mainly on the model learning paradigm, originally proposed in artificial intelligence, to automatically build an automaton model of a running system in a black-box fashion -- purely via interactions with the running system.
Short Bio: Alexandra Silva is a theoretical computer scientist whose main research focuses on semantics of programming languages and modular development of algorithms for computational models. A lot of her work uses the unifying perspective offered by coalgebra, a mathematical framework established in the last decades. Alexandra is currently a senior lecturer at University College London. Previously, she was an assistant professor in Nijmegen and a post-doc at Cornell University, with Prof. Dexter Kozen, and a PhD student at the Dutch national research center for Mathematics and Computer Science (CWI), under the supervision of Prof. Jan Rutten and Dr. Marcello Bonsangue. She was the recipient of the Presburger Award 2017, the Leverhulme prize 2016, and an ERC starting Grant in 2015.