论文部分内容阅读
伴随着计算机技术、大数据技术、云计算技术的飞速发展，基于云计算的网络犯罪案件频繁发生，云取证技术在此背景下逐渐兴起。云取证要求在复杂的网络环境中，确保取证证据的原始性、完整性和可靠性。云取证是计算机取证的一个前沿领域，它处于包含各种网络设备和计算机网络节点的云计算环境中，是计算机取证和网络取证的综合体。云取证比一般计算机取证环境更复杂，取证情形更难分析。取证难度的加大迫切需要一种形式化描述方法使得云取证调查具有可靠性和可信性。 为此，本文提出了一种结合OCL（对象约束语言）与TA（时间自动机）的云取证形式化描述方法:对象约束语言描述云取证的静态属性语义特征，时间自动机模型描述云取证的动态行为事件，从静态特征描述、动态事件验证两方面保证取证证据准确、可靠。本文的主要创新性工作如下: (1)提出一种采用OCL语言描述的云数字取证可扩展特征语义模型，简要地阐述了云数字取证的概念，并详细描述使用OCL和FODA（面向特征的领域分析方法）的建模过程。对电子数据的特征、特征集合空间、云取证特征集合空间的概念进行描述，利用语义逻辑关系建立特征空间，在数字取证领域中对特征进行全面的语义描述。利用特征集描述证据的静态属性，并利用约束条件验证属性的有效性。该模型不仅解决了电子数字的静态取证描述问题，而且解决了证据静态属性间的冲突检测问题。 (2)采用瀑布模型的开发方式，形式化描述云环境下电子证据的动态行为。首先，介绍时间自动机的概念。其次，用时间自动机形式化描述电子数据取证特征集合，系统阐述事件行为的各种交互组合方式及其形式模型，用动态行为模型解决云取证电子数据动态行为时间的重构问题。 (3)在时间自动机模型基础上，提出一种基于MLTS（多集标号迁移系统）的非法行为检测算法。该算法将时间自动机转换为标号迁移系统，并进一步扩展成多集标号迁移系统，利用标号迁移系统的组合属性，使用可隐藏动作属性的动作组合判断动态行为组合的合法性算法，解决电子数据的动态行为取证问题。 (4)为验证上述描述方法的有效性，以云计算的流媒体点播系统和食品安全追溯系统为例阐述云取证系统的设计、建模和应用分析过程。利用Hadoop和Xen等搭建云计算实验平台，分析讨论取证系统的性能。