电子数据取证的可信固定方法

孙国梓,耿伟明,陈丹伟,林清秀

(1.南京邮电大学计算机技术研究所,南京 210003;2.南京邮电大学计算机学院,南京 210003)

电子数据取证的可信固定方法

孙国梓1,2,耿伟明2,陈丹伟1,2,林清秀2

(1.南京邮电大学计算机技术研究所,南京 210003;2.南京邮电大学计算机学院,南京 210003)

在介绍传统电子数据固定方法的基础上,针对可信取证理念,给出电子数据静态属性可信的支撑框架和可信固定方法.运用DSA数字签名、时间戳技术,并结合基于证实数字签名的第 3方保证方案,研究电子数据具体的可信固定算法.通过形式化分析,定义并描述电子数据静态属性可信的约束规则,为电子数据可信固定提供支持.结合取证实例,运用已总结的公理和规则进行可信取证的形式化分析.结果表明,该方法能对电子证据进行可信固定.

电子数据取证;可信取证;可信固定;形式化分析

目前,网络和计算机犯罪的数量逐年增加.打击犯罪的关键在于获得充分、可靠和强有力的证据.信息犯罪的很多证据是以电子数据的形式通过计算机或网络进行存储和传输的,因此需要采用计算机对电子数据进行取证(digital data forensics)[1].对计算机取证的研究,一直以来重点都是放在电子数据的获取和对所取得数据的分析上.对于电子数据取证的有效性或可信性还缺乏相应的论证,这样取得的数据容易受到质疑,其采信度也会降低.电子证据固定是司法鉴定工作的开始,同时也是后续所有鉴定工作的基础,因此电子证据的固定工作是否能使电子证据可信是至关重要的.

1 电子数据固定方法

电子证据的固定是指采用流程化的、标准的、合法的手段,使用专业的设备和软件,在不修改原始介质数据的前提下,创建出一个原始介质的副本供后期工作使用.

1.1 传统固定方法

根据固定时机的不同,电子证据固定分为静态固定法和动态固定法.静态固定一般是针对静态的相对稳定的数据进行的固定.一般说来,静态固定的工作相对简单,因为存储介质及电子数据已经处于静止状态,不存在外在破坏威胁因素,只要设备和方法得当,就可以很好地进行固定工作.而动态固定,由于存在外在攻击及破坏性,电子证据的固定相对较难.对于动态固定,一般固定流程[2]为:记录现场计算机的连接状态—固定易失数据—关闭当前计算机系统—取出硬盘介质—对硬盘介质进行写保护—使用专用设备进行硬盘复制—数字签名并封存保护—固定结束.硬盘复制机固定法和“只读锁 +软件”固定法是常用的 2种电子证据固定方法.前者采用基于位对位复制原理的高速硬盘设备进行复制,并使用 MD5算法进行一致性验证;后者是在原始硬盘的接口与所带的硬盘复制机接口不匹配或副本硬盘的容量比原始硬盘小等情况下使用的方法,例如,可通过 Encase的获取功能,将硬盘介质的内容生成符合国际惯例的 E01文件,并通过 MD5算法进行一致性验证.

1.2 可信取证与可信固定方法

针对目前计算机取证中“人 +工具”的取证现状和取证模式,考虑将当前的取证模式扩充为“人 +工具 +证明”,即在着眼于利用工具取得证据的同时,尽可能分享经验丰富的取证人员的知识和经验,并建立一套以逻辑、自动机等数学理论为基础的形式化取证模型,同时从理论上证明模型在取证中的有效性(即取证是可信的),最终形成一套可信取证的证明体系,以使电子数据的取证系统更加完备,所取得的数据更具说服力.借鉴可信计算的思想,文献[2]提出“可信取证”(trusted forensics)理念,结合电子数据的固有特征和取证行为,将电子数据可信取证宏观分为 2个方面:1)可信的静态属性(电子数据本身的静态特征可信);2)可信的动态行为(由电子数据转换为证据所需的过程或行为可信).以此为基础,实现指定电子数据可信获取(发现、固定、提取)和可信展现(分析、表达).本文所指的电子证据的固定,是指在电子证据可信发现(在不破坏电子证据静态属性前提下,采用一定的嗅探技术或匹配检索技术对电子证据进行发现的过程)的假设前提下,对电子证据进行固定备份,以备后续电子证据的可信提取和可信展现等过程.针对图 1所示的可信支撑框架,给出其形式化的描述过程.

