【摘 要】
：
随着区块链和智能合约技术的广泛运用,越来越多的数字资产、隐私信息等敏感数据被存储到区块链上,因此区块链应用中的安全漏洞可能导致严重的后果。以安全模式为基础实现区块链应用的验证是提升应用安全性的一种有效途径,现有方法根据系统安全需求选择适用的安全模式,在此基础上将模式与功能模块组合为系统的设计模型,并通过模型检测方法验证系统的安全性。但这些方法往往将系统看作一个整体进行建模和验证,忽略了系统内部模块
论文部分内容阅读
随着区块链和智能合约技术的广泛运用,越来越多的数字资产、隐私信息等敏感数据被存储到区块链上,因此区块链应用中的安全漏洞可能导致严重的后果。以安全模式为基础实现区块链应用的验证是提升应用安全性的一种有效途径,现有方法根据系统安全需求选择适用的安全模式,在此基础上将模式与功能模块组合为系统的设计模型,并通过模型检测方法验证系统的安全性。但这些方法往往将系统看作一个整体进行建模和验证,忽略了系统内部模块的组合细节。本文提出一种基于安全模式的区块链应用建模和验证方法,首先使用代数规约语言SOFIA描述安全模式及其组合,以构建区块链应用的形式化模型,然后将SOFIA规约转换为Alloy规约后使用模型检测工具来验证组合的正确性和应用的安全性。本文主要包括以下四个方面的研究工作:1.分析安全模式的主要结构并给出安全模式的定义,在此基础上使用代数规约语言SOFIA描述模式的数据结构、操作行为和安全需求,并使用图数据库Neo4j构建安全模式数据库,实现模式的管理和检索。2.给出一个基于安全模式的区块链应用建模方法,首先将区块链应用分解为一系列基本模块和组合模块,并确定各个基本模块使用的安全模式,然后通过实例化安全模式构建基本模块的代数规约,最后使用抽象规约和实现规约的双元结构描述组合模块的对外功能和内部实现。3.提出一个自底向上的区块链应用验证方法,将SOFIA规约转换为Alloy规约后使用模型检测工具依次验证基本模块是否满足功能和安全需求,以及组合模块是否正确组合了其子模块且满足相应需求,并设计实现了规约转换原型工具A2A。4.使用本文方法对区块链众筹应用BCF和区块链在线医疗系统BOMS进行案例分析,并与现有方法进行比较。实验结果表明本文方法能够有效地检测出区块链应用规约中的缺陷,提升了区块链应用的安全性。
其他文献
无线电能传输由于具有良好的灵活性、安全性、可靠性和便捷性,已成为国内外的研究热点。磁耦合器是无线电能传输系统的关键部件,但目前基于铁氧体屏蔽层或铁氧体加铝板屏蔽层构成的磁耦合器存在体积大、重量重和成本高等问题,严重制约了无线电能传输技术的进一步发展和应用。为此,本文围绕磁耦合器的线圈特性和屏蔽层优化设计展开研究,提出了一种新型磁芯结构和一种新型混合屏蔽层结构,具体工作如下:首先,分析磁耦合器优化设
精噁唑禾草灵（FE）是一种芳氧苯氧丙酸类除草剂,其微生物代谢途径的首步反应为酯键断裂,生成精噁唑禾草灵酸（FA）和乙醇。有关FE水解酶的报道较少,其代谢机制有待阐明。实验室前期从FE高效降解菌Rhodococcussp.T1和Acinetobacter sp.DL-2中分离鉴定得到FE水解酯酶Feh和AfeH,两者的序列相似性为10%,且具有较大的催化特性差异。本论文选取Feh和AFeH为研究对象
我国是农药需求和使用量极大的国家。农药是保障我国农业生产的重要生产资料,但与农药污染相关的问题也随之而来。为解决这一问题,一是要加大研发力度,研制出低毒低残留的新型替代农药;二是加强农药对环境毒害和动态规律研究。植物诱抗剂是近年来较热门的研究方向,能够诱导农作物分泌能抵御病虫害的物质以达到防治作物病虫害的目的。香草硫缩病醚作为新研制的一种植物诱抗剂,对番茄褪绿病等植物病害有显著预防效果,具有高效低
随着国际社会对资源开发保护和能源转型的重视,清洁能源发电将走向主力电源的位置,高比例可再生能源接入电网是必然趋势,并网研究日益重要。高比例随机出力的分布式电源接入电网后,系统中的随机变量不仅包含随时随地波动的负荷,还增加了分布式电源出力等不确定变量,使配电网无功优化更加复杂,因此研究不确定因素下的电力系统无功优化具有实际应用意义。本文针对分布式电源并网特性,综合考虑配电网运行经济性、稳定性和可靠性
木薯原产于巴西,随着现在经济的快速发展,木薯在世界各地的热带及亚热带地区都被广泛种植。目前,在中国的广西,广东,福建,云南,贵州及海南等省均广泛种植。木薯的块根富含淀粉,在我国工业淀粉产业中,木薯淀粉占到市场份额的10%左右,同时是重要的燃料乙醇和绿色化学工业材料。木薯是热带地区低收入农民的主要粮食作物,全球总产量的65%都被用来制作人类食品,木薯粉以及木薯叶则是高能量的饲料原料。木薯淀粉以及木薯
随着时代进步和科技发展,摄影得以迅速普及,逐渐地融入到大众的日常生活中,其拍摄方式的简便化使得图像素材无限丰富。蓝晒工艺是一种极具代表性的古典摄影技术,其操作简便、光影感丰富、独一无二性等特点充分体现了个性化的影像语言。在当代摄影提供图像素材的基础上,蓝晒工艺的创造性也为摄影图像的发展提供了更加广阔的空间。近年来,蓝晒工艺逐渐呈现与纺织服装领域融合的趋势,但要实现广泛的应用仍有诸多亟待突破的问题,
菊花（Chrysanthemum morifolium）是起源于中国的一种传统名花,栽培历史悠久,种类繁多,兼具观赏、食用、茶用、药用价值。茶用菊具有多种有益的功能性内含物,现已成为一种重要的保健饮品。近年来,茶用菊产区黑斑病频发,已成为严重制约茶用菊规模化生产的严重病害。化学防治中不规范地喷施农药会带来农药残留、环境污染以及病原抗药性等问题。唯有鉴定出优质抗病种质,明确黑斑病菌致病及茶用菊抗病机
黄瓜绿斑驳花叶病毒（Cucumbergreen mottle mosaic virus,CGMMV）严重危害黄瓜、西瓜、瓠瓜、甜瓜等葫芦科作物,且该病毒会导致作物大幅度减产。近年来,我国各口岸检验检疫部门多次在进境种子中检测出CGMMV。感染CGMMV的植株因环境条件、株系类别、寄主植物的不同,发病时表现的症状也有所差异,一般情况下会导致植株生长迟缓、矮化,叶片斑驳畸形,果肉纤维化甚至腐烂。针对C
风机性能试验作为风机生产应用中不可或缺的一环,在实际设计优化过程中尤为重要。目前国内所测风机主要用于通风、换气和引风,这与速冻装备风机的运行情况差异较大。本文从速冻装备出发,对离心风机的性能试验系统进行了设计开发,主要内容如下:首先,通过对冷风机性能参数和测试系统实际需求的分析,完成了某速冻装备离心风机性能测试系统的总体方案设计。其次,在GB/T 1236-2000《工业通风机用标准化风道进行性能