Massimo Bartoletti

Giu 062018
Upcoming Seminar
Transcompiling and Analysing Firewalls
June 11, 17.00 (Aula F) Palazzo delle Scienze - Cagliari  
Letterio Galletta IMT Lucca (IT)
Abstract. Configuring and maintaining a firewall configuration is notoriously hard. On the one hand, network administrators have to know in detail the policy meaning, as well as the internals of the firewall systems and of their languages. On the other hand, policies are written in low-level, platform-specific languages where firewall rules are inspected and enforced along non trivial control flow paths. Further difficulties arise from Network Address Translation (NAT), an indispensable mechanism in IPv4 networking for performing port redirection and translation of addresses.
Lug 182016

Upcoming Seminar

July 22, 15.00 (Aula C)
Palazzo delle Scienze - Cagliari

Andrea Bracciali

SICSA Lecturer - University of Stirling (UK)

Abstract. Decentralised smart contracts represent the next step in the development of protocols that support the interaction of independent players without the presence of a coercing authority. Based on protocols à la BitCoin for digital currencies, smart contracts are believed to be a potentially enabling technology for a wealth of future applications. The validation of such an early developing technology is as necessary as it is complex. In this paper we combine game theory and formal models to tackle the new challenges posed by the validation of such systems.
 Scritto da in 18 Luglio 2016  seminari  Commenti disabilitati su Seminar: Validation of Decentralised Smart Contracts Through Game Theory and Formal Methods
Lug 022016
Upcoming Seminar
July 7, 15.00 (Aula C) Palazzo delle Scienze - Cagliari
Alceste Scalas
Imperial College London
Abstract. Designing, developing and maintaining concurrent applications is an error-prone and time-consuming task; most difficulties arise because compilers are usually unable to check whether the inputs/outputs performed by a program at runtime will adhere to a given protocol specification. To address this problem, we propose lightweight session programming in Scala: we leverage the native features of the Scala type system and standard library, to introduce (1) a representation of session types as Scala types, and (2) a library, called lchannels, with a convenient API for session-based programming, supporting local and distributed communication. We generalise the idea of Continuation-Passing Style (CPS) protocols, studying their formal relationship with session types. We illustrate how session programming can be carried over in Scala: how to formalise a communication protocol, and represent it using Scala classes and lchannels, letting the compiler help spotting protocol violations. We attest the practicality of our approach with a complex use case, and evaluate the performance of lchannels with a series of benchmarks.
 Scritto da in 2 Luglio 2016  seminari  Commenti disabilitati su Seminar: Lightweight session programming in Scala
Giu 132016

1 - Introduction to cryptocurrencies and smart contracts

15.4.2016 h12.00 - Lab M (Massimo Bartoletti)

2 - Introduction to smart contracts in Ethereum

22.4.2016 h12.00 - Lab M (Tiziana Cimoli)  --  Slides

3 - Incentives for smart contracts

29.4.2016 h11.00 - Lab M (Nicola Atzei) -- Slides

4 - Vulnerabilities of Bitcoin

6.5.2016 h11.00 - Lab M (Stefano Lande) -- Slides

5 - Analysis of the Bitcoin protocol

13.5.2016 - h11.00 - Lab M (Alessandro Sebastian Podda) -- Slides

6 - Ethereum in depth

20.5.2016 h11.00 - Lab M (Nicola Atzei and Tiziana Cimoli) -- Slides

7 - A survey of frameworks for smart contracts

27.5.2016 h11.00 - Lab M (Livio Pompianu) -- Slides

 Scritto da in 13 Giugno 2016  seminari  Commenti disabilitati su Seminars series: cryptocurrencies and smart contracts
Set 022015
Compliance and subtyping in timed session types September 7, 15.45 (Aula F) Palazzo delle Scienze - Cagliari Maurizio Murgia
Dipartimento di Matematica e Informatica, Università degli Studi di Cagliari
Abstract. We propose an extension of binary session types, to formalise timed communication protocols between two participants at the endpoints of a session. We introduce a decidable compliance relation, which generalises to the timed setting the usual progress-based notion of compliance between untimed session types. We then show a sound and complete technique to decide when a timed session type admits a compliant one, and if so, to construct the least session type compliant with a given one, according to the subtyping preorder induced by compliance. Decidability of subtyping follows from these results. We exploit our theory to design and implement a message-oriented middleware, where distributed modules with compliant protocols can be dynamically composed, and their communications monitored, so to guarantee safe interactions.
 Scritto da in 2 Settembre 2015  seminari  Commenti disabilitati su Seminar: Compliance and subtyping in timed session types
Set 022015

Upcoming Seminar

On the decidability of honesty and of its variants

September 3, 11.30 (Aula F)
Palazzo delle Scienze - Cagliari

Massimo Bartoletti
Dipartimento di Matematica e Informatica, Università degli Studi di Cagliari

We address the problem of designing distributed applications which require the interaction of loosely-coupled and mutually distrusting services. In this setting, services can use contracts to protect themselves from unsafe interactions with the environment: when their partner in an interaction does not respect its contract, it can be blamed (and punished) by the service infrastructure. We extend a core calculus for services, by using a semantic model of contracts which subsumes various kinds of behavioural types. In this formal framework, we study some notions of honesty for services, which measure their ability to respect contracts, under different assumptions about the environment. In particular, we find conditions under which these notions are (un)decidable.
contatti | accessibilità Università degli Studi di Cagliari
C.F.: 80019600925 - P.I.: 00443370929
note legali | privacy