1 磁盘描述的形式化基础
1.1 文件系统描述
我们选择FAT12文件系统为例，因为它具有很多简单特性：只有一片磁碟、高级和低级格式化使用同一个命令、不需要分区等等，而且大部分操作系统都支持它。另外，FAT文件系统非常简单、容易理解，它的技术手册也很容易获取。尽管也有众所周知的弱点，但它现在仍然有着较为广泛的应用。
为了管理磁盘上的数据，FAT12文件系统使用三种不同的数据结构：文件分配表、目录区和数据区[2]。
1.2 磁盘反取证攻击与不变量
我们这里所说的不变量源于这样一个事实，即磁盘或文件系统中的信息可能有冗余，或者可能分散在不同的层[3]。使用不变量可以将我们对因反取证攻击而缺失了的信息的需求转化为一个形式证明的正确性规则，并能以表达式的形式将其形式化规约为一个状态谓词。系统安全的形式验证也因此可归结为对具有这些不变量的系统可达状态的检查。
2 文件系统的形式化描述
为了对文件系统进行面向取证调查的形式化描述，我们采取如下六个步骤：
1）从文件系统中抽象细节。文件系统包含很多分项和细节使得它的描述难以理解且难以验证或证明。因此我们从文件系统中抽取出形式化规约所必须的一些细节。
2）建立文件系统基本库。在文件系统规约中，要描述它们的布局和数据组织安排，还是有些复杂的。因此，在面向磁盘反取证攻击的规约语言中应该具备一个专门的文件系统基本库。为此我们定义一个包含文件系统布局架构中的基本元素的文件系统库。例如，对FFS文件系统，这些基本元素包括：扇区、碎片、块、超级块、分组以及索引结点[4]等。
3）创建文件系统的可信形式化模型。我们考虑两类描述文件系统所用的行为集：第一类是合法的、由操作系统提供的平常功能行为；第二类是技术含量较高的或恶意使用文件系统的行为。
规约当然可以直接利用它们来描述系统的运转以及它们对文件系统元素带来的影响。
4）不变量的形式化描述。一个深入了解文件系统的调查者能够提取出一系列对发现反取证攻击有用的正确性性质（不变量），并以此分析出与安全事件相关的信息，避免在数据收集期间遗漏有用的证据。这一方法可以应用于任何文件系统，更为重要的是它能丢弃大量的无用数据而快速识别出攻击。
5）假设恢复行为。一般来讲，要让系统从一个状态迁移到另一个状态而又缺少一些具体信息的细节时，假设似乎是一种必然选择。在磁盘反取证攻击的情况下，要想从被侵害的状态中恢复，我们可以用假设来填补一些信息细节的缺失，比如攻击是如何进行的，或者在被更改前数据是如何组织的等等。
6）整合系统。在最后一步中，形式化规约应该允许已定义行为集中行为的任何连续序列都能在可信模型中得到定义，并且它们所表示的都是对文件系统的合法使用。
3 用TLHA+规约文件系统
本节，我们以FAT12文件系统为例，用TLHA+[1]创建文件系统基本库、给出文件系统的形式化规约，并用随后描述的一组安全性和活性不变量对磁盘反取证攻击进行侦测。
3.1 文件系统基本库
我们用FatLib模块来规约FAT12文件系统基本库，主要由三部分组成，下面我们给出每一部分中的最重要的元素和操作。
1）文件分配表。我们描述的文件分配表恰好有（n+2）个值，前面的n个值表示相应磁盘簇的数值，后面的两个代表簇链的结束标记和坏簇标记。我们用一个从可用簇号（包括结束标记eof（fat）和坏簇标记bad（fat））到自身的函数来表示文件分配表。
2）目录区。我们不妨假设所有文件都存储在根目录下，所以没有文件夹。我们用三个分项来表示任一个目录条目，即文件标识符、开始簇号、使用簇的数量。然后，我们定义一个从目录条目集到三值元组（文件标识符、开始簇号、使用簇的数量）集的函数来表示目录区。
3）数据区。我们同样把数据区定义为一个函数，它把每一个簇的簇号映射到它所存储的内容，这些内容可以是Data型和nodata型。前者是一个TLHA+常量，而后这是我们定义的一个假想值，用来表示空簇的内容。
3.2 文件系统使用建模
本节我们为文件系统的使用过程建立可信的形式化模型，并将其用于FAT12文件系统的TLHA+规约。此模块是对模块FatLib的扩展，我们把它命名为AttDet。该模块使用三个常量：SecNbr、Data和DirNbr，分别表示可用簇的数量、系统可能生成的数据内容和目录区支持的最大目录条数。除常量外，规约中还定义三个变量：文件分配表fattb、目录区dir和数据区dataarea。
系统的初始状态由谓词Init描述，其中定义的磁盘是已经格式化的，所有文件分配表的条目都设置为0，对目录区也做同样设置。至于数据区，每一个簇都没有数据。实际上，这就是一个刚完全格式化后的磁盘状态。
系统的行为包括写文件行为WriteFile（fid）、删除文件的行为DeleteFile（fid）、磁盘快速格式化行为QuickFormat、表示由入侵者或技术高超的用户进行的行为序列ModifyDisk，最后我们定义一个关系，叫做下一状态关系——Next，来表示上面定义的所有行为的析取。它蕴含了系统所有可容许的状态，也就是对文件系统的合法使用。
4 反取证攻击的模型检测
为了自动验证所描述系统的正确性性质，我们使用检测工具TLHC[1]。尽管它有着众所周知的局限性，如空间爆炸问题，但模型检测技术却是侦查磁盘反取证攻击的有效方法。首先，这一技术在识别不变量的违反上比其他技术如定理证明等快得多。其次，它可以就违反不变量的情况给出反例，也因此可以辨别出潜在的攻击场景。
4.1反取证攻击场景的生成
我们在模块AttDet中描述了集Data的一批符号常量和为两个参数SecNbr和DirNbr赋值，即定义一个具体实例之后，就可以利用TLHC来检查上节中讨论的正确性性质。其结果生成了大量的磁盘反取证攻击场景。
4.2 不变量与可能攻击场景
现在，假设一个调查者使用我们提出的形式化方法，从最初获得的有效证据出发，对基于FAT的文件系统的反取证攻击进行调查取证。使用我们在模块FATLib中定义的文件系统基本库，并因此亦可使用同样的不变量。事实上，后者仅依赖于文件系统模型本身。另外，由于模型检测工具的输出结果是一些导致不变量被违反的并不完整
的文件系统使用轨迹，这就要求调查者根据自己的知识和经验来推断攻击是如何进行的。
4.3 基于假设的数据恢复
有些磁盘反取证攻击的数据是比较容易恢复的，例如，某个攻击对给定文件对应的簇链进行了不大的修改，只要修复这一改动，文件就可被恢复正常。不幸的是，尽管某些可用的数据收集工具可以从一些一般的攻击案例中恢复部分数据，但这一工作通常都受到反取证攻击的制约。
为了克服以上的缺点，我们提供一种智能的、使用TLHA+的方法，从4.1中所描述的攻击场景中恢复数据。在缺少判断攻击如何进行或数据是如何组织的信息时，我们将以假设予以填补。
我们的方法包括描述一组独立的行为，每一个行为都是在某一个或一些假设条件下，对文件系统的修改，以及可观察到的反常——对不变量的违反。
5 小结
本研究利用假设行为时序逻辑语言TLHA+及其模型检测工具TLHC，设计具体证明方法和途径，其目标是形式化和自动化磁盘入侵取证调查以及从遭受攻击的系统中恢复数据。这一方法支持对大量已知和未知的基于磁盘技术的反取证攻击的侦查。另外，它能够通过对有效磁盘证据的非确定性推理发现攻击，恢复数据，以规避进一步的攻击。
参考文献：
[1] 李均涛，唐郑熠，李祥.基于行为时序逻辑的入侵取证研究[J].计算机应用研究，2011，28（7）： 2742-2745.
[2] Tony Sammes and Brian Jenkinson. Forensic Computing： A Practitioner’s Guide. Springer-Verlag UK， 2000.
[3] Sriranjani Sitaraman and S. Venkatesan. Forensic analysis of file system intrusions using improved backtracking. In Proceedings of the Third IEEE International Workshop on Information Assurance （IWIA’05）， pages 154–163， College Park， MD， USA， March 23-24 2005.
[4] Kulesh Shanmugasundaram and Nasir Memon. Automatic reassembly of document fragments via context-based statistical models. In Proceedings of 19th Annual Computer Security Applications Conference， pages 152-159， Las Vegas， NV， USA， December 8-12 2003. IEEE Computer Society.
