Karthik Pattabiraman

Karthik Pattabiraman is a Professor of Electrical and Computer Engineering at the University of British Columbia (UBC). He received his MS and PhD in computer science from the University of Illinois at Urbana Champaign (UIUC) in 2004 and 2009, and spent a postdoctoral year at Microsoft Research (MSR), Redmond before joining UBC in 2010. His research interests are in dependability, security, and software engineering. Karthik has won multiple awards such as the Inaugural Rising Star in Dependability Award, 2020, from the IEEE and the IFIP, the distinguished early-career alumnus award from the University of Illinois (UIUC), CS department, 2018, and multiple UBC-wide awards for excellence in research and mentoring. Together with his students and collaborators, he has published over 100 papers, many of which have received distinguished paper awards at venues such as DSN and ICSE. He is a distinguished contributor of the IEEE computer society, a distinguished member of the ACM, and the vice-chair of the IFIP Working Group on dependable computing and fault-tolerance (WG 10.4). A detailed biography may found at: https://blogs.ubc.ca/karthik/about/full-bio/.

Fault Injection is Dead. Long Live Fault Injection!

Abstract: Fault injection (FI), or fault simulation, is one of the most popular methods to evaluate the dependability of real-world systems. FI has a rich history in our community, going back nearly five decades. FI has led to fundamental insights into the dependability of numerous real-world systems, and has spurred significant research in diverse areas. There have also been many mature fault injection tools developed, many of which have been successfully deployed in industry. Yet, there is a perception in other communities that FI is a solved research problem, and that the only remaining challenges in FI are engineering issues. In this talk, I will argue that this is far from the truth, and that there are still many unaddressed research questions pertaining to the accurate emulation of hardware and software faults. I will also argue that FI is even more important in new domains such as machine learning (ML) and autonomous systems. I will draw upon my research group’s work in the FI area over the last decade or so, as well as discussions with different stakeholders, to outline what I believe are the grand challenges for FI. This is joint work with my students and colleagues at UBC, and industry collaborators.

José Bacelar Almeida

José Bacelar Almeida currently an Assistant Professor at the Department of Informatics at Universidade do Minho and researcher at HASLab/INESC TEC. He obtained my PhD degree in Computer Science from this university in 2003. His research interests lie in Cryptography and Information Security and its intersection with Program Verification. He has been working on the development of high-assurance cryptographic implementations for the last 10 years, aiming to bridge the gap between theoretical security and real-world security. He is particularly interested in provable security and its interplay with the formal verification of cryptographic proofs and cryptographic software implementations.

Jasmin/EasyCrypt — a framework for high-assurance software development

Abstract: Jasmin is a low-level language designed to support the development of high-assurance and high-speed cryptographic software. It was designed to support the so-called “assembly in the head” programming, that smoothly combines high-level constructs (such as control-flow; typed variables and memory; etc.) that favour expressiveness and verification, with architectural-level ones (assembly instructions, flag manipulation, etc.) that empower programmers essentially the same level of control as if they were using directly assembly to develop optimised implementations. For the verification of Jasmin programs, the framework leverages on EasyCrypt — a theorem prover originally developed to formalise security proofs, which supports program logics for reasoning about correctness and equivalence of imperative programs. In this talk we shall present the main features of the Jasmin/EasyCrypt development framework, and the design choices that have driven its development. In doing it, we intend to make the case that most of those features are shared by other applications domains beyond cryptographic software development, such as embedded or safety-critical systems.