-
Mechanizing Refinement Types (extended)
Authors:
Michael Borkowski,
Niki Vazou,
Ranjit Jhala
Abstract:
Practical checkers based on refinement types use the combination of implicit semantic sub-ty** and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal meta-theoretic accounting of the soundness of refinement type systems using this combination has proved elusive. We present λ_RF a core refinement calculus…
▽ More
Practical checkers based on refinement types use the combination of implicit semantic sub-ty** and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a formal meta-theoretic accounting of the soundness of refinement type systems using this combination has proved elusive. We present λ_RF a core refinement calculus that combines semantic sub-ty** and parametric polymorphism. We develop a meta-theory for this calculus and prove soundness of the type system. Finally, we give a full mechanization of our meta-theory using the refinement-type based LiquidHaskell as a proof checker, showing how refinements can be used for mechanization.
△ Less
Submitted 12 July, 2022;
originally announced July 2022.
-
Towards Cross-Blockchain Smart Contracts
Authors:
Markus Nissl,
Emanuel Sallinger,
Stefan Schulte,
Michael Borkowski
Abstract:
In recent years, manifold blockchain protocols have been proposed by researchers and industrial companies alike. This has led to a very heterogeneous blockchain landscape. Accordingly, it would be desirable if blockchains could interact with each other. However, current blockchain technologies offer only limited support for interoperability, thus preventing tokens or smart contracts from leaving t…
▽ More
In recent years, manifold blockchain protocols have been proposed by researchers and industrial companies alike. This has led to a very heterogeneous blockchain landscape. Accordingly, it would be desirable if blockchains could interact with each other. However, current blockchain technologies offer only limited support for interoperability, thus preventing tokens or smart contracts from leaving the scope of a particular blockchain.
As a first step towards a solution for cross-chain smart contract interactions, we introduce a framework which allows to invoke a smart contract from another blockchain. We offer support for continuing a smart contract after receiving a result from a different blockchain, and for calling smart contracts recursively across blockchains. We provide a reference implementation for Ethereum-based blockchains using Solidity and evaluate the performance regarding time and cost overheads.
△ Less
Submitted 28 June, 2021; v1 submitted 14 October, 2020;
originally announced October 2020.
-
A Framework for Blockchain Interoperability and Runtime Selection
Authors:
Philipp Frauenthaler,
Michael Borkowski,
Stefan Schulte
Abstract:
The suitability of a particular blockchain for a given use case depends mainly on the blockchain's functional and non-functional properties. Such properties may vary over time, and thus, a selected blockchain may become unsuitable for a given use case. This uncertainty may hinder the widespread adoption of blockchain technologies in general. To mitigate the impact of volatile blockchain properties…
▽ More
The suitability of a particular blockchain for a given use case depends mainly on the blockchain's functional and non-functional properties. Such properties may vary over time, and thus, a selected blockchain may become unsuitable for a given use case. This uncertainty may hinder the widespread adoption of blockchain technologies in general. To mitigate the impact of volatile blockchain properties, we propose a framework that monitors several blockchains, allows the user to define functional and non-functional requirements, determines the most appropriate blockchain, and enables the switchover to that chain at runtime. Our evaluation using a reference implementation shows that switching to another blockchain can save cost and enable users to benefit from better performance and a higher level of trust.
△ Less
Submitted 15 May, 2019;
originally announced May 2019.
-
Blockchain-based Data Provenance for the Internet of Things
Authors:
Marten Sigwart,
Michael Borkowski,
Marco Peise,
Stefan Schulte,
Stefan Tai
Abstract:
As more and more applications and services depend on data collected and provided by Internet of Things (IoT) devices, it is of importance that such data can be trusted. Data provenance solutions together with blockchain technology are one way to make data more trustworthy. However, current solutions do not address the heterogeneous nature of IoT applications and their data. In this work, we identi…
▽ More
As more and more applications and services depend on data collected and provided by Internet of Things (IoT) devices, it is of importance that such data can be trusted. Data provenance solutions together with blockchain technology are one way to make data more trustworthy. However, current solutions do not address the heterogeneous nature of IoT applications and their data. In this work, we identify functional and non-functional requirements for a generic IoT data provenance framework, and conceptualise the framework as a layered architecture. Using a proof-of-concept implementation based on Ethereum smart contracts, data provenance can be realised for a wide range of IoT use cases. Benefits of a generic framework include simplified adoption and a more rapid implementation of data provenance for the IoT.
△ Less
Submitted 6 August, 2019; v1 submitted 15 May, 2019;
originally announced May 2019.
-
DeXTT: Deterministic Cross-Blockchain Token Transfers
Authors:
Michael Borkowski,
Marten Sigwart,
Philipp Frauenthaler,
Taneli Hukkinen,
Stefan Schulte
Abstract:
Current blockchain technologies provide very limited interoperability. Restrictions with regards to asset transfers and data exchange between different blockchains reduce usability and comfort for users, and hinder novel developments within the blockchain space.
As a first step towards cross-blockchain interoperability, we propose the DeXTT cross-blockchain transfer protocol, which can be used t…
▽ More
Current blockchain technologies provide very limited interoperability. Restrictions with regards to asset transfers and data exchange between different blockchains reduce usability and comfort for users, and hinder novel developments within the blockchain space.
As a first step towards cross-blockchain interoperability, we propose the DeXTT cross-blockchain transfer protocol, which can be used to transfer a token on any number of blockchains simultaneously in a decentralized manner. We provide a reference implementation using Solidity, and evaluate its performance. We show logarithmic scalability of DeXTT with respect to the number of participating nodes, and analyze cost requirements of the transferred tokens.
△ Less
Submitted 15 May, 2019;
originally announced May 2019.
-
Event-based Failure Prediction in Distributed Business Processes
Authors:
Michael Borkowski,
Walid Fdhila,
Matteo Nardelli,
Stefanie Rinderle-Ma,
Stefan Schulte
Abstract:
Traditionally, research in Business Process Management has put a strong focus on centralized and intra-organizational processes. However, today's business processes are increasingly distributed, deviating from a centralized layout, and therefore calling for novel methodologies of detecting and responding to unforeseen events, such as errors occurring during process runtime. In this article, we dem…
▽ More
Traditionally, research in Business Process Management has put a strong focus on centralized and intra-organizational processes. However, today's business processes are increasingly distributed, deviating from a centralized layout, and therefore calling for novel methodologies of detecting and responding to unforeseen events, such as errors occurring during process runtime. In this article, we demonstrate how to employ event-based failure prediction in business processes. This approach allows to make use of the best of both traditional Business Process Management Systems and event-based systems. Our approach employs machine learning techniques and considers various types of events. We evaluate our solution using two business process data sets, including one from a real-world event log, and show that we are able to detect errors and predict failures with high accuracy.
△ Less
Submitted 9 January, 2018; v1 submitted 22 December, 2017;
originally announced December 2017.
