Showing 1–11 of 11 results for author: Neykova, R

DApps Ecosystems: Map** the Network Structure of Smart Contract Interactions

Authors: Sabrina Aufiero, Giacomo Ibba, Silvia Bartolucci, Giuseppe Destefanis, Rumyana Neykova, Marco Ortu

Abstract: In recent years, decentralized applications (dApps) built on blockchain platforms such as Ethereum and coded in languages such as Solidity, have gained attention for their potential to disrupt traditional centralized systems. Despite their rapid adoption, limited research has been conducted to understand the underlying code structure of these applications. In particular, each dApp is composed of m… ▽ More In recent years, decentralized applications (dApps) built on blockchain platforms such as Ethereum and coded in languages such as Solidity, have gained attention for their potential to disrupt traditional centralized systems. Despite their rapid adoption, limited research has been conducted to understand the underlying code structure of these applications. In particular, each dApp is composed of multiple smart contracts, each containing a number of functions that can be called to trigger a specific event, e.g., a token transfer. In this paper, we reconstruct and analyse the network of contracts and functions calls within the dApp, which is helpful to unveil vulnerabilities that can be exploited by malicious attackers. We show how decentralization is architecturally implemented, identifying common development patterns and anomalies that could influence the system's robustness and efficiency. We find a consistent network structure characterized by modular, self-sufficient contracts and a complex web of function interactions, indicating common coding practices across the blockchain community. Critically, a small number of key functions within each dApp play a pivotal role in maintaining network connectivity, making them potential targets for cyber attacks and highlighting the need for robust security measures. △ Less

Submitted 3 January, 2024; originally announced January 2024.

Comments: 28 pages, 23 figures

MindTheDApp: A Toolchain for Complex Network-Driven Structural Analysis of Ethereum-based Decentralised Applications

Authors: Giacomo Ibba, Sabrina Aufiero, Silvia Bartolucci, Rumyana Neykova, Marco Ortu, Roberto Tonelli, Giuseppe Destefanis

Abstract: This paper presents MindTheDApp, a toolchain designed specifically for the structural analysis of Ethereum-based Decentralized Applications (DApps), with a distinct focus on a complex network-driven approach. Unlike existing tools, our toolchain combines the power of ANTLR4 and Abstract Syntax Tree (AST) traversal techniques to transform the architecture and interactions within smart contracts int… ▽ More This paper presents MindTheDApp, a toolchain designed specifically for the structural analysis of Ethereum-based Decentralized Applications (DApps), with a distinct focus on a complex network-driven approach. Unlike existing tools, our toolchain combines the power of ANTLR4 and Abstract Syntax Tree (AST) traversal techniques to transform the architecture and interactions within smart contracts into a specialized bipartite graph. This enables advanced network analytics to highlight operational efficiencies within the DApp's architecture. The bipartite graph generated by the proposed tool comprises two sets of nodes: one representing smart contracts, interfaces, and libraries, and the other including functions, events, and modifiers. Edges in the graph connect functions to smart contracts they interact with, offering a granular view of interdependencies and execution flow within the DApp. This network-centric approach allows researchers and practitioners to apply complex network theory in understanding the robustness, adaptability, and intricacies of decentralized systems. Our work contributes to the enhancement of security in smart contracts by allowing the visualisation of the network, and it provides a deep understanding of the architecture and operational logic within DApps. Given the growing importance of smart contracts in the blockchain ecosystem and the emerging application of complex network theory in technology, our toolchain offers a timely contribution to both academic research and practical applications in the field of blockchain technology. △ Less

Submitted 3 October, 2023; originally announced October 2023.

Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types

Authors: Nicolas Lagaillardie, Rumyana Neykova, Nobuko Yoshida

Abstract: Communicating systems comprise diverse software components across networks. To ensure their robustness, modern programming languages such as Rust provide both strongly typed channels, whose usage is guaranteed to be affine (at most once), and cancellation operations over binary channels. For coordinating components to correctly communicate and synchronise with each other, we use the structuring me… ▽ More Communicating systems comprise diverse software components across networks. To ensure their robustness, modern programming languages such as Rust provide both strongly typed channels, whose usage is guaranteed to be affine (at most once), and cancellation operations over binary channels. For coordinating components to correctly communicate and synchronise with each other, we use the structuring mechanism from multiparty session types, extending it with affine communication channels and implicit/explicit cancellation mechanisms. This new ty** discipline, affine multiparty session types (AMPST), ensures cancellation termination of multiple, independently running components and guarantees that communication will not get stuck due to error or abrupt termination. Guided by AMPST, we implemented an automated generation tool (MultiCrusty) of Rust APIs associated with cancellation termination algorithms, by which the Rust compiler auto-detects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanism for communication, synchronisation and propagation of the notifications of cancellation for arbitrary processes. We have implemented several usecases, including popular application protocols (OAuth, SMTP), and protocols with exception handling patterns (circuit breaker, distributed logging). △ Less

