通过静态类型分析系统软件的安全性艾蒂安·米隆引用此版本：艾蒂安·米隆。通过静态类型分析系统软件的安全性其他[cs.OH]。皮埃尔和玛丽·居里大学-巴黎第六大学，2014年。法语。NNT：2014PA066120。电话：01067475HAL ID：电话：01067475https://theses.hal.science/tel-01067475提交日期：2014年HAL是一个多学科的开放存取档案馆，用于存放和传播科学研究论文，无论它们是否被公开。论文可以来自法国或国外的教学和研究机构，也可以来自公共或私人研究中心。L’archive ouverte pluridisciplinaire通过静态类型分析系统软件的安全- Linux内核的应用程序蒂安·米隆在Emmanuel Chailoux和Sarah Zennou的指导THese要获得标题科学博士提及计算机2014年7月10日在由以下人员组成的评审团面前进行了UNIVERSITY PIERRE和 MARIE CURIEOCTORALE学院I信息学、电信和电子学报告员Sandrine Blazy IRISAPierre Jouvelot矿业巴黎科技董事Emmanuel Chailloux皮埃尔和玛丽居里大学SarahZennou空客集团创新检查员吉勒·穆勒皮埃尔和玛丽·居里大学文森特·西蒙网谷歌邀请奥利维尔·莱维兰·安西我许多C程序员认为"强键入"只是意味着在键盘上增加额外的重量。彼得·范登林登""ii.如果你只是来开玩笑的，那就开始吧。谢谢你最后一页要写!我听过多少次"感恩是最简单的"这句话然而，我在完成这项工作的满足感和忘记帮助我完成这项工作的许多人中的一个的恐惧之间左右为难首先，我要感谢我的论文导师Emmanuel Chailloux和Sarah Zennou。如果没有他们有见地的建议和大量的校对，我不可能完成这项工作。还要感谢Sandrine Blazy和Pierre Jouvelot同意归还我的手稿，并感谢他们的评论，这有助于提高手稿的质量。 我还要感谢评审团的其他成员，吉勒·穆勒和文森特·西蒙内，以及奥利维尔·勒维兰，他是我们的嘉宾。如果这次冒险能够成功，也要感谢博士学校团队所做的工作，特别是Marylin Galopin和ChristianQueinnec，他们一直知道如何帮助我完成这个真正的行政追求，这就是博士学位。 我也祝愿贝特朗·格拉纳多一切顺利，他将接管EDITE。研究工作的对应部分传统上是教学工作这个项目开始于空中客车集团创新（当时的EADS创新工程），当时我还是一名对编译感兴趣的工程专业学生。 感谢瓦茨拉夫·戈达尔和查尔斯·海曼斯为我提供了这次实习机会，并将其扩展到我的论文项目。接下来的事情有点模糊，我衷心感谢Axel Tillequin和整个SE/IT团队对我的信任，他们在一个特殊的环境中欢迎我，这对一个年轻的研究人员来说是一个很好的环境。 再次感谢Sarah同意继续这个项目。我还要感谢这些年来接待我的另一个团队：APR团队，特别是走廊里讨论的不同研究主题让我 我还要感谢这些年来为我的工作条件提供便利的行政人员。该项目的一部分也由CERCLES²项目资助我特别感谢Pascal Manoury在巴黎狄德罗大学PPS实验室对我的欢迎在这里。26-00-325办公室以自己的方式参与了本文件的编制。停顿Alberto 宣 布 的 café 和 它 的 仪 式 性 pistonnade 允 许 我 们 日 复 一 日 地 讨 论 通 用 编 程 （ 和Ramzy）、应用函子、用Rust编写Basic解释器的最佳方式，或者让我们克服詹姆斯敦的第5级的策略，所有这些当然都有原理图、画谜和计数器支持因此，感谢Vivien（我不会像其他人那样指名道姓）、Phi-lippe（我们知道他的藏身之处）、Benjamin（因为他的品味）、Mathias（因为他有品位）、Guillaume（因为他的9-3咖啡交易，你会给我1公斤红酒吗？），Au-rélien（Rochechouart的古典类型），Jeremie（λ--永恒面前的叛徒）和所有在那里呆得更短的人。iii.据说论文 为了分享愉快的时刻，缓解怀疑的时刻，非常感谢一直在那里的朋友们。也感谢我的家人，他们总是给我继续我的最后，谢谢你，安娜。 你肯定是一个谁看到了最多的幕后这一长期的工作，同时扮演的角色，一个知己和新闻官，总是回答"很快!" "那么，斯蒂芬，他什么时候支持？" 今天特别奉献给Tarpuy，Mato，垫的女士，煎饼的女士，Guile和惊喜的客人的主题，以及整个团队的最终形式在编写本文件时，没有滥用λ-术语材料中的T型台目录iv1引言11.1操作系统的作用..........................................................................................................................1.2内核空间和用户空间之间的分离1.3系统类型41.4语言61.5L’analyse1.6从..................................................................................................................................................1.7论文10的目标和贡献1.8论文11大纲I安全的形式化方法2操作系统2.1物理体系结构2.2任务和权限级别2.3系统调用2.4困惑的副问题....................................................................................................................... 183现有静态分析3.1分类213.2语法方法3.3价值分析与抽象解释3.4类型243.5安全语言3.6Hoare 27的逻辑3.7证据助理第一部分的结论系统代码分析语言4评估的语法和语义4.1注释364.2语法404.3记忆和价值观414.4口译员434.5对值的4.6对存储器状态的操作4.7访问者49四目录v4.8评价背景.................................................................................................................................................4.9左............................................................................................................................................................. 值544.10 表达式.....................................................................................................................................................554.11 指令......................................................................................................................................................... 574.12 错误584.13 句子和程序的执行.................................................................................................................4.14 示例595类型635.1环境和符号.............................................................................................................................................645.2表达式.....................................................................................................................................................655.3指令......................................................................................................................................................... 685.4功能695.569句话5.6类型70的安全性5.7值的类型5.8类型72的属性5.9进步与保护776类型扩展6.1初步示例：用作位掩码....................................................................................................................... 的整数826.1.1修正案836.1.2例如：!xy.................................................................................................................. 846.2指标来源分析6.2.1SAFESPEAK............................................................................................................................................................86的内核扩展6.2.2语义..........................................................................................................................................扩展886.2.3简单..........................................................................................................................................类型的不足896.2.490型.........................................................................................................................................系统的扩展6.2.5类型92的安全性第二部分的结论第三章实验7实施997.1NEWSPEAK和编译链7.2L’outil7.3示例1077.4业绩1088案例研究：Linux内核8.1内核代码111的特性8.2Linux....................................................................................................................................................112中的系统调用8.3风险1138.4第一个错误示例：RadeonKMS 113驱动程序8.5第二个示例：Black fin....................................................................................................................115上的ptrace8.6实验....................................................................................................................................................... 程序117六、目录第三部分的结论9结论1259.1捐款....................................................................................................................................................... 1259.2与C 126的差异9.3前景129ARadeon模块KMS133B语法和评估规则B.1表达式...................................................................................................................................................的语法137B.2指令....................................................................................................................................................... 的语法138B.3运算符...................................................................................................................................................的语法138B.4评估背景...............................................................................................................................................B.5错误评估规则......................................................................................................................................B.6左值和表达式的求值规则..................................................................................................................B.7语句、句子和程序的评估规则.........................................................................................................B.8内核扩展评估规则..............................................................................................................................C类型规则C.1常量和左...............................................................................................................................................值的类型规则143C.2运算符的类型规则C.3表达式和语句...................................................................................................................................... 的类型规则145C.4值的类型规则C.5内核扩展类型规则D证据147D.1镜片成分D.2进展148D.3保存153D.4内核....................................................................................................................................................... 156扩展的进展D.5内核....................................................................................................................................................... 扩展的保留157图159列表定义列表161定理和引理列表网站参考参考书目1651个一、引言通信、视听、运输、医疗：所有这些领域在过去几十年中都发生了变化，特别是由于数字革命事实上，最小的电子设备现在都包含可编程的硬件组件。2014年，我们当然会想到手机，它的功能和复杂性使它们更接近台式电脑例如，谷歌的Android操作系统是基于Linux内核的，最初是为微型计算机设计的操作系统的内核... ... ）和在其上运行的应用程序（例如，web浏览器、计算器或地址簿它还必须保证数据的安全性：作为一个可信的中介，内核有许多责任，并且是唯一可以访问某些敏感信息的人。重要的是要确保他是唯一一个可以访问它的人特别是，必须能够验证用户向内核发出的请求不会自愿或非自愿地劫持内核并使其泄露机密信息。问题是，就像所有的软件一样，操作系统内核虽然校对和调试活动占用了大部分的开发时间，但很容易忽略编程缺陷这些错误或bug可能会在物质或人的层面上产生戏剧性的后果。例如，一架空客A320飞机上有近1000万行代码，确保这些代码不会危及乘客的安全至关重要。一种有效的技术是执行测试，即然后可以检测到不需要的行为但是，即使进行了大量的测试，另一种方法是在运行程序之前分析程序的源代码，并拒绝运行包含某些危险结构的程序。C’est静态分析中最常见和最简单的技术之一例如，如果n是整数变量的名称这允许您知道程序是否会处理彼此不兼容的数据。1CH A P I T R E2第1章。引言回到操作系统内核，这些内核既处理敏感数据，也处理来自外部世界的数据，而这些数据是无法保证的我们希望能够区分这两类数据。更具体地说，确保操作系统内核隔离的关键点之一本文的目的是证明静态类型可以用来检测和禁止这些危险的操作1.1操作系统的作用计算机由许多硬件组件组成：微处理器、内存和各种外围设备。 在用户级别，有几十个软件可以执行各种计算和通信。操作系统允许在这两个秤之间进行接口。在计算机系统的历史进程中最初，程序员可以访问整个硬件：可以访问所有内存，可以使用所有指令然而，这是一个有点限制，因为它只允许一个人与系统交互。在20世纪60年代后半期，出现了第一个"分时"系统，允许多个用户同时工作。允许例如，几个程序将一个接一个地使用处理器，并且每个程序将主存储器或硬盘驱动器的一部分如果多个程序这些是操作系统的角色因此，程序不是通过低级指令直接访问硬件，而是与内核通信，内核例如，让我们比较一下从CD-ROM或USB驱动器复制数据时实际发生的情况。• 在CD-ROM的情况下，您必须询问SATA总线，询问驱动器中是否存在磁盘，激活引擎，计算磁盘上数据的帧号，请求读取，然后触发存储器的副本。• 使用密钥，您必须查询USB总线，在其中查找正确的设备编号正确的通道编号，将读取命令应用于正确的块编号，然后复制存储器这两个操作虽然简而言之，操作系统是软件和硬件之间的中介，特别是负责管理内存、外围设备和专业设备。1.2. 内核空间和用户空间之间的分离3耶稣。实现细节不会呈现给用户;相反，用户会处理抽象，如文件的概念。有关操作系统概念和案例研究的详细说明1.2内核空间和用户由于内核保证硬件的安全使用，因此用户或运行的程序不能直接操作内核。因此，有必要在内核空间和用户空间之间建立保护。在硬件级别，我们使用特权级别的概念来确定D’une例如，假设因此，不会触发内存保护错误因此，对于操作内存中数据的指令下表描述如果例如，倒数第二处理器模式特权（代码）特权（数据）可能的访问核心核心核心是的核心核心使用者是的核心使用者核心是的核心使用者使用者是的使用者核心核心不使用者核心使用者不使用者使用者核心不使用者使用者使用者是的除此检查外，某些类型由于用户程序无法访问这些低级指令，因此它们所能做的非常有限 通过只使用非特权指令，我们只能执行计算，而不能执行从程序外部可见的操作。因此，为了使用硬件或访问高级抽象（如创建新进程），它们必须通过内核。 内核和用户程序之间的通信由系统调用机制组成。1. 在这里，"更高"是"更有特权"的同义词在第2章介绍的英特尔实施中4第1章. 引言在系统调用期间，使用来自用户的参数调用内核函数（在内核模式下）。因此，在处理这些数据时必须特别小心。例如，考虑一个从磁盘读取的系统调用：我们将参数（d，o，n，a）传递给内核，其中d是磁盘的名称，o（对于偏移量）是磁盘上开始读取的地址，n是要读取的字节数，以及内存在预期的用例处理器处于内核模式，正在但是，即使这种情况在运行时没有产生实际上，如果我们向系统调用传递一个属于内核空间一部分的地址，会执行几乎是相同的：在复制时，我们处于内核模式，执行处理内核数据的内核指令。 同样，在执行过程中也没有错误。因此，您可以写入类似地，写到磁盘（和读到内存）的函数从这些基元可以访问其他正在执行的进程，或者将执行转移这是因为我们通过测试内核的权限来访问内存，而不是测试发出请求的用户（用户）的权限。 这个问题被称为混乱的副问题[Har88]。因此，为了实现系统调用，有必要禁止直接取消引用其值可以由用户控制的指针。 在通过地址传递参数的情况下，有必要在运行时检查参数是否具有与调用方相同的权限。很容易通过这样1.3类型系统大多数编程语言都包含类型的概念，其目的之一是防止对彼此不兼容的数据进行在内存中，计算机处理的唯一数据根据所执行的操作，它们将被解释为整数、内存地址或字符。然而，很明显，有些操作是没有意义的：例如，将一个数字乘以一个地址或取消引用除法的结果是我们希望能够防止的行为。简而言之，类型化的目的是对对象进行分类，并根据对象的类限制可能的操作：简而言之允许这种分类的模型被称为类型系统，通常由一组类型规则组成动态类型在这种情况下，程序处理的每个值都用一个标签来装饰，该标签定义了如何解释该然后在运行时执行类型化规则。 例如，"+"运算符检查其两个操作数是否具有"整数"标签，然后构造通过将两个操作数相加而获得的值。1.3. 5型系统两个值，标签为"整数"。静态类型在这种情况下，我们在编译时进行检查。为了验证这一点，我们给每个函数一个约定，就像"如果传递了两个整数，并且函数返回一个值，那么这个值将是一个整数"。编译器可以使用静态类型系统来静态地检查这组合约例如，我们可以说"+"运算符的这意味着，如果我们传递两个整数（INT，INT），那么得到的值也是一个整数。相反，如果传递给该运算符的不是强类型化或弱类型化无论何时执行此分析，都可以对没有类型化错误的程序有或多或少的保证通过将其推向极端，强类型系统确保值始终具有预期的类型。对于静态类型，这允许完全消除运行时但通常情况并非如此，因为语言中可能存在允许绕过类型系统的构造，例如类型转换运算符。 这就是所谓的弱类型。多态性有时为函数指定唯一类型的限制太多如果我们考虑一个函数将一个元素添加到列表中，或者另一个函数对一个数组进行排序，它们的类型是否应该包括被操作元素的类型？作为第一近似，我们可以想象为要操作的数据类型提供一个代码版本。这是C语言或Pascal语言的早期版本所采用的解决方案，这使得编写库变得非常困难[Ker81]。这称为单态射。另一种方法是允许多个函数具有相同的名称，但参数类型不同。例如，我们可以分别定义两个整数之间、两个浮点数之间或一个整数和一个浮点数之间的加法根据编译时已知的信息，将选择正确的版本这就是C++中运算符的工作方式。这被称为特别多态性或重载。另一种技术是不根据函数参数的类型，而是根据调用函数的对象来确定被调用的函数。这允许这称为对象多态 在这种情况下，它依赖于子类型：如果A1和A2是B的子类型，则可以在需要B类型值的地方使用A1或A2类型的值。在这种情况下，将调用相应的函数最后一种可能性是参数多态性，它涉及使用相同的代码，而不考虑参数的类型例如，在这种情况下，我们使用单个函数来处理整数列表或浮点数在某些情况下，不是为每个函数分配一个类型，而是为它分配一个参数化的类型，该类型可以实例化为一个具体的在列表处理函数的情况下，其思想是，当不接触元素时，无论其类型如何，处理都是有效的。 该技术在[Mil78]中首次描述。对于不同静态类型系统的概述，特别是多态性6第1章。引言1.4语言Unix系统从1969年开始开发，最初是在PDP-7小型计算机上的汇编程序中开发的 为了帮助这种移植，有必要创建一个"可移植汇编程序"，即C语言[KR88，ISO99]。它的目标是在汇编语言之上提供抽象控制结构（if、while、for）允许使用结构化编程，即限制goto语句的使用。数据类型也是从机器抽象出来的：因此，int表示一个机器整数，而与其实际大小无关。 它的类型系统虽然是静态的（编译时可能会有类型错误），但相当基本：所有形式的转换都被接受，一些转换由编译器自动插入，并且语言提供的大多数abs-pull都是可渗透的。Linux内核是用C语言的方言编写的。苹果的Mac OS X系统的内核然而，这种语言 有些结构是模棱两可的，而许多行为是隐含的。如果要分析程序，最方便的做法是使用更简单的中间表示，以在这种情况下，我们向分析添加一个初步阶段我们介绍了一些可以用于此目的的语言：中间端第一个候选者当然是C编译器除了标准C之外，它们还具有接受大多数软件使用的各种扩展（GNU、Microsoft、Plan9）的优点。特别是，Linux内核严重依赖于GNU扩展GCC使用名为GIMPLE [Mer03]的内部表示这是一个用C语言编写的树结构，它依赖于许多宏来隐藏内部实现细节，这些细节在两个版本之间可能会有所不同。由于这种表示被认为很难处理，MELT [Sta11]项目允许生成一个用Lisp方言编写的编译器插件。LLVM[LA04]是一个由开源社区开发的编译器，后来由Apple赞助与GCC不同，它的代码库是用C++编写它使用一个中间表示，可以作为C++数据结构、紧凑的字节码文件或文本进行操作Cmm是在编译OCaml[LDG+ 10，CMP03]时用于生成代码的内部表示，可在编译器源代码中使用（因此它是OCaml数据结构）。这种语言的优点是2. 根据是否存在名为a的类型，表达式（a）-（b）将被解释为-（b）的转换类型。在类型a中，或从表达式（a）和（b）中减去。3. 例如，可以使用较小的整数调用接受长整数的函数这将被隐式转换1.5. L’ANALYSE STATIQUE DANS L’INDUSTRIE AÉRONAUTIQUE不幸的是，C--[PJNO 97][1]是一个旨在统一编译器所使用的中间语言的项目。这个想法是，如果前端可以发出C--（作为文本），就有可能获得高效的机器代码。例如，Haskell GHC编译器使用与C--非常相似临时中间语言由于构造适合于静态分析的中间表示的问题并不新鲜，因此已经有几个由于CIL[NMRW02]是C程序的OCaml表示，自2002年以来一直在由于插件机制，它允许对C程序的静态分析进行快速原型化CompCert C、Clight和Cminor是Compcert中使用的中间语言，Compcert是一个经过认证的C编译器[BDL06，AB07]。 这些中间语言用于前端和中间端传递。1.5L’analyse面对1.2节中描述的理论和技术问题，有必要正确看待与之相关的工业问题。这里介绍的工作实际上是由EADS创新工厂的安全和软件安全团队在工业研究培训协议（CIFRE）的框架内完成的。今天因此，如果这类软件出现故障，我们可能会面临巨大的经济影响，甚至冒着人命的风险。验证和确认阶段是航空电子软件生命周期的核心，这是众所周知的。例如，如果飞行控制软件得到更有效的验证，阿丽亚娜5号的第一次飞行失败肯定是可以避免的有几种方法可以消除故障风险事实上，需要两种双重方法：测试和形式化方法。第一种方法是将软件置于特定的情况下，并验证输出是否与预期结果相对应："黑盒"测试包括仅对不同规模的模块规范（例如：软件、模块、类、方法）进行测试 相反，所谓的"白盒"测试是在有可用实现的情况下编写的。例如，这确保了每一次执行都是借用的。这种方法类似于教孩子们的九分证明：可以证明错误，但不能证明程序是正确的第八章第一章引言L’approche 例如， 通过确保它们是"安全的"，我们以自动化的方式证明没有错误。L’interprétation如果一组值的抽象是具体集合的超集，则该方法是合理的换句话说，我们得到了一个过度近似。"安全"区（对应于无错误的执行）通常有一个相当简单的形式，考虑到所考虑的错误：它是简单集合的乘积，如区间。相反，程序的所有实际行为都是以更复杂和不可计算的形式出现的。通过以更简单的形式计算后者的近似值，可以更容易地测试行为是否在安全区域内：分析是合理的这一事实图1.1总结了这种方法：危险值的集合用阴影线表示，安全值的集合用白色表示，程序的实际行为的集合用点表示，近似值用灰色表示 可能会出现几种情况。在图1.1（a）中，我们在编译时证明了程序在运行时不会有错误。 在图1.1（b）中，近似值涵盖了危险情况：由于缺乏精确度而发出警报。在图1.1（c）中，近似值是不合理的（通过构造，我们避免了最后，在图1.1（d）中，由于错误行为的存在，我们发出了正确的警报因此，困难在于构造正确的过近似，但保持足够的精度。为了建立这种过度近似，可以使用各种工具。例如，一个整数可以用它的最小值和最大值来表示（抽象范围），而指向数组的指针可以用一组变量来表示，这些变量与存储器区域开始的偏移量相关联（抽象范围）。指向数组的指针）。彭吉利项目在这个意义上，作为Penjili项目[AH07]的一部分，EADS创新工厂开发了基于抽象解释的工具这些静态分析不直接处理C代码，而是处理一种称为NEWSPEAK [HL08]的中间语言它的表达能力足以编译大多数C程序，包括Linux内核中使用的许多GNU扩展（8.1节），并且存在C和Ada的自动翻译器（7.1节）。其次，它的指令是正交的和最小的：通常只有一种方法可以做事情。例如，控制流被限制为无限循环和向前跳跃（广义的"break"）。最后，当某些结构不明确时，会做出选择 例如，函数参数的计算是按特定顺序进行的，类型大小是在每个变量声明中指定的，等等。将中间语言与分析阶段分开可以大大简化静态分析器。（一）（b）（c）（d）1.6. 从图1.1：过度近似。所有错误的状态都是阴影的。用点表示的程序的有效状态集由灰色集合近似。循环仅处理NEWSPEAK语言以及用于操作它的工具可以在[3]上以免费许可证获得。基于这些工具的Penjili静态分析器已用于分析数百万行代码的关键嵌入式软件。它所有这些工具都是用OCaml语言[LDG+ 10，CMP03]编写的1.6从验证航空电子软件的安全性是至关重要的，但它的优点是，这些软件的开发考虑到了这些困难。 通过首先知道所有约束来构建安全系统比事后验证现有系统是否能够满足这些安全约束更容易。然而，这种设计软件的方式是非常昂贵的。因此，对于不太重要的组件，考虑现有的软件或库可能是值得的，特别是在开源世界这些软件更难分析，因为它们是在没有任何特殊约束的情况下编写的不仅允许语言的所有结构，即使是那些难以处理的结构（类型转换、动态分配、递归、文件系统访问等），而且还可以使用非标准扩展结构s {chara;int b;短c;};结构s {chara;int b;短c;} 属性（打包）;第一章第十章引言不自给自足的计划绝大多数的计划都是不自给自足的。这是因为它们几乎总是与其环境交互或调用库函数这意味着正在分析的文件我们不仅无法访问它们的源代码，而且我们也无法先验地了解它们的规格一种解决方案可以是为它们提供特定的处理（例如，通过为它们分配预定义的类型有些函数直接与操作系统交互 例如，pthread_Create（t，NULL，f，NULL）启动f（NULL），同时继续执行竞争对手。例如，图1.2显示了packed属性（GCC支持）对结构编译的影响。如果没有它，字段将以便于存储器访问的方式对齐，例如，通过使每个字段的地址以4个字节的倍数开始（粗体）。 这需要引入未使用的填充字节（灰色）。因此，该结构的总大小为12个八位字节。ABCABCFIGURE 1.2：使用相反，使用packed完全消除了填充，并允许将结构的大小减少到仅7个字节。 由于b和c不对齐，因此访问它们的效率较低。一般来说，编译器允许通过扩展对发布的代码进行精细的自定义。它们有时会以一种微妙的方式改变程序的执行方式1.7论文的目标和贡献这项工作的目的是在C语言中定义和实现"轻量级"静态分析（即比抽象解释值分析更简单），以检测用户指针的危险使用。我们建议将实际上，类型允许以相当大的粒度对程序的执行环境（这里是系统调用参数）进行建模，而更细的粒度是困难的，并且需要对环境进行建模。
我的内容管理
展开
