一种验证分布式协议活性属性容错机制的模型检测方法

云计算是一种通过网络以服务的方式向用户提供按需收费的计算资源的模式,目前企业逐渐将业务部署、数据处理转移到云计算平台上进行.因为可扩展性、性能等各方面需求,所以云平台部署在分布式系统上.由于分布式系统采用大量的商品机通过复杂的结构进行搭建,因此分布式系统中组件发生故障是无法避免的.为了提高分布式系统的可靠性,技术人员在开发分布式系统时为其设计了容错机制.为了保证容错机制在分布式系统发生故障时能真正有效地工作,故障注入是检验容错机制的方法之一,通过人为地向系统中注入特定的故障,观察系统的行为并检验容错机制是否正确工作.由于分布式系统的并发特性,传统软件测试方法无法对其进行完全测试,近年来越来越多地使用模型检测技术来对分布式系统进行验证.现有的模型检测技术注重对分布式系统的安全性属性和活性属性的检测,忽略了对容错机制尤其是活性属性容错机制的检测,所以如何验证系统的活性属性容错机制是目前面临的挑战.采用抽象模型检测方法会引入模型与实际系统不匹配的问题.同时,采用实现级模型检测方法会加剧模型检测中的状态空间爆炸问题.本文提出了一个实现级模型检测工具LTMC(Liveness Properties Fault Tolerance Model Checker),结合故障注入技术对分布式协议的安全性属性与活性属性及其容错机制进行验证.同时,基于分布式系统节点的角色,本文提出了一种对等约减策略PRP(Peer Reduction Policy)对LTMC需要搜索的状态空间进行约减,缓解了状态空间爆炸问题.此外,LTMC通过引入逻辑时钟机制,优先搜索那些更有实际价值的事件执行路径.LTMC能够有目标地在待验证系统运行的特定时刻注入特定的故障,而不依赖于随机故障注入策略;当待验证系统发生改变时,只需要简单地对工具进行轻微的修改;LTMC可以系统地发现分布式协议中指定类型的所有Bug.在本文最后,我们将LTMC应用到ZooKeeper和Cassandra的几个协议中,并与深度优先搜索作对比,可以发现LTMC有3.7～594.4倍的状态空间约减率.     

DataCon:面向安全研究的多领域大规模竞赛开放数据

网络安全数据是开展网络安全研究、教学的重要基础资源,尤其基于实战场景下的安全数据更是科研教学成果更符合安全实践的保障。然而,由于网络安全的技术变化快、细分领域多、数据敏感等原因,寻找合适的网络安全数据一直是研究者们进行科研和老师开展实践教学时关注的重要问题。本文总结并分析了多个领域的经典公开安全数据集,发现其在研究应用时存在数据旧、规模小、危害大等不足;克服安全数据领域选择、大规模实战数据获取、安全隐私开放等困难,构造了更符合当前科研需求DataCon安全数据集。数据集大规模覆盖DNS、恶意软件、加密恶意流量、僵尸网络、网络黑产等多个领域,且均来自实战化场景,并基于DataCon竞赛平台将其开放给参赛者和科研人员。目前,DataCon数据集涵盖了已成功举办四届的“DataCon大数据安全分析大赛”的全部数据,大赛被国家教育部评为优秀案例,并进入多所高校研究生加分名单,数据内容也一直随着真实网络环境中攻防场景的变化而持续更新。目前,DataCon数据集涵盖了已成功举办四届的“DataCon大数据安全分析大赛”的全部数据,大赛被国家教育部评为优秀案例,并进入多所高校研究生加分名单,数据内容也一直随着真实网络环境中攻防场景的变化而持续更新。数据集持续收到科研人员、学术的数据使用申请,支撑了多篇学术论文的发表,充分说明了其有效性和可用性。我们希望DataCon数据及竞赛能够对网络安全领域产、学、研结合有所帮助和促进。