Submitted 28 April, 2022; originally announced April 2022.

Comments: 48 pages, 19 figures, 3 tables, conference: ECOOP 2022, 28 corollaries/lemmas/theorems

Proceedings of the 13th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software

Authors: Marco Carbone, Rumyana Neykova

Abstract: The increasingly concurrent and parallel landscape of hardware and software infrastructures demands the exploration and understanding of a wide variety of foundational and practical ideas. The International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES) is dedicated to work in this area. The workshop offers a forum for researchers from differ… ▽ More The increasingly concurrent and parallel landscape of hardware and software infrastructures demands the exploration and understanding of a wide variety of foundational and practical ideas. The International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES) is dedicated to work in this area. The workshop offers a forum for researchers from different fields to exchange new ideas about these challenges to modern and future programming, where concurrency and distribution are the norm rather than a marginal concern. The topic is central and combines well with the main conferences of ETAPS, in particular with ESOP. △ Less

Submitted 22 March, 2022; originally announced March 2022.

Journal ref: EPTCS 356, 2022

kmclib: Automated Inference and Verification of Session Types

Authors: Keigo Imai, Julien Lange, Rumyana Neykova

Abstract: Theories and tools based on multiparty session types offer correctness guarantees for concurrent programs that communicate using message-passing. These guarantees usually come at the cost of an intrinsically top-down approach, which requires the communication behaviour of the entire program to be specified as a global type. This paper introduces kmclib: an OCaml library that supports the developme… ▽ More Theories and tools based on multiparty session types offer correctness guarantees for concurrent programs that communicate using message-passing. These guarantees usually come at the cost of an intrinsically top-down approach, which requires the communication behaviour of the entire program to be specified as a global type. This paper introduces kmclib: an OCaml library that supports the development of correct message-passing programs without having to write any types. The library utilises the meta-programming facilities of OCaml to automatically infer the session types of concurrent programs and verify their compatibility (k-MC). Well-typed programs, written with kmclib, do not lead to communication errors and cannot get stuck. △ Less

Submitted 26 November, 2021; v1 submitted 23 November, 2021; originally announced November 2021.

Comments: kmclib is available at https://github.com/keigoi/kmclib

Statically Verified Refinements for Multiparty Protocols

Authors: Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, Nobuko Yoshida

Abstract: With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a ty** discipline for message-passing concurrency, guaranteeing communication safety properties such as deadlock freedom. While originally MPST focus on the communication aspects, and employ a simple ty** system for comm… ▽ More With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a ty** discipline for message-passing concurrency, guaranteeing communication safety properties such as deadlock freedom. While originally MPST focus on the communication aspects, and employ a simple ty** system for communication payloads, communication protocols in the real world usually contain constraints on the payload. We introduce refined multiparty session types (RMPST), an extension of MPST, that express data dependent protocols via refinement types on the data types. We provide an implementation of RMPST, in a toolchain called Session*, using Scribble, a multiparty protocol description toolchain, and targeting F*, a verification-oriented functional programming language. Users can describe a protocol in Scribble and implement the endpoints in F* using refinement-typed APIs generated from the protocol. The F* compiler can then statically verify the refinements. Moreover, we use a novel approach of callback-styled API generation, providing static linearity guarantees with the inversion of control. We evaluate our approach with real world examples and show that it has little overhead compared to a naïve implementation, while guaranteeing safety properties from the underlying theory. △ Less

Submitted 14 September, 2020; originally announced September 2020.

Comments: Conditionally Accepted by OOPSLA' 20. Full version with appendix

Multiparty Session Programming with Global Protocol Combinators

Authors: Keigo Imai, Rumyana Neykova, Nobuko Yoshida, Shoji Yuen

Abstract: Multiparty Session Types (MPST) is a ty** discipline for communication protocols. It ensures the absence of communication errors and deadlocks for well-typed communicating processes. The state-of-the-art implementations of the MPST theory rely on (1) runtime linearity checks to ensure correct usage of communication channels and (2) external domain-specific languages for specifying and verifying… ▽ More Multiparty Session Types (MPST) is a ty** discipline for communication protocols. It ensures the absence of communication errors and deadlocks for well-typed communicating processes. The state-of-the-art implementations of the MPST theory rely on (1) runtime linearity checks to ensure correct usage of communication channels and (2) external domain-specific languages for specifying and verifying multiparty protocols. To overcome these limitations, we propose a library for programming with global combinators -- a set of functions for writing and verifying multiparty protocols in OCaml. Local behaviours for all processes in a protocol are inferred at once from a global combinator. We formalise global combinators and prove a sound realisability of global combinators -- a well-typed global combinator derives a set of local types, by which typed endpoint programs can ensure type and communication safety. Our approach enables fully-static verification and implementation of the whole protocol, from the protocol specification to the process implementations, to happen in the same language. We compare our implementation to untyped and continuation-passing style implementations, and demonstrate its expressiveness by implementing a plethora of protocols. We show our library can interoperate with existing libraries and services, implementing DNS (Domain Name Service) protocol and the OAuth (Open Authentication) protocol. △ Less

