SPIN模型在猎头领域的融合、演进及其应用

文章介绍了猎头公司吸纳SPIN模型的普遍属性和心理方法,并在理论层面予以融合和演化,并以客户需求分析为应用支点,探讨猎头实践的调整和变革。

基于SPIN的Linux管道模型检测研究

针对科学实验载荷使用的Linux操作系统,对其测试方法等做了研究总结。模型检测作为一种全自动运行的形式化验证手段,在其适用领域对发现系统逻辑错误意义重大。针对操作系统测试需要,对Linux管道通信进行了源代码研究,使用有限状态自动机进行建模并转化为Promela语言,并运用SPIN模型检测工具对其进行了形式化验证;对之前研究中模型不完整、不够细化、主体间关联性等问题进行了改进和完善,并就实验中发现的问题进行分析,并提出了改进方案。

RGPS过程层元模型正确性验证

利用Web服务本体描述语言对RGPS过程层元模型进行描述,建立Promela模型。基于线性时序逻辑,以及Spin检测工具的偏序规约和on-the-fly等优化技术对Promela模型进行正确性验证,设计并实现RGPS过程层元模型正确性验证平台。通过城市交通系统实例证明该验证方法的正确性和有效性。

基于SPIN的远程证明协议的形式化分析及改进

远程证明是解决移动支付安全问题的有效手段之一。通过对可信计算远程证明协议进行分析,发现用户平台配置信息的隐私性、用户的认证性和远程验证者的认证性存在脆弱点,使用SPIN模型检测工具,应用模型检测方法对协议进行了形式化分析,检测出破坏性攻击漏洞。针对协议中的漏洞对协议进行改进,提出了一种基于用户属性加盐哈希的方法,通过用户属性保证协议的安全传输。最后使用SPIN检测改进后的协议,证明了改进方案的有效性、安全性,阻断了发现的攻击。

基于Spin的安全协议形式化验证技术

针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑(LTL)公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协议改进方案,并针对改进后的协议,给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法:模型检测过程中的存储状态数减少,使模型复杂度降低约40%;迁移状态数减少,使验证效率提升约44%。

智能合约的形式化验证方法

智能合约是一种代码合约和算法合同,将成为未来数字社会的基础技术,它利用协议和用户接口,完成合约过程的所有步骤.总结了智能合约主要技术特点和现存的可信、安全等问题,提出将形式化方法应用于智能合约的建模、模型检测和模型验证过程,以支持规模化智能合约的生成.研究提出了一个应用于智能合约生命周期的形式化验证框架和验证方法,针对一个智能购物场景,采用Promela建模语言对智能购物合约进行建模,用SPIN进行了模型检测,验证了形式化方法对智能合约的作用.

基于Hash轻量级RFID安全认证协议

为应对伪装攻击、位置攻击、重放攻击、异步攻击和DNS攻击等安全问题,提出一种轻量级安全认证协议—MH协议,对轻量级Hash函数的加密以及认证时间戳做出改进,有效减少逻辑位的操作。为验证该方法的正确性,使用BAN逻辑方法以及SPIN模型检测工具,从多个角度和方面,与其它轻量级安全协议进行比较,在运算复杂度相同的情况下,MH协议的安全强度达到了0.438,具有较强的安全性能。

基于PUF的安全固态盘双向认证协议

针对固态盘数据保护问题,提出一种基于物理不可克隆函数(physical unclonable function,PUF)的固态盘双向认证协议,实现加密固态盘和用户之间的身份认证以及密钥管理。认证协议以盘端PUF模块生成的物理指纹作为最高可信根,采用口令+UKey双认证因子,UKey作为用户身份认证标识和数据密钥载体。使用BAN逻辑和SPIN工具从形式化的角度对提出的协议进行分析和模型检测,分析结果表明,所提协议能够实现有效的双向认证,具备对恶意女仆攻击、中间人攻击、重放攻击、物理探测攻击、侧信道攻击等的抵抗能力。

无人机无线通信协议的形式化认证分析与验证

针对无人机组与地面控制站之间进行无线通信时的身份认证问题,首先分析无线通信协议的工作流程及其形式化表示,然后对网络系统中的诚实主体和攻击者进行形式化建模,其中推导了协议安全属性的LTL公式,通过建立密钥机制,实现控制站与无人机节点以及各个无人机节点之间的身份认证;运用模型检测工具SPIN验证无线通信协议的一致性,其中提出一种改进的知识项获取方法,加快攻击者需掌握知识集的求取过程;验证结果表明该无人机无线通信协议具有中间人攻击漏洞。