定义 1 支撑层次模型,定义 6元组来表示电子数据静态属性可信的支撑层次模型(Trusted Discovery,Trusted Fix,Trusted Extraction,Rule Storage,Tools＆Sofewares,Evidence Collected Machine,Evidence Collected-Machine Transcription,Operation Set).

其中,TrustedDiscovery是可信发现,指在不破坏电子数据静态特征的前提下,对可能的电子证据进行发现的过程,当有取证需求时,可信发现模块的工作引擎触发相应的工作模块,对被取证机进行分析,并把分析的结果报告给可信固定模块;TrustedFix指可信固定,即在不破坏电子数据静态属性的前提下或者为了能保证电子证据静态属性的可信性而采取的固定手段或方法;Evidence Collected Machine是被取证机;Evidence Collected Machine Transcription是被取证机副本,它具有与Evidence Collected Machine同样的有效性,是后续取证操作的副本;Trusted Extraction指可信提取,是使用相应的技术手段从被取证机副本中提取出有效的证据信息,以便提供给相关的司法部门作为证据;Rule Storage是操作规则库,根据具体情况给出对应的操作规则;Tools＆Sofewares是进行操作可以调用的工具和软件;Operation Set是操作集合,起到信息反馈和各个模块之间的连接作用.

定义该模型及其模型组元之间的关系规则:

规则 1 fbj(j=1,2,3,…,n)表示某一特定的取证活动,fs为某取证操作服务,FB为全部取证操作集合,则∀fs,∃fb1,fb2,fb3,…,fbn∈FB,满足(fb1,fb2,fb3,…,fbn)→fs.

即每个取证操作服务都要由 1个取证行为序列完成.

规则 2 设 fsj(j=1,2,3,…,n)表示一系列特定的取证操作服务,fg表示某个取证操作的目的,则∀fg,∃fs1,fs2,fs3,…,fsn,满足

即某个取证操作目的由 1个或多个取证操作服务达到.

图1 电子数据静态属性可信的支撑框架Fig.1 Framework of trusted static-attribute for digital data

2 基于时间戳的可信固定方法

为了研究方便,把前面电子证据可信固定的方法定义为函数 TF().例如,对于电子证据 X,TF(X)表示采用此种方法对电子证据 X进行固定.本节在计算机取证的基础上,以确定目标信息可信性为目的,运用 DSA(digital signature algorithm)数字签名机制及简单时间戳技术[3-9],提出一种保证和证明电子证据完整性、可信性的方案.在基于密码学及简单时间戳的前提下,证明方案的安全性和可信性.

2.1 理论基础

时间戳机制包括 3方:1)时间戳服务机构 TSA;2)时间戳申请者 A;3)时间戳信赖者 R.

本文把即时产生的信息文档记为 fi;单向哈希函数记为 h();h()生成的消息摘要记为 d;时间戳签名记为 tsd;时间戳函数记为 sig();t为 TSA收到时间戳请求的时间;被取证机记为 S;使用‖表示字符串连接操作;C表示信息记录一致性验证者.关于时间戳签名协议的描述参见文献[3-4],另外可参考文献[5-8]了解数字签名的 DSA算法.

2.2 电子数据可信固定流程

计算机系统中需安全转移的关键性文件主要有系统安全日志、入侵检测日志以及各种重要应用程序安全记录等.这些文件信息记录是逐条产生的,网络恶意入侵者成功入侵后的第一件事就是删除其中与其入侵过程有关的信息记录或者直接删除文件.因此相应的信息记录必须在产生之后尽快复制、签名,并进行安全转移.为了快速地对新产生的信息记录 fi进行安全转移,必须在 fi生成的时候就进行复制、签名和安全存储,见图 2[9].1)生成新纪录 fi,即时转移该信息到安全存储器,并用数字签名软件进行哈希值计算,di=h(fi);发送到权威时间戳服务器 TSA进行

数字签名,并回送到安全存储器 S,进行安全保存.2)针对 p、q、g公开的要求,产生满足条件的素数 p和 q,计算 g=h(p-1)/qmod p.同时,产生随机的小于q的 k值,计算出对应的 r和 k-1.3)由上述一组结果(ki,,ri),根据公式 y=gxmod p计算相应的公开密钥 yi.根据公式 s=(k-1(SHA(f)+xr))mod q计算相应的 si.至此,得到的 ri和 si就是被取证机 S对第 i条信息记录 fi的数字签名.当 1条新的信息记录

