• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE Annual Computers, Software, and Applications Conference >Developing Safe Smart Contracts
【24h】

Developing Safe Smart Contracts

机译：开发安全智能合约

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Blockchain is a shared, distributed ledger on which transactions are digitally recorded and linked together. Smart Contracts are programs running on Blockchain and are used to perform transactions in a distributed environment without need for any trusted third party. Since smart contracts are used to transfer assets between contractual parties, their safety and security are crucial and badly written and insecure contracts may result in catastrophe. Actor-based programming is known to solve several problems in building distributed software systems. Moreover, formal verification is a solid technique for developing dependable systems. In this paper, we show how the actor model can be used for modeling, analysis and synthesis of smart contracts. We propose Smart Rebeca as an extension of the actor-based language Rebeca, and use the model checking toolset Afra for verification of smart contracts. We implement a synthesizer to synthesize Solidity programs that run on the Ethereum platform from Smart Rebeca models. We examine the challenges and opportunities of our approach in modeling, formal verification, and synthesis of smart contracts using actors.
机译：区块链是一个共享的，分布式的分类帐，其上的交易被数字记录并链接在一起。智能合约是在区块链上运行的程序，用于在分布式环境中执行交易，而无需任何受信任的第三方。由于智能合约用于在合同双方之间转移资产，因此其安全性至关重要，书写不当，不安全的合约可能会导致灾难。基于Actor的编程可以解决构建分布式软件系统中的几个问题。此外，形式验证是开发可靠系统的可靠技术。在本文中，我们展示了参与者模型如何用于智能合约的建模，分析和综合。我们建议将Smart Rebeca作为基于角色的语言Rebeca的扩展，并使用模型检查工具集Afra来验证智能合约。我们实现了一个合成器，以从Smart Rebeca模型合成在以太坊平台上运行的Solidity程序。我们研究了在使用参与者进行智能合约的建模，形式验证和综合中，我们的方法所面临的挑战和机遇。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号