1,987 research outputs found
Usage automata
No full textUsage automata are an extension of finite stata automata,
with some additional features (e.g.\ parameters and guards)
that improve their expressivity.
Usage automata are expressive enough to model security requirements
of real-world applications;
at the same time, they are simple enough to be statically amenable,
e.g.\ they can be model-checked against abstractions of program usages.
We study here some foundational aspects of usage automata.
In particular, we discuss about their expressive power, and about their
effective use in run-time mechanisms for enforcing usage policies
Il carteggio Maas-Bartoletti (1948-1949) [con M. Losacco e R. Otranto]
No full textÈ pubblicata e commentata la corrispondenza scientifica tra Paul Maas e Vittorio Bartoletti relativa all'edizione delle "Elleniche di Ossirinco", testo storiografico greco frammentario del IV secolo a.C. recuperato grazie a una scoperta papirologica.The scholarly correspondence between Paul Maas and Vittorio Bartoletti concerning the edition of the "Hellenica Oxyrhynchia" (a fragmentary historical text of the 4th cent. BCE edited from a papyrus) is published here with a commentary
Primitives for Contract-based Synchronization
No full textWe investigate how contracts can be used to regulate the interaction between processes. To do that, we study a variant of the concurrent constraints calculus presented in [1], featuring primitives for multi-party synchronization via contracts. We proceed in two directions. First, we exploit our primitives to model some contract-based interactions. Then, we discuss how several models for concurrency can be expressed through our primitives. In particular, we encode the pi-calculus and graph rewriting
MEV-Freedom, in DeFi and Beyond (Invited Talk)
No full textMaximal Extractable Value (MEV) refers to a class of recent attacks on public blockchains, where adversaries with the power to reorder, drop or insert transactions in a block can "extract" value from user transactions in the mempool. Empirical research has shown that mainstream DeFi protocols, like e.g. Automated Market Makers and Lending Pools, are massively targeted by MEV attacks. This has detrimental effects on their users, on transaction fees, and on the congestion of blockchain networks. Despite the growing knowledge on MEV attacks on blockchain protocols, an exact definition is still missing. Indeed, formally defining these attacks is an essential prerequisite to the design of provably secure, MEV-free blockchain protocols. In this talk, we propose a formal definition of MEV, based on a general, abstract model of blockchains and smart contracts. We then introduce MEV-freedom, a property enjoyed by contracts resistant to MEV attacks. We validate this notion by rigorously proving that Automated Market Makers and Lending Pools are not MEV-free. We finally discuss how to design MEV-free contracts
Il carteggio Maas-Bartoletti (1948-1949)
No full textEdizione della corrispondenza fra Paul Maas e Vittorio Bartoletti in merito al lavoro di edizione, da parte di quest'ultimo, dei frammenti fiorentini (PSI 1304) delle «Elleniche di Ossirinco» (in collaborazione con Rosa Otranto e P. Massimo Pinto, ai quali si debbono le pp. 215-256). Il carteggio ha inizio con l'invio dell'estratto a Paul Maas da parte di Vittorio Bartoletti (20 settembre 1948). Denso di congetture, ripensamenti, correzioni, riflessioni critico-testuali, esso costituisce uno strumento essenziale per la comprensione della genesi e dell'allestimento del testo critico delle «Elleniche di Ossirinco»
Constant-deposit multiparty lotteries on Bitcoin
No full textAn active research trend is to exploit the consensus mechanism of cryptocurrencies to secure the execution of distributed applications. In particular, some recent works have proposed fair lotteries which work on Bitcoin. These protocols, however, require a deposit from each player which grows quadratically with the number of players. We propose a fair lottery on Bitcoin which only requires a constant deposit
An analysis of bitcoin OP_RETURN metadata
No full textThe Bitcoin protocol allows to save arbitrary data on the blockchain through a special instruction of the scripting language, called OP_RETURN. A growing number of protocols exploit this feature to extend the range of applications of the Bitcoin blockchain beyond transfer of currency. A point of debate in the Bitcoin community is whether loading data through OP_RETURN can negatively affect the performance of the Bitcoin network with respect to its primary goal. This paper is an empirical study of the usage of OP_RETURN over the years. We identify several protocols based on OP_RETURN, which we classify by their application domain. We measure the evolution in time of the usage of each protocol, the distribution of OP_RETURN transactions by application domain, and their space consumption
Static Enforcement of Service Deadlines
No full textWe consider the problem of statically deciding when a service always provides its functionality within a given amount of time. In a timed pi-calculus, we propose a two-phases static analysis guaranteeing that processes enjoy both the maximal progress and the well-timedness properties. Exploiting this analysis, we devise a decision procedure for checking service deadlines
An empirical analysis of smart contracts: platforms, applications, and design patterns
No full textSmart contracts are computer programs that can be consistently executed by a network of mutually distrusting nodes, without the arbitration of a trusted authority. Because of their resilience to tampering, smart contracts are appealing in many scenarios, especially in those which require transfers of money to respect certain agreed rules (like in financial services and in games). Over the last few years many platforms for smart contracts have been proposed, and some of them have been actually implemented and used. We study how the notion of smart contract is interpreted in some of these platforms. Focussing on the two most widespread ones, Bitcoin and Ethereum, we quantify the usage of smart contracts in relation to their application domain. We also analyse the most common programming patterns in Ethereum, where the source code of smart contracts is available
- …
