1,721,087 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
Bitcoin metadata
No full textDataset containing the metadata extracted from OP_RETURN transactions in the first 480.000 blocks of the Bitcoin blockchai
Primitives for Contract-based Synchronization
Full text linkWe 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
Contract-Oriented Computing in CO2
No full textWe present CO2, a parametric calculus for contract-based computing in distributed systems. By abstracting from the actual contract language, our calculus generalises both the contracts-as-processes and contracts-as-formulae paradigms. The calculus features primitives for advertising contracts, for reaching agreements, and for querying the fulfilment of contracts. Coordination among participants happens via multi-party sessions, which are created once agreements are reached. We present two instances of our calculus, by modelling contracts as processes in a variant of CCS, and as formulae in a logic. We formally relate the two paradigms, through an encoding from contracts-as-formulae to contracts-as-processes which ensures that the promises deducible in the logical system are exactly those reachable by its encoding as a process. Finally, we present a coarse-grained taxonomy of possible misbehaviours in contract-oriented systems, and we illustrate them with the help of a variety of examples
Planning and Verifying Service Composition
No full textA static approach is proposed to study secure composition of services.
We extend the -calculus with primitives for selecting and
invoking services that respect given security requirements.
Security-critical code is enclosed in policy framings with a possibly
nested, local scope.
Policy framings enforce safety and liveness properties.
The actual run-time behaviour of services is over-approximated by
a type and effect system.
Types are standard, and effects include the actions with possible security
concerns --- as well as information about which services may be invoked
at run-time.
An approximation is model checked to verify policy framings within
their scopes.
This allows for removing any run-time execution monitor,
and for determining the plans driving the selection of those
services that match the security requirements on demand
Towards a linear contract logic
No full textWe introduce a linear logic for contracts. The logic (called PCLLW) extends intuitionistic linear affine logic ILLW with a contractual implication connective, along the lines of Propositional Contract Logic (PCL). A proof system for PCLLW is presented, and it is shown sound and complete with respect to a phase structure model. By exploiting the finite model property, we show that PCLLW is decidable
Constant-deposit multiparty lotteries on Bitcoin
Full text linkAn 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
Lending Petri nets
No full textWe study Lending Petri nets, an extension of Petri nets where places may carry a negative number of tokens. This allows for modeling contracts where a participant may promise to give some of her resources under the guarantee that some other resources
will eventually be obtained in exchange. We then propose an interpretation of the Horn fragment of Propositional Contract Logic
in Lending Petri nets. In particular, we show that provability in the logic corresponds to reachability of certain markings in nets,
and that proof traces correspond to ``honored'' firing sequences in nets
A Journey into Bitcoin Metadata
Full text linkBesides recording transfers of currency, the Bitcoin blockchain is being used to save metadata — i.e. arbitrary pieces of data which do not affect transfers of bitcoins. This can be done by using different techniques, and for different purposes. For instance, a growing number of protocols embed metadata in the blockchain to certify and transfer the ownership of a variety of assets beyond cryptocurrency. A point of debate in the Bitcoin community is whether metadata negatively impact on the effectiveness of Bitcoin with respect to its primary function. This paper is a systematic analysis of the usage of Bitcoin metadata over the years. We discuss all the known techniques to embed metadata in the Bitcoin blockchain; we then extract metadata, and analyse them from different angles
- …
