Browsing by Author "Pace, Gordon J."

Filter results by typing the first few letters
Now showing 1 - 3 of 3
  • No Thumbnail Available
    Item
    AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification
    (International Conference on Runtime Verification, 2022) Azzopardi, Shaun; Ellul, Joshua; Falzon, Ryan; Pace, Gordon J.
    Aspect-oriented programming tools aim to provide increased code modularity by enabling programming of cross-cutting concerns separate from the main body of code. Since the inception of runtime verification, aspect-oriented programming has regularly been touted as a perfect accompanying tool, by allowing for non-invasive monitoring instrumentation techniques. In this paper we present, AspectSol, which enables aspect-oriented programming for smart contracts written in Solidity, and then discuss the design space for pointcuts and aspects in this context. We present and evaluate practical runtime verification uses and applications of the tool.
  • No Thumbnail Available
    Item
    On the Specification and Monitoring of Timed Normative Systems
    (2022) Azzopardi, Shaun; Pace, Gordon J.; Schapachnik, Fernando; Schneider, Gerardo
    In this article we explore different issues and design choices that arise when considering how to fully embrace timed aspects in the formalisation of normative systems, e.g., by using deontic modalities, looking primarily through the lens of monitoring. We primarily focus on expressivity and computational aspects, discussing issues such as duration, superposition, conflicts, attempts, discharge, and complexity, while identifying semantic choices which arise and the challenges these pose for full monitoring of legal contracts.
  • No Thumbnail Available
    Item
    Tainting in Smart Contracts: Combining Static and Runtime Verification
    (Lecture Notes in Computer Science book series (LNCS,volume 13498), 2022) Azzopardi, Shaun; Ellul, Joshua; Falzon, Ryan; Pace, Gordon J.
    Smart contracts exist immutably on blockchains, making their pre-deployment correctness essential. Moreover, they exist openly on blockchains—open for interaction with any other smart contract and offchain entity. Interaction, for instance with off-chain oracles, can affect the state of the smart contract, and correctness of these smart contracts may depend on the trustworthiness of the data they manipulate or events they generate which, in turn, would depend on which parties or what information contributed to them. In this paper, we develop and present dynamic taint analysis techniques to enable data tainting in smart contracts. We propose an extension of Solidity that enables labelling inputs of interaction endpoints with dynamic data-carrying labels that capture actionable information about the sender. These labels can then be propagated dynamically across transactions to transitively dependent data. Specifications can then refer to such taints, for instance for ensuring that certain data could not have been influenced through interaction by a certain party. We further allow the use of taints as part of the language, affecting the control flow of the smart contract. To manage the overheads of such runtime tainting we develop sound static analysis-based techniques to prune away unnecessary instrumentation. We give a case study as a proof-of-concept, and measure the overheads associated with our additions before and after optimisation.