的签名完成,S就将签名ri、si、信息记录f′i、记录序列号i以及该记录生成的时间ti发送到安全存储对象M中.可以验证 S签名的有效性,也可以验证第 i条签名所对应的信息摘要有效,有效防止第 i条签名与第 i-1条签名之间被删除或添加任何记录,具体电子数据信息签名的验证参考文献[9].

2.3 基于证实数字签名的第 3方保证

图2 电子数据可信固定流程Fig.2 Workflow of trusted fixing for digital data

上述电子证据的固定方案,某种程度上而言,已经可以保证电子数据经签名后的有效性.为了更好地进行电子数据的可信固定,与前面的方案相结合,参考文献[5],本文继续引入一种证实数字签名的方案,从第 3方(或称证实者)的角度来加以保证.在电子数据取证的过程中,证实数字签名的参与方有签名者S(犯罪嫌疑人),证实者 C(第 3方的司法鉴定机构)以及验证者 V(公检法等相关职能部门).由此,构建数字签名的相应算法.图 3给出了第 3方保证的算法流程.

1)犯罪嫌疑人 S的密钥生成算法 针对(p,q,g)的公开要求,假定 y是犯罪嫌疑人的公开钥,x是对应的秘密钥,且 y=gxmod p.由此得到CKGS(1l)=SKG(1l)→(p,q,g,y,x).

2)第 3方司法鉴定机构 C的密钥生成算法 设n是2个大素数的乘积,(n,e)是公开钥,d是相应秘密钥,则有 CKGC(1l)=EKG(1l)→(n,e,d).

3)犯罪嫌疑人S的签名算法 使用DSA中的普通数字签名算法 Sig对信息签名,得到关于信息 m={0,1}*的签名,再利用 RSA对签名(r,s)进行加密,得到证实签名 σ=(c1,c2)=(remod n,semod n).文献[5]给出了证实与否认算法.另外,也可考虑利用文献[6]的有效群签名方案进行第 3方的公正鉴定,限于篇幅,本文不再深入讨论.

图3 第 3方保证流程Fig.3 Workflow of third party guarantee

3 电子数据静态属性可信的约束规则

以下列出的是规范电子数据静态属性可信约束的部分定义、公理和规则.首先对它们进行形式化的描述.

定义 2 电子数据取证操作,指运用一定的合乎规范的方法和流程,从计算机或计算机网络中获取数据的过程.

定义 3 电子数据取证规范,指为了保证电子数据的可信性,在取证过程中,必须遵循的一系列行为准则.

定义 4 电子数据取证可信,指所取得的数据具有完整性和原始数据的一致性.

定义 5 电子数据静态特征可信,指与原始数据相比较,复件电子证据的属性没有发生变化.

定义 6 原始数据,指计算机或计算机网络中所包含的所有数据,记为 D={d1,d2,d3,… ,dm}.

定义7 所取数据,指运用一定的取证手段从原始数据中提取出的数据,记为D′={d′1,d′2,d′3,…,d′m},其中m＞=1.

定义 8 电子证据类型,指 estyle={efstyle,evolatile},其中,efstyle为固定型数据,evolatile为易于挥发的电子数据,也即非固定型数据.

定义 9 电子证据创建时间,记作 EST={est1,est2,est3,…,estr}.其中,r＞=1,r是自然数.

定义 10 可信发现 TD={td1,td2,td3,…,tdn},是指在保证电子证据不被破坏的前提下,对可能的电子证据进行发现的操作.例如,在预见可能存在易失数据的前提下,不能采取关机操作,而要采取安全的措施获取易失数据.

定义 11 可信固定 TF={tf1,tf2,tf3,…,tfm},是指在从 TD→TD′的过程中,保证 SD′EST↔SDEST,即保证SD′EST与 SDEST具有一致性 .

定义12 可信操作TO={to1,to2,to3,…,tok},TF⊂TO∧TD⊂TO,指能保证电子证据静态属性可信的操作;

定义 13 取证开始时,计算机所处的状态集合为 S={s,r,c,⇁c},其中,s表示关闭,r表示运行,c表示联网,⇁c表示未联网.

定义 14 电子证据转换模型,是指电子证据由原始证据到所取证据的转换过程流程.其形式化的转换如图 4所示.其中,转换工作指由 D→D′的过程中所有的工作.

定义 15 定义 es为 D的载体,es′为 es的副本.

下面给出电子数据可信取证中的一些公理、规则.

