Papers
- How To Save Fees in Bitcoin Smart Contracts: a Simple Optimistic Off-chain Protocol
Dario Maddaloni, Riccardo Marchesin, and Roberto Zunino
6th Distributed Ledger Technologies Workshop (DLT), 2024 (to appear)
In brief: we sketch a protocol for the
off-chain execution of Bitcoin smart contracts. Normally, the on-chain
execution of such contracts requires one to pay a fee for each contract
step, potentially leading to a large number of fees to be paid.
Instead, our off-chain protocol only requires three fees to be paid
in the best case where all the participants are honest. The off-chain
protocol correctly executes the contract even when some participants
are dishonest (but more fees might be needed).
- Secure compilation of rich smart contracts on poor UTXO blockchains
Massimo Bartoletti, Riccardo Marchesin, and Roberto Zunino
IEEE European Symposium on Security and Privacy (EuroS&P), 2024 (to appear)
In brief: we propose a clause-based intermediate
language (ILLUM) for smart contracts that can be securely compiled to
the UTXO model with covenants. We also show how to compile a Solidity-like
high level language to ILLUM (also providing a reference inplementation).
- DeFi composability as MEV non-interference
Massimo Bartoletti, Riccardo Marchesin, and Roberto Zunino
Financial Cryptography (FC), 2024 (to appear)
In brief: we study a notion of smart contracts
composability based on "local MEV" (the value which can be extracted from
a contract by an adversary) and non-interference.
- Sound approximate and asymptotic probabilistic bisimulations for PCTL
Massimo Bartoletti, Maurizio Murgia, and Roberto Zunino
Logical Methods in Computer Science (LMCS), 2023
In brief: extended version of COORDINATION 2022
- A Sound Up-to-n, δ Bisimilarity for PCTL
Massimo Bartoletti, Maurizio Murgia, and Roberto Zunino
COORDINATION, 2022
In brief: we consider an approximate
semantics for PCTL where probability bounds are relaxed according to an
error parameter, and an approximate bisimulation which is similarly
relaxed according to a parameter.
We establish soundness: when a state satisfies a PCTL formula and is bisimilar
to another state, the new state satisfies the same formula (albeit with a
slightly larger error).
- Verifying liquidity of recursive Bitcoin contracts
Massimo Bartoletti, Stefano Lande, Maurizio Murgia, and Roberto Zunino
Logical Methods in Computer Science (LMCS), 2022
In brief: we study a sound verification
technique for guaranteeing liquidity of recursive BitML contracts.
- Computationally sound Bitcoin tokens
Massimo Bartoletti, Stefano Lande, and Roberto Zunino
Computer Security Foundations Symposium (CSF), 2021
In brief: we extend Bitcoin with
neighbourhood covenants, and use those to implement secure fungible tokens.
- A Formal Model of Algorand Smart Contracts
Massimo Bartoletti, Andrea Bracciali, Cristian Lepore, Alceste Scalas, and Roberto Zunino
Financial Cryptography (FC), 2021
In brief: a formal model of stateless Algorand smart contracts.
- Renegotiation and recursion in Bitcoin contracts
Massimo Bartoletti, Maurizio Murgia, and Roberto Zunino
COORDINATION, 2020
In brief: a BitML extension with consensual recusion / renegotiation; non-consensual recursion is discussed as well.
- A General Syntax for Nonrecursive Higher Inductive Types
Marco Girardi, Roberto Zunino, and Marco Benini
Italian Conference on Theoretical Computer Science (ICTCS), 2020
In brief: A formalization of a class of HITs and their induction principles.
- Bitcoin Covenants Unchained
Massimo Bartoletti, Stefano Lande, and Roberto Zunino
International Symposium on Leveraging Applications of Formal Methods (ISoLA), 2020
In brief: a model of Bitcoin covenants and a few simple examples.
- Formal Models of Bitcoin Contracts: A Survey
Massimo Bartoletti and Roberto Zunino
Frontiers in Blockchain, Vol. 2 page 8, 2019
In brief: we survey a few languages and formalisms for modelling Bitcoin contracts.
- Developing secure Bitcoin contracts with BitML
Nicola Atzei, Massimo Bartoletti, Stefano Lande, Nobuko Yoshida, and Roberto Zunino
27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2019
In brief: We present a tool for verifying Bitcoin contracts written in BitML.
- Verifying Liquidity of Bitcoin Contracts
Massimo Bartoletti and Roberto Zunino
Principles of Security and Trust (POST), 2019
In brief: we consider BitML smart contracts running on top of Bitcoin, and study several notions of liquidity. We prove liquidity decidable in BitML, through a suitable abstraction.
- Efficient Finite Difference Method for Computing Sensitivities of Biochemical Reactions
Vo Hong Thanh, Roberto Zunino, and Corrado Priami
Proceedings of the Royal Society A, Vol. 474, Issue 2218, 2018
In brief: We exploit rejection-based stochastic simulation to estimate the sensitivity of some parameters in biochemical networks.
- Fun with Bitcoin Smart Contracts
Massimo Bartoletti, Tiziana Cimoli and Roberto Zunino
International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), 2018.
In brief:
we provide a gentle introduction to Bitcoin smart contracts written in BitML.
- BitML: a calculus for Bitcoin smart contracts
Massimo Bartoletti and Roberto Zunino
ACM Conference on Computer and Communications Security (CCS), 2018.
In brief:
BitML is a simple process calculus for smart contracts which
features a computationally sound implementation on Bitcoin.
- SoK: Unraveling Bitcoin Smart Contracts
Nicola Atzei, Massimo Bartoletti, Tiziana Cimoli, Stefano Lande and Roberto Zunino
Principles of Security and Trust (POST), 2018.
In brief:
we describe several standard smart contracts in Bitcoin using
a systematic approach.
- A formal model of Bitcoin transactions
Nicola Atzei, Massimo Bartoletti, Stefano Lande and Roberto Zunino
Financial Cryptography (FC), to appear - 2018.
In brief: we present a
formal model of the Bitcoin blockchain, describing in precise terms
some of its aspects. In particular, we model the several sighashes which
Bitcoin supports, and the recently enabled Segregated Witnesses.
- Constant-deposit multiparty lotteries on Bitcoin
Massimo Bartoletti and Roberto Zunino
In Workshop on Bitcoin and Blockchain Research (BITCOIN), 2017.
In brief: we present a cryptographic
protocol which exploits the blockchain to realize a secure and fair
lottery where participants have to deposit only a constant amount of
currency. This improves from a previous protocol which required a quadratic
amount.
- Verifiable Abstractions for Contract-Oriented Systems
Massimo Bartoletti, Maurizio Murgia, Alceste Scalas and Roberto Zunino.
Journal of Logical and Algebraic Methods in Programming (JLAMP), 2017.
In brief: improved analysis w.r.t. WRLA'15,
for an extended CO2 also featuring conditionals and value-passing. Model
checking via Maude is still possible with an enhanced abstraction.
- Efficient stochastic simulation of biochemical reactions with noise and delays
Vo Hong Thanh, Roberto Zunino, and Corrado Priami
Journal of Chemical Physics (JCP), Vol. 146, Number 8, 2017
In brief: We propose a method which can improve the performance of some standard stochastic simulation algorithms. Our method focuses on the search step of these algorithms, which can be modified so to re-use some information which was already computed when the last reaction fired.
- Honesty by Typing
Massimo Bartoletti, Alceste Scalas, Emilio Tuosto and Roberto Zunino
Logical Methods in Computer Science (LMCS), Vol. 12, Issue 4, 2016.
In brief: Extended version of FORTE/FMOODS'13, featuring a simpler type system.
- Efficient Formulation of the Rejection-based Algorithm for Biochemical Reactions with Delays
Vo Hong Thanh, Roberto Zunino, and Corrado Priami
International Journal of Bioinformatics Research and Applications (IJBRA), accepted 2016, published in Vol. 15, No. 2, 2019.
In brief: Next-trial RSSA (NRSSA) is a stochastic simulation algorithm which borrows some ideas from NRM and RSSA. It improves over RSSA by requiring fewer random numbers during the simulation.
- Accelerating Rejection-based Simulation of Biochemical Reactions with Bounded Acceptance Probability
Vo Hong Thanh, Roberto Zunino, and Corrado Priami
Journal of Chemical Physics (JCP), Vol. 144, Number 22, 2016
In brief: We present a rejection-based approximate stochastic simulation algorithm, and compare it with others.
- Efficient Constant-Time Complexity Algorithm for Stochastic Simulation of Large Reaction Networks
Vo Hong Thanh, Roberto Zunino, and Corrado Priami
IEEE/ACM Transactions on Computational Biology and Bioinformatics (TCBB), Vol. 14, Issue 3, Pages 657 - 667, 2017 (first published online: 15 Feb 2016)
In brief: We study a stochastic simulation algorithm which borrows from RSSA and CR-SSA (composition-rejection).
- Contracts as Games on Event Structures
Massimo Bartoletti, Tiziana Cimoli, G. Michele Pinna and Roberto Zunino.
Journal of Logical and Algebraic Methods in Programming (JLAMP), Vol. 85, Issue 3, Pages 399–424, 2016
In brief: We relate games on event structures, the notions of agreement and protection, contracts, and session types.
- ℓ: An Imperative DSL to Stochastically Simulate Biological Systems
Roberto Zunino, Ɖurica Nikolić, Corrado Priami, Ozan Kahramanogullari and Tommaso Schiavinotto.
Chapter in Programming Languages with Applications to Biology and Security, LNCS 9465, pages 354-374, 2015
In brief: We introduce a computer language for modelling and simulating biological systems. The language is imperative, while borrowing its semantics from multiset rewriting systems.
- Compliance in Behavioural Contracts: A Brief Survey
Massimo Bartoletti, Tiziana Cimoli and Roberto Zunino.
Chapter in Programming Languages with Applications to Biology and Security, LNCS 9465, pages 103-121, 2015
In brief: We compare several compliance relations
in behavioural contracts.
- On the decidability of honesty and of its variants
Massimo Bartoletti and Roberto Zunino.
Web Services, Formal Methods and Behavioural Types (WS-FM/BEAT), 2015
In brief: We prove that honesty
(as defined in CO2) is undecidable.
- Debits and Credits in Petri Nets and Linear Logic
Massimo Bartoletti, Pierpaolo Degano, Paolo Di Giamberardino, and
Roberto Zunino.
Chapter in "Logic, Rewriting, and Concurrency", LNCS 9200, pages 135-159,
2015
In brief: we consider intuitionistic linear
logic with mix, relate it to PCL, and connect its Horn fragment with
Debit Petri Nets and their transition semantics.
- On the Rejection-based Algorithm for Simulation and Analysis of Large-Scale Reaction Networks
Vo Thanh, Corrado Priami, and Roberto Zunino.
Journal of Chemical Physics (JCP), Vol. 142, Number 24, 2015.
In brief: we further improve our RSSA algorithm,
by optimizing some crucial sub-steps. We then propose a symultaneous
variant of RSSA, which is able to (exactly) simulate many independent
trajectories more efficiently than naively simulating each of them
individually.
- Models of Circular Causality
Massimo Bartoletti, Tiziana Cimoli, G. Michele Pinna, and Roberto Zunino.
Distributed Computing and Internet Technology (ICDCIT), 2015. (invited)
- Vicious Circles in Contracts and in Logic
Massimo Bartoletti, Tiziana Cimoli, Paolo Di Giamberardino, and Roberto Zunino.
Science of Computer Programming (SCP), Vol. 109, pages 61-95, 2015.
In brief: Extended version of ICE'13.
- Choreographies in the Wild
Massimo Bartoletti, Julien Lange, Alceste Scalas, and Roberto Zunino.
Science of Computer Programming (SCP), Vol. 109, pages 36-60, 2015.
In brief: Bottom-up synthesis of a choreography,
using a multiparty variant of CO2 with asynchronous message passing.
- Efficient Rejection-based Simulation of Biochemical Reactions with Stochastic Noise and Delays
Vo Thanh, Corrado Priami, and Roberto Zunino.
Journal of Chemical Physics (JCP), Vol. 114, Number 13, 2014.
In brief: RSSA is a rejection-based simulation
algorithm for reaction networks which is faster than the standard SSA and NRM in
many cases.
- A semantic Deconstruction of Session Types
Massimo Bartoletti, Alceste Scalas and Roberto Zunino.
International Conference on Concurrency Theory (CONCUR), 2014.
In brief: We provide equivalent definitions
for some standard concepts in session types (e.g. compliance, subtyping,
progress) without referring to the syntax, and instead only relying on
the LTS semantics.
Our main tool, I/O simulation can be used for the refinement of types,
in a syntax-agnostic way.
- Modelling and Verifying Contract-Oriented Systems in Maude
Massimo Bartoletti, Maurizio Murgia, Alceste Scalas and Roberto Zunino.
International Workshop on Rewriting Logic and its Applications (WRLA), 2014.
In brief: CO2 finite-state processes
can be verified to be honest via an abstraction and model-checking.
The approach can be implemented in Maude in a simple way.
- Circular Causality in Event Structures
Massimo Bartoletti, Tiziana Cimoli, G. Michele Pinna and Roberto Zunino.
Fundamenta Informaticae (FI), Vol. 134, Number 3-4, pages 219-259, 2014.
In brief: We propose circular event structures
(CES) as a model for circular causality.
Reachability in CES is related to provability in PCL.
- Adaptive Tree-Based Search for Stochastic Simulation
Algorithm
Vo Hong Thanh and Roberto Zunino.
International Journal of Computational Biology and Drug Design, 2014 (in press).
In brief: In stochastic simulation for
reaction networks, we optimize the search for the next reaction exploiting
complete trees and Huffman trees.
- Contract Agreements via Logic
Massimo Bartoletti, Tiziana Cimoli, Paolo Di Giamberardino and Roberto Zunino.
Interaction and Concurrency Experience (ICE), 2013.
In brief: Proof traces are used to
collect the order in which atomic propositions appear in a Horn PCL
proof. Relationships are established between proof traces and reachability
and urgency in circular event structures.
- Honesty by Typing
Massimo Bartoletti, Alceste Scalas, Emilio Tuosto and Roberto Zunino.
Formal Techniques for Distributed Systems (FORTE/FMOODS), 2013.
In brief: A type system is provided to
guarantee CO2 process honest.
- A Theory of Agreements and Protection
Massimo Bartoletti, Tiziana Cimoli and Roberto Zunino.
Principles of Security and Trust (POST), 2013.
In brief: Contracts between mutually distrusting
participants are modelled using event structures. Participants in a group
agree when they have a strategy to "win", while a standalone participant
is protected when she will never "lose", not even in a malicious group.
We prove that agreement and protection are mutually exclusive in event
structures, and introduce circular event structures to reconcile them.
- An event-based model for contracts
Massimo Bartoletti, Tiziana Cimoli, G. Michele Pinna and Roberto Zunino.
Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES'12), 2013.
- Splitting for rare event simulation in biochemical systems
Vo Hong Thanh and Roberto Zunino.
SimuTools 2013.
In brief: A splitting metodology for estimating the probability of rare events in stochastic systems is proposed.
- A Rule-Based and Imperative Language for Biochemical Modeling and Simulation
Đurica Nikolić, Corrado Priami and Roberto Zunino.
Software Engineering and Formal Methods (SEFM), 2012. (invited)
In brief: An imperative, graph-modifying
language is proposed to model biochemical systems.
- Contract-Oriented Computing in CO2
Massimo Bartoletti, Emilio Tuosto and Roberto Zunino.
Scientific Annals of Computer Science (SACS), Vol. 22, Issue 1, 2012.
In brief: We study several variants
of CO2 using different contract models.
- On Computation and Synchronization Costs in Spatial Distributed Simulation
Roberto Zunino.
Journal of Simulation (JOS), Vol. 6, Issue 3, 2012.
In brief: Extended version of PADS'11,
also incuding experimental results.
- On the Realizability of Contracts in Dishonest Systems
Massimo Bartoletti, Emilio Tuosto and Roberto Zunino.
COORDINATION, 2012.
In brief: In the CO2 process calculus,
a participant can promise some behaviour through a "contract", and
then maliciously break her promise. This departs from most approaches
to behavioural types, which assume a sort of angelic behaviour, aiming
to bring such approahces closer to the real world which is plagued by
security issues.
We focus on the detection of misbehaving participants and
the property of honesty, guaranteeing that promises are always respected
in all contexts.
- Model Checking Usage Policies
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari and Roberto Zunino.
Mathematical Structures in Computer Science (MSCS), Volume 25, Issue 03, 2015, pages 710-763 (Submitted Jan 2011, Accepted after revision Nov 2011, Published online Nov 2014, Printed March 2015).
- An Imperative Language of Self-modifying Graphs for Biological Systems
Corrado Priami, Paola Quaglia and Roberto Zunino.
ACM Symposium on Applied Computing (SAC), 2012.
- Tree-Based Search for Stochastic Simulation Algorithm
Vo Hong Thanh and Roberto Zunino.
ACM Symposium on Applied Computing (SAC), 2012. (poster paper)
- Tools and Verification
Massimo Bartoletti, Luis Caires, Ivan Lanese, Franco Mazzanti, Davide Sangiorgi, Hugo Torres Vieira and Roberto Zunino.
Chapter in Results of the SENSORIA Project, 2011.
- Call-by-Contract for Service Discovery, Orchestration and Recovery
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari and Roberto Zunino.
Chapter in Results of the SENSORIA Project, 2011.
- Trading Computation Time for Synchronization Time in Spatial Distributed Simulation
Roberto Zunino.
25th ACM/IEEE/SCS Workshop on Principles of Advanced and Distributed Simulation (PADS), 2011.
- Contracts in Distributed Systems
Massimo Bartoletti, Emilio Tuosto and Roberto Zunino.
Interaction and Concurrency Experience (ICE), 2011.
-
Static Enforcement of Service Deadlines
Massimo Bartoletti and Roberto Zunino.
IEEE International Conference on Software Engineering and Formal Methods (SEFM), 2010.
- Primitives for Contract-based Synchronization
Massimo Bartoletti and Roberto Zunino.
Interaction and Concurrency Experience (ICE), 2010.
- A Calculus of Contracting Processes
Massimo Bartoletti and Roberto Zunino.
Logic in Computer Science (LICS), 2010.
-
Security Issues in Contract-based Computing
Massimo Bartoletti and Roberto Zunino.
Formal Aspects of Security and Trust (FAST), 2009.
-
Local Policies for Resource Usage Analysis
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari and Roberto Zunino.
ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 31, Issue 6, 2009.
-
nu-types for Effects and Freshness Analysis
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari and Roberto Zunino.
International Colloquium on Theoretical Aspects of Computing (ICTAC), 2009.
-
Securing Java with Local Policies
Massimo Bartoletti, Gabriele Costa, Pierpaolo Degano, Fabio Martinelli and Roberto Zunino.
Journal of Object Technology, Vol. 8, No. 4, 2009.
-
Jalapa: Securing Java with Local Policies
Massimo Bartoletti, Gabriele Costa and Roberto Zunino.
BYTECODE, 2009.
-
Model Checking Usage Policies
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari and Roberto Zunino.
Trustworthy Global Computing (TGC), 2008.
-
Semantics-based Design for Secure Web Services
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari and Roberto Zunino.
IEEE Transactions on Software Engineering, Vol. 34, Issue 1, 2008.
-
LocUsT: a Tool for Model Checking Usage Policies
Massimo Bartoletti and Roberto Zunino.
-
L’orientamento ai servizi.
Massimo Bartoletti, Vincenzo Ciancia, Gian Luigi Ferrari, Roberto Guanciale, Daniele Strollo and Roberto Zunino.
Mondo Digitale, Issue 25, 2008.
-
Securing Java with Local Policies
Massimo Bartoletti, Gabriele Costa, Pierpaolo Degano, Gian Luigi Ferrari, Fabio Martinelli and Roberto Zunino.
Workshop on Formal Techniques for Java-like Programs, 2008.
-
Certificates for Tree Automata Completion
Roberto Zunino.
FCS-ARSPA-WITS, 2008.
-
Hard Life with Weak Binders
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari and Roberto Zunino.
EXPRESS, 2008.
-
Secure Service Orchestration
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari and Roberto Zunino.
FOSAD 2007
-
Types and Effects for Resource Usage Analysis
Massimo Bartoletti, Pierpaolo Degano, Gian Luigi Ferrari and Roberto Zunino.
Foundations of Software Science and Computation Structures (FOSSACS), 2007.
-
Handling exp, × (and Timestamps) in Protocol Analysis
Roberto Zunino and Pierpaolo Degano.
Foundations of Software Science and Computation Structures (FOSSACS), 2006.
-
Defending the Bank with a Static Analysis
Roberto Zunino.
Nordic Conference on Secure IT Systems (NordSec), 2006.
-
Weakening the Perfect Encryption Assumption in Dolev-Yao Adversaries
Roberto Zunino and Pierpaolo Degano.
Theoretical Computer Science 340(1), pages 154-178, 2005
-
Finite Approximation of Terms up to Rewriting
Roberto Zunino and Pierpaolo Degano.
Manuscript, 2005
-
A Note on the Perfect Encryption Assumption in a Process Calculus
Roberto Zunino and Pierpaolo Degano.
Foundations of Software Science and Computation Structures (FOSSACS), 2004.
-
Control Flow Analysis for the Applied Pi-calculus
Roberto Zunino.
ENTCS 99, pages 87-110, 2004.
Home
Roberto Zunino, 2021