Title: Security Protocols: Model Checking Standards
Abstract: The design of security protocols is typically approached as an art, rather than a science, and often with disastrous consequences. But this need not be so! I have been working for ca. 20 years on foundations, methods, and tools, both for developing protocols that are correct by construction and for the post-hoc verification of existing designs. In this talk I will introduce my work in this area and describe my experience analyzing, improving, and contributing to different industry standards, both existing and upcoming.
Bio: David Basin is a full professor within the Department of Computer Science, ETH Zurich since 2003, where he heads the Information Security Group. He is also department head. He received his bachelor’s degree in mathematics from Reed College in 1984, his Ph.D. from Cornell University in 1989, and his Habilitation from the University of Saarbrücken in 1996. His appointments include a postdoctoral research position at the University of Edinburgh (1990 - 1991), and afterwards he led a subgroup, within the programming logics research group, at the Max-Planck-Institut für Informatik (1992 - 1997). From 1997 - 2002 he was a full professor at the University of Freiburg where he held the chair for software engineering. His research focuses on Information Security, in particular on foundations, methods, and tools for modeling, building, and validating secure and reliable systems. He is Editor-in-Chief of the ACM Transactions on Privacy and Security and of Springer-Verlag’s book series on Information Security and Cryptography. He is also the founding director of ZISC, the Zurich Information Security Center, which he led from 2003-2011. He was named Fellow of the ACM in 2018 for his contributions to Information Security and Formal Methods.
Title: Making Sense of Fast Big Data
Abstract: Computing systems that make human sense of big data, usually called personalization systems or recommenders, and popularized by Amazon and Netflix, essentially help Internet users extracting information of interest to them. Leveraging machine learning techniques, research on personalization has mainly focused on improving the quality of the information extracted, according to some measure of quality. Yet, building an operational recommender goes far beyond, especially in a world where data is not only big but also changes very fast. This talk will discuss system challenges to scale to a large number of users and a growing volume of fastly changing data to eventually provide real-time personalization.
Bio: Anne-Marie Kermarrec is a senior researcher at Inria, France where she led a research group on large-scale distributed systems from 2006 to 2015. She is currently the CEO of the Mediego startup that she founded in April 2015. Mediego provides content personalisation services for online publishers, and directly builds on her recent research.She got a PhD thesis from University of Rennes, and has been with Vrije Universiteit, NL and Microsoft Research Cambridge, UK. Anne-Marie received an ERC grant in 2008 and an ERC proof of Concept in 2013. She received from the French Academy of Science the Montpetit Award in 2011 and the Innovation Award in 2017. She has been elected to the European Academy in 2013 and named ACM Fellow in 2016. Her research interests are large-scale distributed systems, peer to peer networks and system support for machine learning.
Title: Versatile Quantitative Modelling: Verification, Synthesis and Data Inference for Cyber-Physical Systems
Abstract: Computing systems are becoming ever more complex, encompassing autonomous control of physical processes, stochasticity and inference from sensor data. This lecture will demonstrate the versatility of quantitative modelling and verification to aid the design of cyber-physical systems with machine learning components. Topics discussed will include recent advances in probabilistic/quantitative verification, template-based model synthesis, resource-performance trade off analysis, attacks on biometric security, and robustness guarantees for machine learning components. The lecture will conclude by giving an overview of future challenges in this field.
Bio: Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. Prior to this she was Professor in the School of Computer Science at the University of Birmingham, Lecturer at the University of Leicester and Assistant Professor at the Jagiellonian University in Cracow, Poland. Kwiatkowska has made fundamental contributions to the theory and practice of model checking for probabilistic systems, focusing on automated techniques for verification and synthesis from quantitative specifications. She led the development of the PRISM model checker (www.prismmodelchecker.org), the leading software tool in the area and winner of the HVC Award 2016. Probabilistic model checking has been adopted in diverse fields, including distributed computing, wireless networks, security, robotics, healthcare, systems biology, DNA computing and nanotechnology, with genuine flaws found and corrected in real-world protocols. Kwiatkowska is the first female winner of the Royal Society Milner Award and was awarded an honorary doctorate from KTH Royal Institute of Technology in Stockholm in 2014. She won two ERC Advanced Grants, VERIWARE and FUN2MODEL, and is a coinvestigator of the EPSRC Programme Grant on Mobile Autonomy. Kwiatkowska is a Fellow of ACM and Member of Academia Europea.
Title: ALGORAND - The Distributed Ledger for the Borderless Economy
Abstract: A distributed ledger is a tamperproof sequence of data that can be read and augmented by everyone. Distributed ledgers stand to revolutionize the way democratic societies and traditional economies operate. They secure all kinds of traditional transactions –such as payments, asset transfers, titling– in the exact order in which they occur; and enable totally new transactions –such as cryptocurrencies and smart contracts. They can remove intermediaries and usher in a new paradigm for trust. As currently implemented, however, distributed ledgers cannot achieve their enormous potential. The global participation and trust necessary to realize an inclusive and borderless economy require substantially better technology. Algorand is an alternative, democratic, and efficient distributed ledger. Unlike prior ledgers based on ‘proof of work’, it dispenses with ‘miners’. Indeed, Algorand requires only a negligible amount of computation. Moreover, its transaction history does not ‘fork’ with overwhelming probability: i.e., Algorand guarantees the finality of all transactions. In addition, Algorand guarantees flexible self-governance. A successful society and economy must be able to evolve. A cryptocurrency cannot be an ocean liner on autopilot. By using its hallmark propose-and-agree process, Algorand can consensually correct its course, as necessary or desirable, without any ‘hard forks’, to meet the current and future needs of the community.
Bio: Silvio Micali has been on the faculty at MIT, Electrical Engineering and Computer Science Department, since 1983. Silvio’s research interests are cryptography, zero knowledge, pseudorandom generation, secure protocols, and mechanism design. In 2017, Silvio founded Algorand, a fully decentralized, secure, and scalable blockchain which provides a common platform for building products and services for a decentralized economy. At Algorand, Silvio oversees all research, including theory, security and crypto finance. Silvio is the recipient of the Turing Award (in computer science), of the Goedel Prize (in theoretical computer science) and the RSA prize (in cryptography). He is a member of the National Academy of Sciences, the National Academy of Engineering, and the American Academy of Arts and Sciences and of the Academia dei Lincei. Silvio has received his Laurea in Mathematics from the University of Rome, and his PhD in Computer Science from the University of California at Berkeley.
Title: Towards Formally Designing Collective Adaptive Systems
in cooperation with Lenz Belzner, Thomas Gabor, Rolf Hennicker, and Alexander Knapp
Abstract: Many modern software systems are distributed and consist of interacting entities that have to cope at runtime with dynamically changing environments and possibly also with new requirements. We call such systems ensembles or – in case the entities are collaborating - collective adaptive systems. Examples are robot swarms and also socio-technical systems such as smart city or smart health care applications. As the interactions between the participants of an ensemble may lead to unexpected reactions and as unforeseen functionalities may be needed in order to react correctly to changes of the environment, conventional software development techniques and approaches – be they agile or waterfall - might not provide adequate support. Novel rigorous engineering techniques are needed where mathematical as well as artificial intelligence techniques and foundational methods play a prominent role. This talk presents a systematic approach for designing ensembles including an ensemble engineering life cycle, an ensemble specification method based on dynamic logic and two complementary approaches to adaptation: role-based adaptation modelling and online planning using reinforcement learning.
Bio: Martin Wirsing is vice president for teaching and studies of LMU Munich and full professor for Informatics. In 2016, he was awarded a Degree of Doctor of Science (Honoris Causa) by Royal Holloway, University of London. His research interests comprise software engineering and its formal foundations, autonomous self-aware systems, and digitalization of universities. In 2006-2015 he was coordinating the European IP projects SENSORIA (2006-2010) on software engineering for service-oriented systems and ASCENS (2010-2015) on engineering collective autonomic systems. In 2007-2010 Martin Wirsing was the chairman of the Scientific Board of INRIA and in 2014-2017 a member of the scientific committee of Institut Mines-Télécom. Currently, he is the chair of the board of trustees of Max Planck Institute of Psychiatry and of the scientific committees of the University of Bordeaux and IMDEA Software Institute. He is a member of the editorial board of several scientific journals and book series including Theoretical Computer Science, Electronic Proceedings in Theoretical Computer Science, and Transactions on Foundations for Mastering Change.