公理 1 ∃di∈ D,dj=TF(di),则 di.lmt=dj.lmt,di.lvt≠ dj.lvt,di.est≠ dj.est,di.ctxt≠ dj.ctxt(lmt为最后一次更改的日期时间;lvt为最后一次访问时间;est为创建的日期时间;ctxt为电子证据内容).

公理 2 ∃di∈ D,dj=copy(di),则 di.lmt=dj.lmt,di.lvt≠ dj.lvt,di.est≠ dj.est,di.ctxt≠ dj.ctxt.

公理 3 ∃di∈D,dj=open(di),则 di文件的访问时间属性发生变化.

公理 4 ∃di∈ D∧ ∃dj∈ D′,若 E(di)=E(dj),则 E可信 .

规则 3 ∃di∈ D∧ ∃dj∈ D′,若 MD5(di)=MD5(dj),则 di≡ dj,取证可信.

规则 4 ∃di∈ D∧ ∃dj∈ D′,若 dj=m irror(di),则 di≡ dj,即 di与 dj可看作完全一致.

规则 5 if(M=C)then D.R=D′.R(如果文件的最后写或修改时间等于创建时间,则认为文件的静态属性可信).

规则 6 ∃di∈D∧di.estyle=evolatile,如果关闭电源,则 di丢失取证无效.

图4 电子证据转换流程Fig.4 Conver flow of digital evidence

规则 7 取证检查时,保证目标计算机系统,避免发生任何改变、伤害、数据破坏或病毒感染.

规则 8 所有的取证分析必须是在复制的硬盘上进行的.

规则 9 如果 es′=bitmirror(es),则取证可信,即比特级别的镜像载质与原载质完全等同.

规则 10 取证工具处于安全的环境中,取证工具没有破坏或者被病毒感染.

规则 11 尽力搜索所有可能存在证据的地方.

规则 12 分析电子数据要在磁盘的镜像拷贝介质里进行,而不能在原始介质上进行分析.

规则 13 加解密技术对数据进行安全保护主要有 2种方式:保密和证明数据的完整性.

规则 14 ∃di∈ D,∃aj,ak∈ A,若 ai(di)↔ aj(di),则 aj、ak有效 .

4 实例分析

下面给出文献[10]中描述的华盛顿大学计算机安全服务小组的资深专家 Dave Dittrich对计算机取证的实例分析.Dave Dittrich在有证据显示计算机系统正在被入侵时切断了系统的电源,之后对原始硬盘进行物理拷贝,并用 MD5对硬盘上的数据信息进行摘要.在遵循一系列计算机取证原则的基础上,他首先使用标准的 UNIX工具进行分析,发现 passwd文件中出现了 3个可疑的账号,于是以此为线索,进一步发现了入侵者在受害机器上安装黑客工具 rootkit的证据.接下来,Dave Dittrich使用 TCT工具,对系统中所有文件进行 MAC时间排序,并恢复被删除的文件,随后,他开始从大量的数据中寻找入侵证据,最后形成完整的最终调查报告.Dave Dittrich所作的主要工作:1)马上切断系统电源;2)对原始硬盘进行物理拷贝;3)同时用 MD5对原始硬盘上的数据做摘要,保存原始证据和摘要信息;4)在取证的过程中,对取证中的每个步骤和发现都进行详细的记录;5)将物理复制的磁盘以只读方式安装在取证系统上;6)使用标准的 Unix工具进行分析,发现可疑账号和与这些账号相关的可疑文件,找到了安装黑客文件的证据及黑客文件;7)使用 TCT(the coroner's toolkit)工具,对系统中所有文件按 MAC时间进行排序,并恢复出所有被删除的文件,寻找线索;8)汇总所有证据,形成取证报告.后续的调查也证明,该次计算机取证为确定犯罪嫌疑人提供了进一步的证据.

分析该次计算机取证和分析过程,结合上文的取证步骤、公理和规则,证明取证过程可信.取证开始,计算机的初始状态为 r(运行状态)和 c(联网状态).

取证步骤 1),保证了接下来要取得的数据与原始数据一致(若采取正常方式关闭 Unix系统,系统的缓存文件将被清除;采用断电的非正常关闭系统方式,则不会丢失这些文件).取证过程可信.

取证步骤 2),在此次取证过程中,重点是要发现入侵者,拷贝中会改变的文件属性对最后结果无影响,过程可信.

取证步骤 3),根据规则 3,过程可信.

取证步骤 5),根据公理 4,在对证据的分析过程中,取证人员以只读方式分析所取证据,分析过程可信.

