1,721,010 research outputs found
Enforcing Determinism of Java Smart Contracts
No full textJava is a high-level, well-known and powerful object-oriented language, with a large support library and a comfortable toolbelt. Hence, it has been proposed for writing smart contracts in blockchain. However, its support library is non-deterministic, which is a blocking issue for its application to smart contracts. This paper discusses the kind of (non-)determinism of the methods of the Java library and how a deterministic fragment of that library can be specified. It shows that some relevant parts are deterministic only under specific conditions on run-time values. It concludes with the description of an instrumentation, for the Takamaka blockchain, that enforces such conditions, statically or dynamically, reporting experiments with its implementation
Software verification challenges in the blockchain ecosystem
Full text linkBlockchain technology has created a new software development context, with its own peculiarities, mainly due to the guarantees that the technology must satisfy, that is, immutability, distributability, and decentralization of data. Its rapid evolution over the last decade implied a lack of adequate verification tools, exposing developers and users to critical vulnerabilities and bugs. This paper clarifies the extent of block chain-oriented software (BoS), that goes well beyond smart contracts. Moreover, it provides an overview of the challenges related to software verification in the blockchain context, encompassing smart contracts, blockchain layers, cross-chain applications, and, more generally, BoS. This study aims to highlight the shortcomings of the state-of-art and of the state-of-practice of software verification in that context and identify, at the same time, new research directions
Blockchain-Based Multirole Authentication and Authorization in Smart Contracts with a Hierarchical Factory Pattern
No full textThe recent spread of smart contracts in several application domains presents challenges in scalability, efficiency, management, and security. In this regard, some design patterns have been proposed to factorize common parts, prevent replicated deployment by promoting reusability, and apply some role-based access control (RBAC) techniques during smart contract execution. In particular, the factory pattern has been widely recognized as a common practice to solve the scalability issue, reducing also the increased gas costs related to both smart contract deployment and its subsequent use. However, in real-world applications, the factory pattern can be considered too limited since it only allows the instantiation of a single type or family of contracts. On the other side, no solutions have been proposed that tightly integrate a factory pattern with RBAC functionalities. In this paper, we propose an extension of the factory pattern, called the hierarchical factory pattern, which integrates a multirole authentication and authorization mechanism tailored explicitly to this pattern since it allows a secure, efficient, and role-specific interaction between the various layers of the hierarchy. The paper ends with some considerations about performance and scalability
An application layer with protocol-based java smart contract verification
Full text linkSmart contracts are software that runs in blockchain and expresses the rules of an agreement between parties. An incorrect smart contract might allow blockchain users to violate its rules and even jeopardize its expected security. Smart contracts cannot be easily replaced to patch a bug since the nature of contracts requires them to be immutable. More problems occur when a smart contract is written in a general-purpose language, such as Java, whose executions, in a blockchain, could hang the network, break consensus or violate data encapsulation. To limit these problems, there exist automatic static analyzers that find bugs before smart contracts are installed in the blockchain. This so-called off-chain verification is optional because programmers are not forced to use it. This paper presents a general framework for the verification of smart contracts, instead, that is part of the protocol of the nodes and applies when the code of the smart contracts gets installed. It is a mandatory entry filter that bans code that does not abide by the verification rules. Consequently, such rules become part of the consensus rules of the blockchain. Therefore, an improvement in the verification protocol entails a consensus update of the network. This paper describes an implementation of a smart contracts application layer with protocol-based verification for smart contracts written in the Takamaka subset of Java, that filters only those smart contracts whose execution in blockchain is not dangerous. This application layer runs on top of a consensus engine such as Tendermint and its derivatives Ignite and CometBFT (proof of stake), or Mokamint (proof of space). This paper provides examples of actual implementations of verification rules that check if the smart contracts satisfy some constraints required by the Takamaka language. This paper shows that protocol-based verification works and reports how consensus updates are implemented. It shows actual experiments as well as limits to its use, mainly related to the fact that protocol-based verification must be fast and its complexity must never explode, or otherwise, it would compromise the performance of the blockchain network
Adaptive Multi-Factor Scoring in Shared Blob for Improving Data Availability in Layer 2 Blockchains
No full textLayer 2 (L2) solutions have recently been developed with the aim of increasing scalability and throughput of traditional blockchain networks such as Bitcoin and Ethereum. The main idea of L2 is to move expensive computations out of the main (L1) network and post back only a summary of the performed transactions. This allows L2 solutions to inherit the security and trustworthiness of L1 while reducing computation and transaction costs. However, data availability, namely the possibility for all blockchain participants to access the data processed outside L1 to verify state transitions independently, is a challenge in L2 solutions. Namely, while on-chain data availability approaches suffer from high costs and long waiting times, off-chain approaches can pose data security risks. This paper takes into consideration the recent introduction of the blob data structure and proposes an Adaptive Multi-Factor Scoring (AMFS) to efficiently manage blobs while dynamically optimizing cost and waiting time. The proposed solution ensures low waiting times and blob posting costs, particularly for small rollups, by implementing the concept of shared blob, maintaining security without compromising performance
Confronto tra sistemi di rilevamento del gesto basati su sensori a infrarossi o ultrasuoni per applicazioni di pianoforte virtuale
Full text linkPresentiamo una tastiera virtuale che mira a sostituire quella del pianoforte con dei tasti in realtà aumentata. Lo sforzo maggiore è stato compiuto nel rilevamento accurato nonché rapido dei movimenti delle mani. Per raggiungere questo obiettivo sono stati confrontati un dispositivo di rilevamento a infrarossi ed uno a ultrasuoni, valutandone pro e contro nell’impiego specifico. Abbiamo poi realizzato un sistema di feedback multimodale riprendendo le azioni delle mani dell’esecutore mediante la fotocamera posteriore di un comune dispositivo mobile, e presentandole all’utente unite alla visualizzazione di una tastiera di pianoforte animata. Connettendo il dispositivo Leap Motion, responsabile del rilevamento a infrarossi, e altri dispositivi hardware per la generazione di stimoli audio e vibrotattili, il prototipo promette potenziali applicazioni come interfaccia musicale mobile a basso costo, trasformando un comune tavolo in uno scenario di realtà aumentata dove possono essere eseguiti semplici esercizi con buona accuratezza e una risposta realistica in assenza di una tastiera reale
MichelsonLiSA: A Static Analyzer for Tezos
No full textSmart contracts are immutable code deployed in a blockchain, whose execution modifies its global state. Code im-mutability leads to immutable bugs. To prevent such bugs, static program analysis infers information about the behavior of the code, statically, before code execution and deployment. This paper introduces MichelsonLiSA, a static analyzer based on abstract interpretation for the verification of smart contracts written in the Michelson low-level language of the Tezos blockchain. It applies MichelsonLiSA to the identification of security issues arising from cross-contract invocations
Intents Analysis of Android Apps for Confidentiality Leakage Detection
No full textIntents are Android’s intra- and inter-application communication mechanism. They specify an action to perform, with extra data, and are sent to a receiver component or broadcast to many components. Components, in the same or in a distinct app, receive the intent if they are available to perform the desired action. Hence, a sound static analyzer must be aware of information flows through intents. That can be achieved by considering intents as both source (when reading) and sink (when writing) of confidential data. But this is overly conservative if the intent stays inside the same app or if the set of apps installed on the device is known in advance. In such cases, a sound approximation of the flow of intents leads to a more precise analysis. This work describes SDLI, a novel static analyzer that, for each app, creates an XML summary file reporting a description of the tainted information in outwards intents and of the intents the app is available to serve. SDLI discovers confidential information leaks when two apps communicate, by matching their XML summaries, looking for tainted outwards intents of the first app that can be inwards intents of the second app. The tool is implemented inside Julia, an industrial static analyzer. On the DroidBench test cases, its shows a precision higher than 75%. On some popular apps from the Google Play marketplace, it spots inter-apps leaks of confidential data, hence showing its practical effectiveness
Static analysis for discovering IoT vulnerabilities
Full text linkThe Open Web Application Security Project (OWASP), released the “OWASP Top 10 Internet of Things 2018” list of the high-priority security vulnerabilities for IoT systems. The diversity of these vulnerabilities poses a great challenge toward development of a robust solution for their detection and mitigation. In this paper, we discuss the relationship between these vulnerabilities and the ones listed by OWASP Top 10 (focused on Web applications rather than IoT systems), how these vulnerabilities can actually be exploited, and in which cases static analysis can help in preventing them. Then, we present an extension of an industrial analyzer (Julia) that already covers five out of the top seven vulnerabilities of OWASP Top 10, and we discuss which IoT Top 10 vulnerabilities might be detected by the existing analyses or their extension. The experimental results present the application of some existing Julia’s analyses and their extension to IoT systems, showing its effectiveness of the analysis of some representative case studies
On-Chain Smart Contract Verification over Tendermint
Full text linkSmart contracts are computer code that runs in blockchain and expresses the rules of an agreement among parties. A bug in their code has major consequences, such as rule violations and security attacks. Smart contracts are immutable and cannot be easily replaced to patch a bug. To overcome these problems, there exist automatic static analyzers that find bugs before smart contracts are installed in blockchain. However, this off-chain verification is optional: programmers are not forced to use it. This paper defines on-chain verification instead, that occurs inside the same blockchain nodes, when the code of smart contracts is installed. It acts as a mandatory entry filter that bans code that does not abide to the verification rules, that are consequently part of the consensus rules of the blockchain. Thus, an improvement in on-chain verification entails a consensus update of the network. This paper provides an implementation of on-chain verification for smart contracts written in the Takamaka subset of Java, running as a Tendermint application. It shows that on-chain verification works, reporting actual experiments
- …
