We propose a simple modelling language extending iContractML 2.0 for access control policies on smart contracts. The language supports multi-party authorisation and dynamic role-based access control (RBAC) where role members can be added or removed at runtime. Models in this language can be mapped to both Solidity and DAML in a model-driven approach to RBACs.

Issam Al-Azzoni

Al Ain University of Science, United Arab Emirates

Reiko Heckel

University of Leicester, United Kingdom

Formal verification has become increasingly crucial in ensuring the accurate and secure functioning of modern software systems. Given a specification of the desired behaviour, i.e. a contract, a program is considered to be correct when all possible executions guarantee the specification. Should the software fail to behave as expected, then a bug is present. Most existing research assumes that the bug is present in the implementation, but it is also often the case that the specified expectations are incorrect, meaning that it is the specification that must be repaired. Research and tools for providing alternative specifications that fix details missing during contract definition, considering that the implementation is correct, are scarce. In this paper, we present a preliminary tool, focused on Dafny programs, for automatic specification repair in contract programming. Given a Dafny program that fails to verify, the tool suggests corrections that repair the specification. Our approach is inspired by a technique previously proposed for another contract programming language and relies on Daikon for dynamic invariant inference. Although the tool is focused on Dafny, it makes use of specification repair techniques that are generally applicable to programming languages that support contracts. Such a tool can be valuable in various scenarios. For instance, programmers can benefit from it when they have a reference implementation and need to analyse their contract options. Similarly, in education, it can serve as an aid for students, providing hints to correct their contracts.

Alexandre Abreu

University of Porto & INESC TEC

Portugal

Nuno Macedo

University of Porto; INESC TEC

Portugal

Alexandra Mendes

Faculty of Engineering, University of Porto & INESC TEC

Portugal

A current trend in service-oriented architectures is to break coarse-grained monolith systems, encapsulating all function capabilities, down into small-scale and fine-grained microservices, which work in concert. The microservices resulting from the decomposition can be independently deployed on physically distributed machines, and an extremely challenging and complex task is to ensure that the behavior emerging from their distributed interaction is equivalent to the original monolith system. Specifically, the price to be paid for the gained distribution is that the emerging microservices interaction may exhibit not only deadlocking behavior, but also extra behavior, which is undesired with respect to the original monolith. In this paper, we propose a method for automatically (i) detecting both deadlocking interactions and extra behavior, and (ii) synthesizing distributed coordinators that when interposed among the resulting microservices avoid deadlocks and undesired interactions.

Marco Autili

University of L'Aquila, Italy

Italy

Gianluca Filippone

University of L'Aquila, Italy

Massimo Tivoli

University of L'Aquila

Italy