OAuth2.0授权委托协议的优化研究与工程实现
这是一篇关于混合加密算法,二进制随机序列,OAuth2.0的优化,形式化验证,单点登录的论文, 主要内容为OAuth2.0应用于Web应用程序认证和授权,被大型开放平台广泛使用。目前报告称,Google和Facebook登录已经被超过28亿个应用程序使用,可见数量庞大,正因如此,其安全性一直备受关注。在OAuth2.0规范中,没有定义授权处理机制、令牌格式、加密方法,传统的实现技术和加密算法在保护访问凭证方面仍存在着安全威胁。针对上述问题,本文引入DESTH-ELGamal混合加密算法,通过二进制随机序列引入明文的处理过程,以及ELGamal算法将二进制随机序列和DESTH算法密钥在服务器间进行交换的方案,对DESTH-ELGamal混合加密算法进行加密改进。采用改进的混合加密算法加密OAuth2.0协议中的访问凭证,在访问凭证的传输过程中,使用SHA-512哈希算法结合ELGamal算法密钥实现签名,最终将访问凭证封装成JWT的格式发送给目标服务器,实现OAuth2.0协议的整体优化。在此基础之上,为确保更加安全的身份验证和信息交换,本文对优化的协议从功能和性能两方面进行评估,使用Spring Cloud,Spring Security框架设计并实现了基于优化的OAuth2.0协议的简单有效、安全可靠的统一身份认证平台。该平台将不同区域的信息系统进行整合,实现域内身份认证与授权,同时集成单点登录功能,以此实现简单高效的资源访问与共享。最后,通过基于概率的模型检测工具Prism对优化的协议进行形式化安全性验证,根据对时延性概率的结果分析,没有发现新协议的漏洞。
基于SCADE的计算机联锁系统建模与验证
这是一篇关于计算机联锁,SCADE,需求管理,建模,仿真,形式化验证的论文, 主要内容为计算机联锁系统是铁路信号系统中保证行车安全的重要设备,失效后可能导致重大人员伤亡和财产损失,系统功能逻辑需要具备很高的安全性要求。然而,传统的计算机联锁系统主要采用手工编码的方式进行开发,软件质量主要依赖于代码评审、走查、测试等人工方式进行保障,存在一定的主观性,无法满足计算机联锁系统的高安全性要求。形式化建模是安全关键系统开发的重要方法之一,具有严格的数学基础,能够准确和无歧义地描述系统需求,并且实现逻辑推理,能够有效地解决传统软件开发方法中存在的模糊性和二义性等问题。SCADE是基于形式化建模方法的高安全性软件开发环境,其提供安全状态机和数据流图两种形式化建模方法,能够直观、清晰、全面地描述软件功能逻辑;结合模型仿真和形式化验证能够直观、全面地分析模型的正确性和安全性,避免软件开发人员的主观性;最后自动生成面向工程的高质量的C代码。本文研究基于SCADE的计算机联锁软件开发方法,利用SCADE的需求管理、形式化建模、模型仿真、形式化验证等工具来保证计算机联锁软件的正确性和安全性,具体包括以下内容:(1)介绍了 SCADE的软件开发模式和同步假设理论,并详细分析了 SCADE的需求管理、安全状态机和数据流图建模、模型仿真、形式化验证以及代码生成机制。(2)分析了计算机联锁系统的基本结构、特点及软件功能,根据系统需求将计算机联锁进路控制过程划分为进路选择、进路锁闭、信号开放、信号保持开放、正常通过进路解锁、取消进路六个阶段,分析各阶段中计算机联锁系统SCADE建模的具体需求。(3)采用安全状态机和数据流图两种建模方法,建立计算机联锁系统进路控制过程的形式化模型。(4)利用SCADE需求管理工具分析计算机联锁系统需求、概要设计和形式化模型之间的追溯关系,保证SCADE模型完全覆盖计算机联锁系统的系统需求和概要设计需求。(5)通过图形化的模型仿真,保证计算机联锁软件模型的正确性;然后提取系统安全属性,利用形式化验证检测计算机联锁模型满足预期的安全属性;最后利用代码生成器自动生成面向工程的C代码。
面向供应链物流的区块链产业应用研究
这是一篇关于区块链,供应链物流,智能合约,形式化验证,模型检测的论文, 主要内容为区块链技术以其交易共识、账本同步、链上信息不可篡改等特性,为企业间业务协同创造了一种全新的业务执行模式,依托区块链平台可实现在多个不同的利益实体间高效地协同业务、可信地执行交易、安全地共享数据,既可提升效率,又可保证公平。但在区块链技术与产业应用结合的具体实践中,仍存在许多需要解决的新问题,一方面是区块链上的交易数据的隐私与安全问题,链上公开交易结果及交易细节,商业应用面临新的安全挑战;另一方面,业务的实现依靠智能合约,合约的逻辑合理性、功能完善性等需要予以保证,可信、公平的业务面临着新风险。针对上述问题,本文围绕区块链技术的产业应用,从支持智能合约运行的区块链平台和支持业务实现的智能合约两个方面着手,研究了面向产业应用的区块链平台建设和保障智能合约正确性的形式化验证等工作,主要研究内容如下:(1)研究了区块链技术支持特定产业应用的网络架构设计、数据存储机制、业务系统运维等问题。结合产业业务需求,提出在网络架构上,设计具有层级化的组织结构,以证书链的模式关联网络上节点的数字身份与现实身份,保证业务参与者在链上的活动可控、可监管;在数据存储上,设计单链多账本模式,将节点计算资源虚拟划分加入不同业务域中,维护业务账本一致性,保证业务数据不会被无关节点获取;在业务运维上,设计自底向上的权限管理模式,从区块链网络、智能合约、业务交互,三个层次对业务操作者进行管理。(2)研究了基于区块链技术的供应链物流产业应用实现,从参与业务实体与实体间的交互关系上,分析传统供应链物流业务场景,提出了基于区块链的业务实现方案;依据业务参与实体的不同,将整个业务过程分为供需匹配、合同签订、货物运输三个阶段,并针对供应链物流业务在各阶段需要达成的业务目标,开发执行区块链业务交易操作的智能合约。借助Fisco Bcos区块链平台,搭建符合业务需求的区块链网络,完成合约部署测试工作。(3)研究了智能合约业务设计完备性的形式化验证方案及验证实现。为了保证智能合约能够正确实现业务需求,采用模型检测的形式化验证方法,在系统建模上,基于有穷自动机模型,从合约业务实现的角度,抽象提取合约状态集合、状态间迁移关系、状态间迁移条件,并以此构造带约束的确定自动机模型,形式化建模合约业务模型;在属性规约上,采用时序逻辑描述合约需要满足的业务属性,并提出状态、变换覆盖的属性完整性设计要求。最后,基于上述建模方案,选用Nu XMV模型检测工具,验证了所编写的智能合约业务设计完备性。(4)研究了基于区块链平台支持业务交易功能实现机制下的智能合约执行正确性的形式化验证方案及验证实现。智能合约业务执行的正确性依赖于区块链平台(系统级)交易共识等的支持,及合约代码层面(应用级)交易执行正确性的保证。依托交易在区块链上的执行流程,以用户进程、节点交易池进程、交易打包、区块执行、合约执行多个交错并发执行的进程,共同建模区块链业务执行系统模型,从系统属性和业务属性两个方面,设计相应的属性规约。最后,基于上述建模方案,选用SPIN模型检测工具,验证了在区块链平台支持下的合约执行正确性问题。
基于安全状态机的计算机联锁系统建模与分析
这是一篇关于计算机联锁,安全状态机,SCADE,建模,仿真,形式化验证的论文, 主要内容为城市轨道交通以其安全可靠、污染低、运量大、速度快、受其他交通方式干扰小等特点,成为解决城市交通拥堵问题的首选方案。基于通信的列车控制系统(Communication-based Train Control, CBT C)具有轨旁设备少、列车追踪间隔短、运营效率高等优点,是列控技术的重要发展方向。计算机联锁(Computer Based Interlocking, CBI)系统作为CBTC的核心子系统之一,是一个安全苛求系统,对列车的安全运行有着重要的影响,具有极高的安全性和可靠性要求,因此,如何保证计算机联锁系统设计开发的安全性和正确性具有十分重要的意义。安全状态机(Safe State Machine, SSM)是一种图形化的同步建模语言,具有并发性、层次性、良好的优先级抢占机制和通信机制,模型清晰、简洁,具有良好的可读性,能够描述安全苛求系统复杂的逻辑过程。SSM形式化的理论基础避免了传统需求分析方法中的模糊性和二义性等缺陷；同时,高安全性应用开发环境(Safety Critical Application Development Environment, SCADE)支持SSM的建模、仿真和形式化验证,为SSM在实际工程中的应用提供了基础。本文选择SSM来对CBI系统进行建模和分析,主要包括以下几个方面：(1)分析了SSM的理论基础、建模特征及格局转移机制,并介绍了SSM在SCADE中的建模、仿真及形式化分析方法；(2)分析了CBI的基本结构及CBTC系统中的CBI的联锁功能,分析了CBI与CBTC子系统的交互关系,对比了CBTC下CBI与传统的联锁系统的区别。(3)将CBI划分为道岔、进路、信号机三个功能模块,分析了各个模块具体的逻辑条件；然后基于SSM的理论,利用SCADE对各个模块进行了建模,具体包括道岔请求、选排、锁闭逻辑,进路请求、检查逻辑,区段方向逻辑及信号开放逻辑等；最后利用SCADE的数据流图将道岔、进路及信号机三个模块集成为CBI逻辑模型。(4)通过SCADE提供的仿真器对模型进行仿真,检查CBI模型的正确性；然后提取系统的安全属性,利用SCADE的形式化验证器对模型进行形式化验证,证明模型满足预期安全需求,保证了模型的安全性和正确性。
Lustre语言安全性及活性模型检测工具的研究与实现
这是一篇关于Lustre同步语言,形式化验证,模型检测,可满足性模理论,活性性质的论文, 主要内容为作为保障软件系统符合设计需求的重要手段之一,模型检测技术在现代系统,特别是反应式实时系统的设计与开发中受到了越来越多的关注。在反应式实时系统这一领域,Lustre同步数据流语言占据了代表性地位。随着Lustre语言在航空航天、工业能源和轨道交通等领域反应式实时系统的设计中被广泛使用,这些领域对软件苛刻的正确性要求使得对Lustre语言构建的程序进行验证变得至关重要。目前已经有许多对Lustre程序进行验证的工具,并且在工业领域也得到了一定的应用。然而,这些工具几乎都只关注了对安全性性质的验证,而在对活性性质的验证方面则尚未有工具提供支持。为了填补这一空白,本文对Lustre语言提出了一种适合于验证的形式化语义,并根据这一语义设计并实现了一种基于SMT求解技术的支持安全性及活性性质验证的模型检测工具。本文的主要研究工作包括:·提出了Lustre语言的形式化语义:为了在性质验证部分将Lustre语言模型转换为迁移系统,本文详细解释了Lustre语言中包括节点和表达式等在内的各个语法结构的含义,然后根据Lustre语言的特点提出了形式化的语义,从瞬时语义和数据流语义两方面分别刻画了Lustre这一同步数据流语言在某一具体时刻和整体时间上的性质,在理论方面保证了后续验证过程中模型变换的正确性。·设计并实现了同时支持安全性和活性验证的Lustre模型检测工具:在对Lustre程序进行语法解析后,将整体的验证流程分为用于消去复杂语法结构的Lustre简化器、将Lustre程序转换为SMT格式迁移关系的SMT翻译器和负责调用模型检测算法进行验证的验证控制器三个部分,使用包括有界模型检测、k-归纳法、不变式生成和IC3算法在内的算法对性质进行并行验证;同时在此基础上使用L2SIA-WFR算法对活性性质提供了支持。·在安全性和活性测试用例集下进行实验评估和分析:对于设计并实现的模型检测工具NKind,在安全性性质和活性性质方面分别采用了经典的测试用例集对其和现有的工具Kind2,JKind和ic3ia进行了性能表现方面的评估和对比。实验评估的结果表明,NKind能够有效地对安全性和活性性质进行求解,同时在求解的效率方面与现有的类似工具相比具有竞争力。
本文内容包括但不限于文字、数据、图表及超链接等）均来源于该信息及资料的相关主题。发布者：代码货栈 ，原文地址：https://bishedaima.com/lunwen/48520.html
