Abstract We introduce the probabilistic two-agent justification logic $\textsf {IPJ}$, a logic in which we can reason about agents that perform interactive proofs. In order to study the growth rate of the probabilities in $\textsf {IPJ}$, we present a new method of parametrizing $\textsf {IPJ}$ over certain negligible functions. Further, our approach leads to a new notion of zero-knowledge proofs.
Recently, Blockchain technology adoption has expanded to many application areas due to the evolution of smart contracts. However, developing smart contracts is non-trivial and challenging due to the lack of tools and expertise in this field. A promising solution to overcome this issue is to use Model-Driven Engineering (MDE), however, using models still involves a learning curve and might not be suitable for non-technical users. To tackle this challenge, chatbot or conversational interfaces can be used to assess the non-technical users to specify a smart contract in gradual and interactive manner. In this paper, we propose iContractBot, a chatbot for modeling and developing smart contracts. Moreover, we investigate how to integrate iContractBot with iContractML, a domain-specific modeling language for developing smart contracts, and instantiate intention models from the chatbot. The iContractBot framework provides a domain-specific language (DSL) based on the user intention and performs model-to-text transformation to generate the smart contract code. A smart contract use case is presented to demonstrate how iContractBot can be utilized for creating models and generating the deployment artifacts for smart contracts based on a simple conversation.
Recently, Blockchain technology adoption has expanded to many application\nareas due to the evolution of smart contracts. However, developing smart\ncontracts is non-trivial and challenging due to the lack of tools and expertise\nin this field. A promising solution to overcome this issue is to use\nModel-Driven Engineering (MDE), however, using models still involves a learning\ncurve and might not be suitable for non-technical users. To tackle this\nchallenge, chatbot or conversational interfaces can be used to assess the\nnon-technical users to specify a smart contract in gradual and interactive\nmanner.\n In this paper, we propose iContractBot, a chatbot for modeling and developing\nsmart contracts. Moreover, we investigate how to integrate iContractBot with\niContractML, a domain-specific modeling language for developing smart\ncontracts, and instantiate intention models from the chatbot. The iContractBot\nframework provides a domain-specific language (DSL) based on the user intention\nand performs model-to-text transformation to generate the smart contract code.\nA smart contract use case is presented to demonstrate how iContractBot can be\nutilized for creating models and generating the deployment artifacts for smart\ncontracts based on a simple conversation.\n
The Ethereum blockchain enables executing and recording smart contracts. The smart contracts can facilitate, verify, and implement the negotiation between multiple parties, also guaranteeing transactions without a traditional legal entity. Many tools supporting the smart contracts development in different areas are flourishing because in Ethereum blockchain valuable assets are often involved. Some of the tools help the developer to find security vulnerabilities via static and/or dynamic analysis or to reduce the Gas fees consumption. Despite the plethora of such tools, there is no tool supporting smart contracts evaluation and analysis via a graphical representation for expert developers.The paper embraces this way to facilitate the developers’ analysis activity, by proposing a graphical representation model to visualize smart contract source code. The paper makes available a tool via a web interface, which accepts the smart contract address as an input and produces a graphical representation of the smart contract as an output. The graphical representation can help developers to better understand the structure of smart contracts and share it with other developers. Moreover, some metrics, such as the relations among smart contracts, are easier to be understood via "spatial" than "tabular" representation. Indeed, representing smart contracts’ metrics via visual representation facilitates the developers, who are used to analyse the source code by directly inspecting it or using other tools that provide the metrics in a table format. Finally, the paper provides detailed data regarding a smart contract to the developers and proposes a graphical representation of the smart contracts without obscuration of details, also highlighting areas of the code that are possibly too big in size and/or too complex via a diagram displaying their connections.
今から30年以上前、会社法の強行法規性をめぐり、「会社法における契約自由」の観点から大いに議論された。会社を「契約の束」とみる企業理論が有力になり、組織や団体のもつ固有性を自明のものとせず、構成員である個人レベルから分析することを通して組織的なものの意義を捉え直すことの必要性が唱えられた。当時、会社法学においては、「会社法における契約自由」の観点から、会社法の強行法規性をめぐって大いに議論された。その後、30年以上が経過した現在、ブロックチェーン技術という現代的な様相の下で、改めて「契約と組織の交錯」する現象としてDAO（Decentralized Autonomous Organizations）が注目に値する。DAOは技術的には分散型のオープンソース・ソフトウェアでブロックチェーン上でコードに基づいて運営されるバーチャルな組織である。DAOの中核にはスマートコントラクトがあり、プログラムコードの実行によって取引が行われ、ブロックチェーンに記録されるとともに、意思決定や財産管理など組織のルールが記述される。つまり、DAOにはスマートコントラクトという契約類似の機能とガバナンスの機能が備わっている。そして、SCが従来の契約（法）や組織（法）に取って代わる機能を果たすならば、DAOは「契約法の死」や「コーポレートガバナンスの死」をもたらすものとなりうる。 本研究の一つの課題は、スマートコントラクトの法的性質を明らかにすることにある。SCは履行の自動化を実現する手段にとどまらず、「ソフトウェアの相互作用」に「意思表示の合致」を認め、SCコードを契約条項と認めうることを明らかにした。もう一つの課題が、The DAOのハッキング事件を契機として顕在化したDAOのガバナンス問題（適切なガバナンスの欠如）である。プロジェクトの価値を最大化するため、多様な主体のインセンティブをうまく調整するための設計が求められる。現段階では完全なオンチェーンガバナンス・ルールに依拠するのではなく、オフチェーンで存在する主体にDAO概念を組み込むアプローチが妥当である。 More than 30 years ago, there was much debate over the mandatory nature of corporate law from the perspective of freedom of contract in corporate law. Firm theory that viewed the company as a "nexus of contracts" gained strength, and the need to rethink the significance of organizational structure by analyzing it from the view point of individual members, instead of taking the inherent nature of organizations as self-evident. At the time, there was much debate in corporate jurisprudence regarding the mandatory nature of corporate law from the perspective of freedom of contract in corporate law. More than 30 years later, under the modern aspect of blockchain technology, DAOs (Decentralized Autonomous Organizations) deserve attention again as a phenomenon of the intersection of contract and organization. At the core of a DAO is a smart contract(cited as SC), in which transactions are executed by executing the program code and recorded in the blockchain, and the rules of the organization, such as decision-making and asset management, are programmed. In other words, DAOs are equipped with both a contract-like function and a governance function. If the SC performs a function that replaces traditional contract (law) and organization (law), the DAO could lead to the "death of contract law" or the "death of corporate governance". One of the tasks of this study is to clarify the legal nature of smart contracts: SC is not only a means to automate performance, but also a means to recognize "software interaction" with "meetings of intent" and SC code can be recognized as a legal contractual terms. Another issue is the governance problem of DAOs (a lack of proper governance), which became apparent in the wake of The DAO hacking incident. In order to maximize the value of the project, designs to successfully coordinate the incentives of various actors are required. At present stage, rather than relying on complete on-chain governance rules, an approach that incorporates the DAO concept into entities that exist off-chain is appropriate.
A well-governed DAO of DAOs can provide technological and community solutions for the evolution of the DAO ecosystem. Through its technological infrastructure designs, a DAO of DAOs can create, improve and expand well-functioning and well-governed networks of DAOs. That DAO infrastructure, in turn, improves most of the applications and uses of digital assets and decentralized commerce for the greater good of society. This article examines the core features of a possible DAO of DAOs design, its ability to expand the DAO ecosystem, and the design’s uses in business and society.
In this contribution we extend an ontology for modelling agents and their interactions, called Ontology for Agents, Systems, and Integration of Services (in short, OASIS), with conditionals and ontological smart contracts (in short, OSCs). OSCs are ontological representations of smart contracts that allow to establish responsibilities and authorizations among agents and set agreements, whereas conditionals allow one to restrict and limit agent interactions, define activation mechanisms that trigger agent actions, and define constraints and contract terms on OSCs. Conditionals and OSCs, as defined in OASIS, are applied to extend with ontological capabilities digital public ledgers such as the blockchain and smart contracts implemented on it. We will also sketch the architecture of a framework based on the OASIS definition of OSCs that exploits the Ethereum platform and the Interplanetary File System.
In this contribution we extend an ontology for modelling agents and their interactions, called Ontology for Agents, Systems, and Integration of Services (in short, OASIS), with conditionals and ontological smart contracts (in short, OSCs). OSCs are ontological representations of smart contracts that allow to establish responsibilities and authorizations among agents and set agreements, whereas conditionals allow one to restrict and limit agent interactions, define activation mechanisms that trigger agent actions, and define constraints and contract terms on OSCs. Conditionals and OSCs, as defined in OASIS, are applied to extend with ontological capabilities digital public ledgers such as the blockchain and smart contracts implemented on it. We will also sketch the architecture of a framework based on the OASIS definition of OSCs that exploits the Ethereum platform and the Interplanetary File System.
With the advancements in blockchain technology, it is possible to do business, manage supply chains, and do voting on it. Blockchain uses smart contracts for maintaining the rules and agreements between two parties. These smart contracts can be easily programmed using the Solidity programming language. Solidity is a statically typed, contract-oriented, high-level language employed for coding smart contracts. Using this, the developers can write robust, self-executing, and authoritative contracts. Solidity generates a byte code that executes on an Ethereum Virtual Machine (EVM). The solidity language is similar to other advanced languages such as C, JavaScript, and Python. It supports various libraries, complex user-defined data types, and OOP concepts like inheritance, among several other features. Some use cases of Solidity-coded smart contracts are systematic voting, auctions, and lottery. This chapter’s central focus is on clearly understanding the Solidity programming language. The need for Solidity is discussed. Its use case and implementation are addressed. Details regarding its environment setup and compilation are shown. Its important components are explained along with examples for a better understanding of syntax. By the end of this chapter, one will be familiar with Solidity and will be able to write smart contracts on it.
Sepehr Sharifi, Alireza Parvizimosaed, Daniel Amyot, Luigi Logrippo · 5 authors
Legal contracts specify the terms and conditions (in essence, requirements) that apply to business transactions. Smart contracts are software systems that monitor and control the execution of contracts to ensure compliance. This paper proposes a formal specification language for contracts, called Symboleo, where contracts consist of collections of obligations and powers that define the legal contract's compliant executions. The formal semantics of Symboleo is based on an extension of an ontology for Law and is described in terms of logical axioms on statecharts that describe the lifetimes of contracts, obligations and powers. Our proposal includes a preliminary evaluation through the specification of a real life-inspired Sale-of-Goods contract, with a prototype execution engine. We envision this language to enable formally verifying contracts to detect requirements-level issues and to generate executable smart contracts (e.g., on blockchain technology).
Giovanni Ciatto, Stefano Mariani, Alfredo Maffi, Andrea Omicini
A common use case for blockchain smart contracts (SC) is that of governing interaction amongst mutually untrusted parties, by automatically enforcing rules for interaction. However, while many contributions in the literature assess SC computational expressiveness, an evaluation of their power in terms of coordination (i.e., governing interaction) is still missing. This is why in this paper we test mainstream SC implementations by evaluating their expressive power in coordinating both inter-users and inter-SC activities. To do so, we exploit the archetypal Linda coordination model as a benchmark—a common practice in the field of coordination models and languages—by discussing to what extent mainstream blockchain technologies support its implementation. As they reveal some notable limitations (affecting, in particular, coordination between SC) we then show how Tenderfone, a custom blockchain implementation providing for a more expressive notion of SC, addresses the aforementioned limitations.
When actions by one agent force another to deviate from their agreements with a third, "victim" turns into "injurer" in the chain's subsequent steps. Should the chain's initiator be responsible only for the direct harm they cause or also bear some of the indirect losses they trigger? Through an axiomatic approach, we<br/>characterize the class of fixed-fraction rules, which strike a balance between incentives for accident prevention on the one hand and fairness in terms of how liabilities are assigned on the other. Their simple design make the rules ideal for practical implementation through smart contracts, enabling automated conflict resolution.
We propose a novel way of embedding functional smart contract languages into the Coq proof assistant using meta-programming techniques. Our framework allows for developing the meta-theory of smart contract languages using the deep embedding and provides a convenient way for reasoning about concrete contracts using the shallow embedding. The proposed approach allows to make a connection between the two embeddings in a form of a soundness theorem. As an instance of our approach we develop an embedding of the Oak smart contract language in Coq and verify several important properties of a crowdfunding contract. The developed techniques are applicable to all functional smart contract languages.
While global sourcing arrangements are highly complex and usually represent large value to the partners, little is known of the use of e-contracts or smart contracts and contract management systems to enhance the contract management process. In this paper we assess the potential of emerging technologies for global sourcing. We review current sourcing contract issues and evaluate three technologies that have been applied to enhance contracting processes. These are (1) semantic standardisation, (2) cognitive technologies and (3) smart contracts and blockchain. We discuss that each of these seem to have their merit for contract management and potentially can contribute to contract management in more complex and dynamic sourcing arrangements. The combination and configuration in which these three technologies will provide value to sourcing should be on the agenda for future research in sourcing contract management.
In this paper, we describe LUNES-Blockchain, an agent-based simulator of blockchains that is able to exploit Parallel and Distributed Simulation (PADS) techniques to offer a high level of scalability. To assess the preliminary implementation of our simulator, we provide a simplified modelling of the Bitcoin protocol and we study the effect of a security attack on the consensus protocol in which a set of malicious nodes implements a filtering denial of service (i.e. Sybil Attack). The results confirm the viability of the agent-based modelling of blockchains implemented by means of PADS.
This review presents and evaluates various formalisms for the purpose of modelling the semantics of financial derivatives contracts. The formalism proposed by Lee is selected as the best candidate among those initially reviewed. Further examination and evaluation of this formalism is done.
Intelligent Cyber-physical systems can be modelled as multi-agent systems\nwith planning capability to impart adaptivity for changing contexts. In such\nmulti-agent systems, the protocol for plan execution must result in the proper\ncompletion and ordering of actions in spite of their distributed execution.\nHowever, in untrusted scenarios, there is a possibility of agents not\nrespecting the protocol either due to faults or due to malicious reasons\nthereby resulting in plan failure. In order to prevent such situations, we\npropose to implement the execution of agents through smart contracts. This\npoints to a generic architecture seamlessly integrating intelligent\nplanning-based CPS and smart-contracts.\n