取证步骤 6)和 7),满足公理 3及规则 14,取证人员先后运用了标准 Unix工具和 TCT工具对所取数据进行分析,2种工具的分析方法互补,分析过程可信.

综合对于取证过程及分析过程的形式化分析,可知取证方法和所取数据均可信,因此可得此次计算机取证可信.事实也证明,此次取证达到了要求,确定了犯罪嫌疑人.

5 结束语

本文针对电子数据静态特征进行了抽象和描述,给出一种保证电子证据可信的电子证据的固定方法和体系,描述了电子证据的形式化表达方法,并通过电子证据的取证实例进行了分析.本文仅针对可信固定的相关方面进行了研究,对于电子数据取证的有效性,即可信取证的其他方面仍需进一步研究.

[1]麦永浩,孙国梓,许榕生,等.计算机取证与司法鉴定[M].北京:清华大学出版社,2009:1-9.

[2]林清秀.电子数据可信取证的形式化方法研究[D].南京:南京邮电大学计算机学院,2009.LIN Qing-xiu.Research on the formalism of trusted forensics on digital data[D].Nanjing:College of Computer,Nan jing University of Posts＆Telecommunications,2009.(in Chinese)

[3]薛金蓉,张洪斌.可信时间戳的网络服务器取证技术研究[J].电子科技大学学报,2007,36(6):1404-1406.XUE Jin-rong,ZHANG Hong-bin.Technical research of reliable time stamp based network server forensics[J].Journal of University of Electronic Science and Technology of China,2007,36(6):1404-1406.(in Chinese)

[4]BRADLEY S,GEORGE M,ANDREW C.A correlation method for establishing provenance of timestamps in digital evidence[J].Digital Investigation,2006,3(1):98-107.

[5]王尚平,王育民,张亚玲.基于 DSA及RSA的证实数字签名方案[J].软件学报,2003,14(3):588-593.WANG Shang-ping,WANG Yu-min,ZHANG Ya-ling.A con firmer signature scheme based on DSA and RSA[J].Journal of Software,2003,14(3):588-593.(in Chinese)

[6]陈少真,李大兴.基于DSA的适合大群体的有效群签名[J].计算机研究与发展,2004,41(2):282-286.CHEN Shao-zhen,LI Da-xing.An efficient group signature scheme for large group on DSA[J].Journal of Computer Research and Development,2004,41(2):282-286.(in Chinese)

[7]BRUCE J,NIKKEL.A portable network forensic evidence collector[J].Digital Investigation,2006,3(3):127-135.

[8]ZOU C,CHIGAN C X.On game theoretic DSA-driven MAC for cognitive radio networks[J].Computer Communications,2009,32(18):1944-1954.

[9]綦朝晖,孙济洲,郭琳琳.一种基于计算机取证的信息一致性方案[J].计算机工程,2006,32(11):172-173,176.QIZhao-hui,SUN Ji-zhou,GUO Lin-lin.Message integrity scheme on computer forensics[J].Computer Engineering,2006,32(11):172-173,176.(in Chinese)

[10]DITTRICH D.Basic steps in forensic analysis of Unix systems[EB/OL].(2001-12-09)[2009-02-06]http:∥staff.washing ton.edu/dittrich/misc/forensics/.

(责任编辑 刘 潇)

One Trusted Fix Method of Digital Data Forensics

SUNGuo-zi1,2,GENGWei-ming2,CHEN Dan-wei1,2,LIN Qing-xiu2
(1.Institute of Computer Technology,Nan jing University of Posts and Telecommunications,Nan jing 210003,China;2.College of Computer,Nanjing University of Posts and Telecommunications,Nanjing 210003,China)

After an introduction of the traditional fix method of digital data,in view of trusted forensics,a framework and its corresponding trusted fixmethod which supports the digital data's static properties is provided.Using DSA digital signature,timestamp,and the third confirmer signature scheme,the specific trusted fix algorithm of digital data is studied.Via formalized analyzing,the constraint rules for the digital data's static propertieshave been defined to be trusted,which also supports to the trusted fix.At last,with introduced axioms,theorems and rules,the formalized analyzing of trusted forensics is validated by certain examples.

digital data forensics;trusted forensics;trusted fix;formalized analyzing

TP 309

A

0254-0037(2010)05-0621-06

2009-12-10.

国家“十一五”计划资助项目(2007BAK34B06);国家自然科学基金资助项目(60703086);南京邮电大学樊登计划资助项目(NY 208009).

孙国梓(1972—),男,安徽天长人,副教授.

book=93,ebook=93