Submitted 23 May, 2020; v1 submitted 13 May, 2020; originally announced May 2020.

Comments: ECOOP 2020

Multiparty Session Actors

Authors: Rumyana Neykova, Nobuko Yoshida

Abstract: Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailboxes. The framework uses Scribble,… ▽ More Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailboxes. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing communication safety of the participating entities. An actor can implement multiple roles in a similar way as an object can implement multiple interfaces. Multiple roles allow for cooperative inter-concurrency in a single actor. We demonstrate our framework by designing and implementing a session actor library in Python and its runtime verification mechanism. Benchmark results demonstrate that the runtime checks induce negligible overhead. We evaluate the applicability of our verification framework to specify actor interactions by implementing twelve examples from an actor benchmark suit. △ Less

Submitted 28 March, 2017; v1 submitted 19 September, 2016; originally announced September 2016.

ACM Class: D.1; D.2; D.3; F.1.2

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 1 (March 29, 2017) lmcs:3227

Timed Runtime Monitoring for Multiparty Conversations

Authors: Rumyana Neykova, Laura Bocchi, Nobuko Yoshida

Abstract: We propose a dynamic verification framework for protocols in real-time distributed systems. The framework is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session types, developed with our industrial partners. Drawing from recent work on multiparty session types for real-time interactions, we extend Scribble with clocks, resets, and clock pre… ▽ More We propose a dynamic verification framework for protocols in real-time distributed systems. The framework is based on Scribble, a tool-chain for design and verification of choreographies based on multiparty session types, developed with our industrial partners. Drawing from recent work on multiparty session types for real-time interactions, we extend Scribble with clocks, resets, and clock predicates constraining the times in which interactions should occur. We present a timed API for Python to program distributed implementations of Scribble specifications. A dynamic verification framework ensures the safe execution of applications written with our timed API: we have implemented dedicated runtime monitors that check that each interaction occurs at a correct timing with respect to the corresponding Scribble specification. The performance of our implementation and its practicability are analysed via benchmarking. △ Less

Submitted 25 August, 2014; originally announced August 2014.

Comments: In Proceedings BEAT 2014, arXiv:1408.5564

ACM Class: verification

Journal ref: EPTCS 162, 2014, pp. 19-26

Multiparty Session Actors

Authors: Rumyana Neykova, Nobuko Yoshida

Abstract: Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailbox. The framework uses Scribble, w… ▽ More Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailbox. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing type-safety and progress of the communicating entities. An actor can implement multiple roles in a similar way as an object can implement multiple interfaces. Multiple roles allow for inter-concurrency in a single actor still preserving its progress property. We demonstrate our framework by designing and implementing a session actor library in Python and its runtime verification mechanism. △ Less

Submitted 13 June, 2014; originally announced June 2014.

Comments: In Proceedings PLACES 2014, arXiv:1406.3313

Journal ref: EPTCS 155, 2014, pp. 32-37

Session Types Go Dynamic or How to Verify Your Python Conversations

Authors: Rumyana Neykova

Abstract: This paper presents the first implementation of session types in a dynamically-typed language - Python. Communication safety of the whole system is guaranteed at runtime by monitors that check the execution traces comply with an associated protocol. Protocols are written in Scribble, a choreography description language based on multiparty session types, with addition of logic formulas for more pre… ▽ More This paper presents the first implementation of session types in a dynamically-typed language - Python. Communication safety of the whole system is guaranteed at runtime by monitors that check the execution traces comply with an associated protocol. Protocols are written in Scribble, a choreography description language based on multiparty session types, with addition of logic formulas for more precise behaviour properties. The presented framework overcomes the limitations of previous works on the session types where all endpoints should be statically typed so that they do not permit interoperability with untyped participants. The advantages, expressiveness and performance of dynamic protocol checking are demonstrated through use case and benchmarks. △ Less

Submitted 10 December, 2013; originally announced December 2013.

Comments: In Proceedings PLACES 2013, arXiv:1312.2218

Journal ref: EPTCS 137, 2013, pp. 95-102