1,721,012 research outputs found
Software transactional memory with interactions
No full textSoftware Transactional memory (STM) is an emerging abstraction for concurrent programming alternative to lock-based synchronizations. Most STM models admit only isolated transactions, which are not adequate in multithreaded programming where transactions need to interact via shared data before committing. To overcome this limitation, in this paper we present Atomic Transactional Memory (ATM), a programming abstraction supporting safe, data-driven interactions between composable memory transactions. This is achieved by relaxing isolation between transactions, still ensuring atomicity. This model allows for loosely-coupled interactions since transaction merging is driven only by accesses to shared data, with no need to specify participants beforehand
Securing the art market with distributed public ledgers
No full textThe art market is an important scenario where many players (artists, buyers, sellers, brokers, etc.) act in a context with partial trust, and still it is crucial to ensure authentication and provenance of artworks. In this paper, we propose to store artworks information and ownership in distributed public ledgers. To this end, we present a distributed, scalable application which provides the main operations for operating on the art market. This application is composed by a back-end based on Ethereum ledger and the IPFS distributed file system, where the data is kept and manipulated by means of suitable Solidity smart contracts; and a web-based front-end. In this way, we obtain the robustness and scalability of Ethereum public ledger with the easiness of common web applications (or even mobile apps). The solution we propose could be applied to similar traceability contexts, where we have to deal with many partners with limited (or no) trust
On the Security and Safety of AbU Systems
No full textAttribute-based memory updates (AbU in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed systems, particularly suited for the IoT. It can be seen as a memory-based counterpart of attribute-based communication, keeping the simplicity of ECA rules. In this paper, we introduce behavioral equivalences for AbU, with the aim of formally defining security and safety requirements for AbU systems. As a consequence, the proposed requirements can help in assuring the security and safety of IoT devices, which are more and more pervasive in our daily life. Finally, we propose (syntactic) sufficient conditions to statically verify the introduced requirements
Some characterization results for permutation algebras
Full text linkIn recent years, many general presentations (metamodels) for calculi with name-passing, either operational or denotational in flavour, have been proposed. In this paper, we investigate the connections among some of these proposals, namely permutation algebras, named sets and sheaf categories, with the aim of establishing a bridge between different approaches to the abstract specification of nominal calculi
A Calculus for Subjective Communication
Full text linkIn this paper we introduce Subjective Communication, a new interaction model for CAS and generalizing the attribute-based communication introduced in the AbC calculus. In this model, a message is broadcasted to every process, but each process can view the very same message in different ways, depending on its attributes. To formalize this model, we introduce SCC, the Subjective Communication Calculus, for which we propose two semantics: Direct SCC, particularly useful when dealing with an edge computing communication paradigm, and Indirect SCC, more suited to a cloud-centric model. We then introduce a stateless bisimilarity for our semantics, which we prove to be a congruence
Assembling Coherent Network Topologies Using Round-Trip Graphs (short paper)
Full text linkDiscovering the network topology in computer networks is challenging due to limited communication and incomplete information about non-immediately connected nodes. In this paper we address the problem of assembling partial views obtained by discovery tools into a coherent representation, using round-trip graphs: labelled bipartite directed graphs representing the communications between hosts, interfaces, and networks. A merge operation is introduced, facilitating compositional and incremental assembly of partial views. This research provides a practical solution for incrementally constructing a comprehensive network topology
Distributed Programming of Smart Systems with Event-Condition-Action Rules
Full text linkIn recent years, event-driven programming languages, e.g. those based on Event Condition Action (ECA) rules, have emerged as a promising paradigm for implementing smart systems, such as IoT devices. Still, actual implementations are bound to a centralized infrastructure, limiting scalability and security. In this work, we present attribute-based memory updates (AbU), a new interaction mechanism aiming to extend the ECA programming paradigm to distributed systems. It relies on attribute-based communication, that is similar to broadcast, but receivers are selected “on the fly” by means of predicates over their attributes. With AbU, smart devices can be easily programmed via ECA rules and, at the same time, they can be deployed to a distributed network. Hence, a centralized infrastructure is not needed anymore: the computation is moved on the edge, improving reliability, scalability, privacy and security
DBCChecker: A Bigraph-Based Tool for Checking Security Properties of Container Compositions
Full text linkDespite their widespread application in modern systems, container composition is often complex and error-prone. In this work, we present DBCChecker, a tool aiming to verify security properties of systems obtained by composition of containers. From the configuration of a container-based system and an abstract description of the interface behaviour of each container, the tool builds a formal model of the overall system, which can be verified in ProVerif (an automatic symbolic protocol verifier), to check that the overall system satisfies the required properties. The system can be described in a specification language capable to express at once the interfaces and connections of containers and the relevant behavioural aspects of their interfaces, called JSON Bigraph Format (JBF), and inspired by previous formal models, based on bigraphs, for containerized architectures
Automated Symbolic Verification of Telegram’s MTProto 2.0
No full textMTProto 2.0 is a suite of cryptographic protocols for instant messaging at the core of the popular Telegram messenger application. In this paper we analyse MTProto 2.0 using the symbolic verifier ProVerif. We provide fully automated proofs of the soundness of MTProto 2.0’s authentication, normal chat, end-to-end encrypted chat, and rekeying mechanisms with respect to several security properties, including authentication, integrity, secrecy and perfect forward secrecy; at the same time, we discover that the rekeying protocol is vulnerable to an unknown key-share (UKS) attack. We proceed in an incremental way: each protocol is examined in isolation, relying only on the guarantees provided by the previous ones and the robustness of the basic cryptographic primitives. Our research proves the formal correctness of MTProto 2.0 w.r.t. most relevant security properties, and it can serve as a reference for implementation and analysis of clients and servers
- …
