2023 Hot Topics in Language-based Security seminar series
Hot topics in language-based security is a series of seminars that will be held by well-known international speakers, organised by the PhD in Computer Science of University of Pisa in collaboration with IMT Lucca, as part of their Research Topics in Software Quality series.
The first part of these seminars, mainly devoted to secure compilation and isolation mechanisms, will also be offered to MS students within the course "Laboratory for Innovative Software".
To get the credits for this seminar series, each PhD student must attend 80% of the seminars.
The seminars address methods and techniques that foster the security of applications and systems from their design and implementation, by focusing on formal methods and the features and properties of programming languages.
To participate in the seminars please contact gian-luigi.ferrari@unipi.it or chiara.bodei@unipi.it.
- March, 14, at 14:00: Roberto Di Cosmo
Location: Aula Seminari Ovest, Computer Science Department and online.
Title: Securing the (Open Source) Software Supply chain: challenges and opportunities
Abstract:Software security is a broad and well established domain, with many research projects and industry products focusing on the traditional goal of detecting, and possibly fixing, vulnerabilities present in a specific software code base. Open Source has brought a new dimension into play: by making available large amounts of software components, developed and distributed collaboratively across the world, it has immensely sped up innovation, but also raised key challenges about the quality, evolution and security of what is today called the "software supply chain" of modern software systems, where many components from disparate origins are put together. How can we search for vulnerabilities among millions of software projects? How can we track their propagation? How can one make sure that the source code of a key module used today will be still there when it is needed in the future? Do we really know what source code we are using, and where it comes from (the Know Your Software principle)? how can we address cybersecurity if we do not know? How do we share this information across the software supply chain? Answering these questions and answering them at scale is quite a challenge. In this presentation, you will discover Software Heritage, an open non-profit initiative, in partnership with Unesco and supported by major IT players, and how the revolutionary infrastructure it is building offers great opportunities to change the way we address these issues. With more than 14 billions unique source files from more than 210 million repositories, it is the largest archive of source code ever built, and you can already access and use it for a variety of purposes.
Material Slides
Short Bio: Biographical information - March, 21, at 14:00: Matteo Busi
Location:
Aula Seminari Ovest, Computer Science Department and Online
Title: Automated Learning and Verification of Embedded Security Architectures
Abstract: Techniques to verify or invalidate the security of computer systems have come a long way in recent years. While sophisticated tools are available to specify and formally verify the behavior of a system, attack techniques have evolved to the point of questioning the possibility of obtaining adequate levels of security, especially in critical applications. In a recent paper, Bognar et al. have clearly highlighted this inconsistency between the two worlds: on one side, formal verification allows writing irrefutable proofs of the security of a system, on the other side, concrete attacks make these proofs waver, exhibiting a gap between models and implementations which is very complex to bridge. In this seminar, we outline a new general methodology based on robust non-interference preservation that reduces this gap by bringing together some peculiarities of the two approaches. Our methodology uses automata learning to extract behavioral models of real systems, and model checking to analyze them and identify attacks or anomalies.
Short Bio: Matteo Busi is a research fellow at Ca' Foscari University, Venice. Previously, he was a PhD student at the University of Pisa and a postdoc at the University of Pisa and at Ca' Foscari. His research interests include cyber-security, programming languages, and formal methods. Currently, he is focusing on secure compilation: "how is it possible to guarantee that program transformations preserve security properties?'' - April, 18, at 14:00: Gian-Luigi Ferrari
Location: Conference room (San Ponziano), IMT Lucca and online
Title: Declarative secure placement of FaaS orchestrations in the Cloud-Edge continuum
Abstract: The decision-making related to the placement of applications made from orchestrated serverless functions onto Cloud-Edge infrastructures is a challenging problem as it must consider functional and non-functional requirements. We illustrate a novel declarative methodology to determine the placement of FaaS orchestration onto Cloud-Edge resources while satisfying the requirements of the FaaS orchestrations and relying on information-flow analyses to prevent information leaks through side channels. The methodology is assessed via a prototype implementation.
(Joint Work with Alessandro Bocci, Antonio Brogi and Stefano Forti)
Short Bio: Gian-Luigi Ferrari is full professor at the Computer Science Department of University of Pisa. His research interests fall in the area of semantic theories for concurrent programming and specification languages. He is also interested in the development of programming languages for highly distributed networks and semantic-based verification environments. - April, 20, at 14:00: Alberto Llluch Lafuente
Location: Aula Seminari Ovest, Computer Science Department and online
Title: Threat Modelling and Assessment with Attack Trees
Abstract: Threat modelling is one of the key activities of security-by-design approaches to cybersecurity. Graphical models of security such as attack trees are particularly appealing to support threat modelling: On the one hand they provide an intuitive visual representation which is easily accessible to all relevant personnel, thus facilitating the dialogue between security experts and decision makers (e.g. managers); On the other hand, they can be provided a rigorous mathematical meaning, which can be leveraged into effective assessment tools. In this talk, I will give an overview of some typical features of attack-tree models as well as some of the current research topics in this area. The focus of the talk will be on the formal foundations of attack-tree models but I will also mention some tools. I will illustrate how attack tree model features are formalised and analysed with classical formal methods instruments: constraint solving, games and stochastic model checking.
Short Bio: Alberto Lluch Lafuente is Full Professor at the Technical University of Denmark. He is currently head of the section for Software Systems Engineering. Previously, he was Associate Professor at the Technical University of Denmark, Assistant Professor at IMT School for Advanced Studies Lucca and Postdoctoral Researcher at the University of Pisa. He obtained his PhD degree from the Albert-Ludwigs Universität in Freiburg in 2003. His research interests are formal methods, software engineering, concurrent and distributed systems, security and artificial intelligence. - May, 11 at 14:00: Stefano Calzavara
Location: Aula Seminari Ovest and online
Title: Formal security verification of tree-based classifiers
Abstract: Decision trees and tree ensembles are popular classification models for tabular data. Similar to other machine learning models, however, they are susceptible to evasion attacks at test time, where adversarial perturbations might transform inputs so that they get misclassified. In this talk, I present some recent results on the security verification of tree-based classifiers. First, I introduce a new security measure called resilience, which mitigates some of the issues of the traditional robustness measure, and I discuss how resilience can be soundly estimated for tree-based classifiers. Then, I introduce a new paradigm called "verifiable learning", which advocates the adoption of new training algorithms designed to learn models which are easy to verify. In particular, I present a new class of tree ensembles admitting security verification in polynomial time, thus escaping from classic NP-hardness results, and I discuss how such models can be trained and efficiently verified.
Short Bio: Stefano Calzavara is an associate professor in computer science at Università Ca' Foscari Venezia. His main research interests are software security, formal methods and their intersection. Stefano has published more than 50 papers on these topics, often at major conferences and journals. He is currently serving as the PC chair of the IEEE Computer Security Foundations Symposium and as the leader of the Italian chapter of OWASP. - May, 16 at 14:00: Mirco Tribastone
Location: Aula Seminari Ovest and online
Title: Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Abstract: Computing the posterior distribution of a probabilistic program is a challenging task for which no one-fit-for-all solution exists. We propose Gaussian Semantics, which approximates the probabilistic semantics of a bounded straight-line program using Gaussian mixtures. It is parametrized by a map associating each program location with the moment order to be matched in the approximation. We provide two main contributions. The first is a universal approximation theorem stating that, under mild conditions, Gaussian Semantics can approximate the exact semantics arbitrarily closely. The second is an approximation that analytically matches up to second-order moments in the face of the generally difficult problem of matching moments of Gaussian mixtures with arbitrary moment order. We test our second-order Gaussian approximation on several case studies from the literature. We show that it can provide accurate estimates, for both continuous and discrete posteriors, in models not supported by competing approximation methods or when exact symbolic techniques fail because of complex expressions or non-simplified integrals requiring expensive numerical solutions.
This is joint work with Luca Bortolussi, Emilio Incerto, and Francesca Randone.
Short Bio: Mirco Tribastone is a Professor of Computer Science at IMT School for Advanced Studies Lucca since 2020, where he leads the research group SySMA - Systems Security Modeling and Analysis. He currently serves as Deputy Rector and scientific coordinator of the Ph.D. doctoral track on Software Quality. Previously, Mirco has been an Associate Professor of Computer Science at IMT since 2015, after holding a position as Associate Professor at the University of Southampton (2013-2015) and as Juniorprofessur at the Ludwig-Maximilians University of Munich (2010-2013). He received a Ph.D. in Computer Science from the University of Edinburgh in 2010. Mirco's research interests are related to the development and analysis of models for dynamical systems, with a focus on the study of performance for computer systems and applications to complex networks, for which he has authored over 120 scientific publications. After having been principal investigator for research projects funded by the European community and the German research foundation DFG, and having served as guest professor through a DFG-funded Mercator Fellowship at the TU Braunschweig (Germany), Mirco is currently the national coordinator of a three-year project funded by the Italian Ministry of University and Research on topics concerning cyber-physical systems. Since 2020, he has been involved in technology transfer through the start-up Valuematic, of which he is a founding partner. - May, 18 at 14:00: Roberto Giacobazzi
To be confirmed Location: Aula Seminari Est and online
Title: Hacking Program Analysis - On the Properties of (In)Complete Abstract Interpretations
Abstract: In this talk I will introduce the foundations and design principles of code protecting transformations for anti reverse engineering applications. This is a gentle introduction to some of the main results concerning both the limits and the possibilities of making code obscure and unlearnable. The battle scenario involves (automated) attackers intended to extract information by reverse engineering the code, and protecting code transformations modeled as distorted compilers devoted to inhibit these attacks. Attacks are inhibited by maximizing imprecision in all attempts made by the attacker (which is an algorithm) to exploit control and data-flow of the obscured code. We show that protecting transformations can be systematically and formally derived as distorted compilers, obtained by virtualizing the source code, i.e., by specializing a suitably distorted interpreter for the given programming language with respect to the source code to protect. The limits of these methods are shown in the context of computability theory. Interestingly, this distortion corresponds precisely to defeat the potency of the expected attacker, which is itself an interpreter and whose potency consists in its ability to extract a complete and precise view of the program's execution.
Short Bio: Roberto Giacobazzi received a PhD in Computer Science (CS) in 1993 from the University of Pisa. From 1993 to 1995, he was PostDoc at the Ecole Polytechnique (Paris) in the equipe of Patrick and Radhia Cousot. Back to the University of Pisa as Assistant Professor in 1995, he moved to the University of Verona as Associate Professor in 1998. Since May 2000 he is Full Professor in CS at the University of Verona. During the last two decades he has been Provost for Education (2001-2004), Provost for Research (2004-2006 and 2022), Dean of the College of Science and Technology (2006-2012), and Head of the CS Department (2019-2021). In 2012 he has been Chair of the National Scientific Qualification Committee for Professorship in CS in Italy. Since 2016 he is Affiliate Faculty at the IMDEA Software Institute in Madrid (Spain) with a Cátedra de Excelencia of the Comunidad de Madrid, awarded in 2017. He is currently Deputy Rector of the University of Verona. His research interests include abstract interpretation, program analysis and verification, semantics of programming languages, program transformation and optimization, security, computability, history of CS, and lattice theory. He was co-founder of JuliaSoft, now part of GrammaTech Inc., USA. General Chair of the 40th ACM POPL2013 and member of the steering committee of POPL until 2015 and of major conferences in program analysis and program verification, he was PI of international projects in the area of Programming Languages. He received the Microsoft Research Software Engineering Innovation Foundation (SEIF) Award in 2013, the Facebook Probability and Programming Research Award in 2020, the Amazon Research Award (ARA) in 2021, and the WhatsApp Research Awards on Privacy Aware Program Analysis in 2022. - May, 23 at 15:00: Marino Miculan
Location: Aula Seminari Ovest and online
Title: Bigraphical models for Container-based Systems
Abstract: Nowadays, containers play a central role in service-oriented architectures, as they allow developers to focus on the logic and dependencies of applications, while system administrators can focus on deployment and management issue. In this talk, we will present a formal model for container-based systems, using the framework of Bigraphical Reactive Systems (BRSs). We first introduce "local directed bigraphs", a variant of bigraphs which allows to deal with localized resources. Then, we define the signature for containers. It turns out that the composition of containers (as implemented by docker-compose or kubectl) corresponds precisely to the composition of the corresponding bigraphs. Moreover, the bigraphic objects representing containers and "pods" can be analysed using techniques from graph theory; e.g., properties about containers can be formalized as properties of the corresponding bigraphic representations. As an example, we show how a potential information leakage in a system can be statically detected by analyzing its bigraphical representation.
Short Bio: Marino Miculan (PhD in Computer Science, University of Pisa, 1997) is Associate Professor at the University of Udine, where he leads the laboratory of Models and Applications of Distributed Systems and the node of the National CyberSecurity Laboratory of CINI. Since May 2022 he has a second affiliation at the University of Venice. He has published about 90 papers in international journals and proceedings; chaired 7 international conferences and been on the PC of other 35. He has participated in 15 national and international projects, usually with leadership positions. Currently Marino Miculan is interested in security issues of distributed, component-based and smart systems; to this end, he applies formal methods to define new models, languages, methodologies and techniques for the formalisation and verification of security properties of these systems. Besides, he knows one or two things about process calculi, distributed ledgers, session types, category theory and logic, bigraphs, coalgebras, structured operational semantics, nominal sets, systems biology, type theory, logical frameworks, proof assistants. - May, 24 at 15:00: Massimo Bartoletti
Location: Aula Seminari Ovest and online
Title: MEV-freedom, in DeFi and beyond
Abstract: Extractable Value refers to a wide class of economic attacks to public blockchains, where adversaries with the power to reorder, drop or insert transactions in a block can "extract" value from user transactions. Empirical research has shown that mainstream protocols, like e.g. decentralized exchanges, are massively targeted by these attacks, with detrimental effects on their users and on the blockchain network. Despite the growing impact of these attacks in the real world, solid theoretical foundations are still missing. In this presentation we discuss some existing attempts towards a formal definition and understanding of MEV. In particular, we present a theory of Extractable Value based on a general, abstract model of blockchains and smart contracts. This theory is the basis for formal proofs of security against Extractable Value attacks.
Short Bio: Massimo Bartoletti is Associate Professor at the Department of Mathematics and Computer Science of the University of Cagliari. His research activity concerns the development of tools and techniques for the specification, analysis and verification of software, with a special emphasis on security. Massimo Bartoletti is founder of the laboratory Blockchain@Unica, one of the first academic research group on blockchain technologies in Italy, director of the node of the Cyber Security National Lab for the University of Cagliari, and core member of the CINI working group on Blockchain. The laboratory is currently investigating several aspects of blockchain technologies, among which custom Domain-Specific Languages for smart contracts. He is principal investigator of several R&D projects on blockchain technologies, and member of the scientific board of several workshops on blockchain technologies. He is also the organisation chair of the first International School on Algorand Smart Contracts, funded by a grant of the Algorand Foundation. - June, 5 at 14:30: Guido Salvaneschi
Location: Aula Seminari Ovest and online
Title: Language abstractions for secure software and systems
Abstract: Programming languages have proven to be effective tools for ensuring non-functional properties of software applications. They facilitate the use of lightweight formal methods, such as type systems, which enable software verification with minimal effort on the part of developers. Additionally, language design can be employed to guide developers towards adopting specific programming practices, thereby promoting the concept of security by design. In this presentation, we will explore various domains where the deliberate selection of language abstractions can enhance the security of distributed software systems. We will examine examples from smart contracts on blockchain platforms, distributed query processing, and secure enclave programming. Lastly, we will provide an overview of promising research directions in the realm of Infrastructure as Code.
Short Bio: Guido Salvaneschi is leading the Programming group at the School of Computer Science, University of St. Gallen, Switzerland. He holds a Ph.D. in Information Technology from Politecnico di Milano, Italy. He has been a postdoc and an Assistant Professor at the Technical University of Darmstadt, Germany. His research has been supported, among others, by the German Research Foundation (DFG) and by the Swiss National Science Foundation (SNSF). He has published papers in a number of programming languages and software engineering venues including OOPSLA, PLDI, ECOOP, ICSE, FSE, ASE and TSE.
Personal website
Organizators
- Chiara Bodei: chiara.bodei@unipi.it
- Lorenzo Ceragioli: lorenzo.ceragioli@unipi.it
- Gabriele Costa: gabriele.costa@imtlucca.it
- Pierpaolo Degano: pierpaolo.degano@unipi.it
- Gian-Luigi Ferrari: gian-luigi.ferrari@unipi.it
- Letterio Galletta: letterio.galletta@imtlucca.it