Dec 20, 1 PM in ICT-507-AB "TD^3: Principles for Trustworthy Software Systems, and how to adopt them"
At Software Science Departmental seminar on Thursday, Dec 20, 2018 at 1 PM Prof. Marino Miculan (University of Udine, Italy) will talk about "TD^3: Principles for Trustworthy Software Systems, and how to adopt them".
The seminar will take place in ICT-507-AB.
Trustworthiness is a holistic property, encompassing security, correctness, reliability, privacy, safety, and survivability. It is not sufficient to address only some of these dimensions, nor it is sufficient simply to assemble trustworthy components. In fact, trustworthiness requires to follow precise development models and to adopt verification tools and testing procedures along the whole software lifecycle. This adoption can be guided by three high level principles: Trustworthy by Design, Trustworthy by Default, Trustworthy by Deployment.
In this lecture we will review these principles, and discuss how formal methods-based tools are crucial to support their adoption. To this end, we will analyse two different case studies, showing how formal methods can be used to improve Trustworthy by Design and by Deployment. In the first example, we will examine the formalisation of MTProto 2.0 and Telegram Passport, two protocols at the core of the popular app Telegram. This formalisation, carried out in the applied π-calculus, is used within the tool ProVerif for the verification of required security properties. In the second example, we consider a formal model for container-based systems, which are commonly used in modern (micro)services-oriented architectures. This model, developed within the framework of Bigraphical Reactive Systems, allowed us to implement new tools for verifying correctness properties of container composition configurations.
Marino Miculan received the Ph.D. degree in Computer Science from the University of Pisa in 1997. Currently he is Associate Professor in Computer Science at the University of Udine, Italy, and he held the Italian national habilitation as Full Professor in Computer Science. In his career he has taught more than 40 courses on Operating Systems, Computer Networks, Distributed Systems, Formal Methods, at the BSc, MSc and PhD levels. He has (co-)authored about 70 publications on formal methods for verification on programs and systems, logical frameworks, type theory, programming language semantics, (meta)models of distributed and concurrent systems, and cryptographic protocols correctness. He has served as Chair, PC Chair, Session Chair, PC Member for several international conferences.
His current research interests include formal (meta)models and tools for the development of trustworthy systems, with particular attention to security and quantitative aspects.