Secure Smart Contracts with Isabelle/Solidity
使用 Isabelle/Solidity 保护智能合约
基本信息
- 批准号:EP/X027619/1
- 负责人:
- 金额:$ 31.58万
- 依托单位:
- 依托单位国家:英国
- 项目类别:Research Grant
- 财政年份:2024
- 资助国家:英国
- 起止时间:2024 至 无数据
- 项目状态:未结题
- 来源:
- 关键词:
项目摘要
Smart contracts are digital contracts stored on a blockchain that are automatically executed when predetermined terms and conditions are met.They are often used to automate financial transactions and thus they hold great potential to transform and disrupt the financial industry.In particular it is estimated that blockchain and smart contracts can add up to $72.2B to the UK's GDP by 2030 and create up to 700,000 new jobs by 2030.Technically, smart contracts are programs and as such, they may contain bugs.However, since smart contracts are often used to automate financial transactions, exploiting these bugs may result in huge financial damages.In 2016, for example, a vulnerability in a smart contract was exploited, resulting in a loss of approximately $60M.More recently, hackers had exploited a vulnerability in a smart contract to steal $600M.In general, it is estimated that since 2019, more than $5B were lost due to vulnerabilities in smart contracts.This threatens society's trust in smart contracts and thus limits their potential for the development of FinTech, one of the most promising sectors for the UK economy.Unfortunately, however, even rigorous testing and auditing cannot guarantee that a smart contract does what it is supposed to do.In the best case scenario, vulnerabilities can be found with these techniques but they can never guarantee their absence.Thus, with this project, we will develop tools and techniques to support the verification of smart contracts to achieve the highest degree of reliability.Finally, we will engage in training next generation experts in the verification of smart contracts by hosting a summer school on formal methods for blockchains in Exeter.
智能合约是存储在区块链上的数字合约,当满足预定的条款和条件时,这些合约会自动执行。它们通常用于自动化金融交易,因此它们具有巨大的潜力来改变和颠覆金融行业。特别是据估计,到2030年,区块链和智能合约可以为英国的GDP增加722亿美元,并创造700亿英镑的收入。从技术上讲,智能合约是程序,因此,它们可能包含错误。然而,由于智能合约通常用于自动化金融交易,利用这些错误可能会导致巨大的财务损失。例如,在2016年,智能合约中的漏洞被利用,导致大约6000万美元的损失。最近,黑客利用智能合约中的漏洞窃取了6亿美元。总体而言,据估计,自2019年以来,由于智能合约中的漏洞而造成的损失超过50亿美元。这威胁到社会对智能合约的信任,从而限制了其对金融科技发展的潜力,英国经济最有前途的部门之一。然而,不幸的是,即使是严格的测试和审计也不能保证智能合约做它应该做的事情。在最好的情况下,这些技术可以发现漏洞,但它们永远不能保证它们的存在。因此,通过这个项目,我们将开发工具和技术来支持智能合约的验证,以实现最高程度的可靠性。最后,我们将通过在埃克塞特举办关于区块链正式方法的暑期学校,参与培训下一代智能合约验证专家。
项目成果
期刊论文数量(0)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
数据更新时间:{{ journalArticles.updateTime }}
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
数据更新时间:{{ journalArticles.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ monograph.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ sciAawards.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ conferencePapers.updateTime }}
{{ item.title }}
- 作者:
{{ item.author }}
数据更新时间:{{ patent.updateTime }}
Diego Marmsoler其他文献
Modeling Adaptive Self-healing Systems
自适应自我修复系统建模
- DOI:
10.48550/arxiv.2304.12773 - 发表时间:
2023 - 期刊:
- 影响因子:0
- 作者:
Habtom Kahsay Gidey;Diego Marmsoler;Dominik Ascher - 通讯作者:
Dominik Ascher
Strategic logics for collaborative embedded systems
协作嵌入式系统的战略逻辑
- DOI:
- 发表时间:
2019 - 期刊:
- 影响因子:2.4
- 作者:
Damian Kurpiewski;Diego Marmsoler - 通讯作者:
Diego Marmsoler
Signature : Sorts , Function , and Predicate Symbols Datatype Specification Interface Specification Architecture Constraint Specification
签名:排序、函数和谓词符号数据类型规范接口规范体系结构约束规范
- DOI:
- 发表时间:
2017 - 期刊:
- 影响因子:0
- 作者:
Diego Marmsoler;Silvio Degenhardt - 通讯作者:
Silvio Degenhardt
Towards Verified Blockchain Architectures: A Case Study on Interactive Architecture Verification
- DOI:
10.1007/978-3-030-21759-4_12 - 发表时间:
2019-06 - 期刊:
- 影响因子:0
- 作者:
Diego Marmsoler - 通讯作者:
Diego Marmsoler
Grounded Architectures: Using Grounded Theory for the Design of Software Architectures
扎根架构:使用扎根理论进行软件架构设计
- DOI:
10.1109/icsaw.2017.41 - 发表时间:
2017 - 期刊:
- 影响因子:0
- 作者:
Habtom Kahsay Gidey;Diego Marmsoler;J. Eckhardt - 通讯作者:
J. Eckhardt
Diego Marmsoler的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
相似国自然基金
基于SMART技术的鳄梨叶中诱导肿瘤细胞铁死亡的先导化合物的定
向挖掘
- 批准号:
- 批准年份:2024
- 资助金额:0.0 万元
- 项目类别:省市级项目
基于“活性-代谢组-基因组-SMART”整合策略发掘老鼠簕内生放线菌新型先导化合物
- 批准号:82360696
- 批准年份:2023
- 资助金额:32 万元
- 项目类别:地区科学基金项目
特定微环境激活的mRNA翻译(SMART)系统的设计及其免疫治疗应用研究
- 批准号:22307121
- 批准年份:2023
- 资助金额:30.00 万元
- 项目类别:青年科学基金项目
基于ANDSystem与多组学的水稻和小麦胁迫响应分子调控网络及智能作物平台(Smart Crop)的构建
- 批准号:
- 批准年份:2022
- 资助金额:105 万元
- 项目类别:
基于SMART设计建立中医药随机对照试验“随证施治”决策模型的研究
- 批准号:
- 批准年份:2020
- 资助金额:52 万元
- 项目类别:面上项目
精神障碍出院患者自杀风险简短联系干预(BCIs)的实施科学研究:基于序列多次分组的随机对照试验(SMART)
- 批准号:72004140
- 批准年份:2020
- 资助金额:24.0 万元
- 项目类别:青年科学基金项目
线上强化失眠认知行为治疗(Smart-CBTI plus)对失眠障碍合并焦虑、抑郁患者的随机对照研究
- 批准号:20Y11906600
- 批准年份:2020
- 资助金额:0.0 万元
- 项目类别:省市级项目
DRiPs致病性T细胞与胰腺CUZD-1蛋白双靶向Smart-DDS诱导免疫耐受治疗1型糖尿病的研究
- 批准号:81970707
- 批准年份:2019
- 资助金额:55.0 万元
- 项目类别:面上项目
基于B-SMART的类风湿关节炎分级诊疗的药物治疗管理模式构建与评价
- 批准号:71804109
- 批准年份:2018
- 资助金额:16.5 万元
- 项目类别:青年科学基金项目
面向Smart Grid基于多反馈路径的安全无线数据收集方法研究
- 批准号:61003309
- 批准年份:2010
- 资助金额:20.0 万元
- 项目类别:青年科学基金项目
相似海外基金
CRII: SaTC: Discerning the Upgradeability of Smart Contracts in Blockchains From a Security Perspective
CRII:SaTC:从安全角度辨别区块链智能合约的可升级性
- 批准号:
2245627 - 财政年份:2023
- 资助金额:
$ 31.58万 - 项目类别:
Standard Grant
An innovative platform to reduce the risk of cyber attacks on smart contracts for all blockchains by minimising human effort and improving the efficacy of security testing.
一个创新平台,通过最大限度地减少人力并提高安全测试的效率,降低所有区块链智能合约遭受网络攻击的风险。
- 批准号:
10047308 - 财政年份:2023
- 资助金额:
$ 31.58万 - 项目类别:
Collaborative R&D
Remote sensing and smart contracts for biodiversity data
生物多样性数据的遥感和智能合约
- 批准号:
10030674 - 财政年份:2023
- 资助金额:
$ 31.58万 - 项目类别:
Collaborative R&D
Distributed Optimization in Residential Power Grids for Real-Time Energy Management Using Blockchain Based Smart Contracts
使用基于区块链的智能合约对住宅电网进行分布式优化,实现实时能源管理
- 批准号:
RGPIN-2019-04632 - 财政年份:2022
- 资助金额:
$ 31.58万 - 项目类别:
Discovery Grants Program - Individual
STTR Phase I: Blockchain ontology and services for monitoring and performing analytics on smart contracts
STTR 第一阶段:用于监控和执行智能合约分析的区块链本体和服务
- 批准号:
2052118 - 财政年份:2022
- 资助金额:
$ 31.58万 - 项目类别:
Standard Grant
Safer Smart Contracts: Using Formal Verification and Programming Languages Techniques to Audit Smart Contracts.
更安全的智能合约:使用形式验证和编程语言技术来审计智能合约。
- 批准号:
568065-2022 - 财政年份:2022
- 资助金额:
$ 31.58万 - 项目类别:
Postdoctoral Fellowships
Ethical Perspectives Towards Using Smart Contracts for Patient Consent and Data Protection of Digital Phenotype Data in Machine Learning Environments
在机器学习环境中使用智能合约获得患者同意和数字表型数据数据保护的伦理视角
- 批准号:
10599498 - 财政年份:2022
- 资助金额:
$ 31.58万 - 项目类别:
An innovative voluntary carbon credit marketplace using smart contracts that will save UK-based firms £30m as well as help project developers access pre financing.
使用智能合约的创新型自愿碳信用市场将为英国公司节省 3000 万英镑,并帮助项目开发商获得预融资。
- 批准号:
10035310 - 财政年份:2022
- 资助金额:
$ 31.58万 - 项目类别:
Collaborative R&D
Toward a Fast and Secure Blockchain Framework for Smart Contracts
建立快速、安全的智能合约区块链框架
- 批准号:
RGPIN-2020-05926 - 财政年份:2022
- 资助金额:
$ 31.58万 - 项目类别:
Discovery Grants Program - Individual
Smart Contracts & Productivity Platform for Sheep & Pigs
智能合约
- 批准号:
830255 - 财政年份:2021
- 资助金额:
$ 31.58万 - 项目类别:
Innovation Loans