Marc Chevalier. Proving the security of software-intensive embedded systems by abstract interpreta-tion.. Cryptography and Security [cs.CR]. Université Paris sciences et lettres, 2020. English. NNT :2020UPSLE069. tel-03127921v20HAL Id: tel-031279210https://hal.inria.fr/tel-03127921v20提交日期：2022年4月27日0HAL是一个多学科开放获取存档，用于存储和传播科学研究文档，无论其是否已发表。这些文档可以来自法国或国外的教育和研究机构，也可以来自公共或私人研究中心。0HAL（开放式多学科存档）是用于存储和传播法国或国外教育和研究机构、公共或私人研究中心的研究级科学文献的开放存档。0通过抽象解释证明软件密集型嵌入式系统的安全性。0Marc Chevalier0引用此版本：0在巴黎科学与文学大学进行的准备0通过抽象解释证明软件密集型嵌入式系统的安全性0通过抽象解释证明软件密集型嵌入式系统的安全性0Marc Chevalier2020年11月27日星期五答辩0巴黎数学科学中心第386号学院0计算机科学专业0评审委员会成员：0Patrick Cousot 美国纽约大学教授 主席0Jérôme Feret INRIA研究员，法国 导师0Isabella Mastroeni 意大利维罗纳大学副教授 评委0Peter Müller 瑞士苏黎世联邦理工学院教授 评委0David Pichardie 法国雷恩高等师范学校教授 评委0Marc Pouzet 法国高等师范学校教授 评委0Sukyoung Ryu 韩国KAIST副教授 评委0Mihaela Sighireanu 法国IRIF副教授 评委i0摘要0本论文致力于通过抽象解释对低级软件（如操作系统）进行分析。分析操作系统是确保软件系统安全的关键问题，因为它们是紧邻硬件的层次，所有应用任务都依赖于它们。对于关键应用程序，我们希望证明操作系统不会崩溃，并且它确保程序的隔离，以便不受信任的程序不能干扰受信任的程序。这种类型程序的分析引发了特定的问题。这是因为操作系统必须使用在普通程序中没有意义的指令来控制硬件。此外，由于硬件特性超出了C的范围，源代码中包含了与C代码混合的汇编块。这是本论文的两个主要方向：处理混合的C和汇编语言，以及精确抽象低级软件特定的指令。这项工作是基于来自工业合作伙伴的案例研究的分析，该案例研究要求在静态分析器Astrée中实现所提出的方法。第一部分是关于混合简化模型的C和汇编语言的形式化，从语法到语义。这个规范对于定义什么是合法的和什么是错误的至关重要，同时考虑到C和汇编之间的相互作用的复杂性，包括数据流和控制流。第二部分是关于抽象解释的简短介绍，重点是以后有用的内容。第三部分提出了混合C和汇编语义的抽象。实际上，这是一系列处理语义各个方面的参数化抽象。第四部分关注低级软件特定指令的抽象问题。可以使用幽灵变量轻松地证明感兴趣的属性，但由于技术原因，设计一个允许令人满意地处理幽灵变量的抽象域的简化乘积是困难的。本部分构建了这样一个通用框架，其中的域允许我们解决我们的问题和其他许多问题。最后一部分详细说明了需要证明的属性，以确保尚未处理的程序的隔离，因为这些属性引发了许多复杂的问题。我们还提出了一些建议，以改进前一部分中引入的具有幽灵变量的域的产品，以提高功能和性能。0ii 摘要iii0摘要0本论文致力于通过抽象解释对低级软件（如操作系统）进行分析。对操作系统的分析是确保软件系统安全性的重要问题，因为它们位于硬件之上，所有应用任务都依赖于它们。对于关键应用程序，我们希望确保操作系统不会崩溃，并且能够保证程序的隔离性，以便未经验证的程序不会干扰受信任的程序。这种类型的程序分析涉及到一些特定的问题。这是因为操作系统必须使用在常规程序中没有意义的操作来控制硬件。此外，由于硬件功能超出了C的范围，源代码中包含了混合了C和汇编代码的代码块。这是本论文的两个主要方向：处理C和汇编的混合，以及对低级软件特定操作进行精细抽象。这项工作是通过对工业合作伙伴的案例研究进行分析而指导的，这需要在静态分析器Astrée中实现所提出的方法。第一部分关注混合C和汇编语言的形式化，从语法到语义。这个规范对于定义什么是合法的和什么是错误的非常重要，同时考虑到C和汇编之间的复杂交互，无论是数据还是控制流方面。第二部分是对抽象解释的简要介绍，仅限于后续有用的内容。第三部分提出了对C和汇编混合语义的抽象。实际上，这是一组参数化抽象，每个抽象都处理这种语义的一个方面。第四部分关注对低级软件特定操作的抽象。感兴趣的属性可以很容易地通过虚拟变量来证明，但由于技术原因，很难设计一个支持令人满意的虚拟变量管理的抽象域的简化产品。本部分构建了一个非常通用的框架以及一些解决我们问题的域。最后一部分介绍了一些需要证明以确保程序隔离性的属性，这些属性尚未处理，因为它们引入了新的复杂问题。0iv 摘要0此外，我们还提出了一些关于在前面的部分中引入虚拟变量的域产品改进的建议，无论是在功能还是性能方面。2.2.1.1General-Purpose Registers. . . . . . . . . . . . . . . . .102.2.1.2EFLAGS Register . . . . . . . . . . . . . . . . . . . . . .112.2.1.3Segment Registers . . . . . . . . . . . . . . . . . . . . . .122.2.1.4Instruction Pointer . . . . . . . . . . . . . . . . . . . . . .122.2.1.5Control Registers and Other System Registers. . . . . .132.2.2Stack. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .132.2.3Privileges . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .132.2.4Modes of Operation. . . . . . . . . . . . . . . . . . . . . . . . . .142.2.5Memory Protection Overview . . . . . . . . . . . . . . . . . . . . .152.2.6Assembly Language. . . . . . . . . . . . . . . . . . . . . . . . . .162.3Memory Management. . . . . . . . . . . . . . . . . . . . . . . . . . . . .172.3.1Address and Operand Sizes . . . . . . . . . . . . . . . . . . . . . .172.3.2Segmentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .182.3.2.1Real-Address Mode Segmentation. . . . . . . . . . . . .182.3.2.2Protected Mode Segmentation . . . . . . . . . . . . . . .19v0目录0摘要 i0摘要 iii0目录 v01 引言 1 1.1 背景 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 201.2 动机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 302 x86架构和系统编程概述 7 2.1 x86架构概述 . . . . . . . . . . . . . . . . . . . . . 702.1.2 32位x86架构的特点 . . . . . . . . . . . . . . . . . . . . . 802.2 执行环境 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10viCONTENTS2.3.2.2.1 Segment Descriptor. . . . . . . . . . . . . . . . .192.3.2.2.2 Segmenting the Linear Address Space . . . . . . .212.3.2.2.3 Global Descriptor Table . . . . . . . . . . . . . . .232.3.2.2.4 Segment Selectors. . . . . . . . . . . . . . . . . .232.3.2.2.5 System Descriptors . . . . . . . . . . . . . . . . . .242.3.3Paging . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .252.3.3.1Translation Mechanism . . . . . . . . . . . . . . . . . . .252.3.3.2Memory Isolation. . . . . . . . . . . . . . . . . . . . . .272.3.3.3Identity Paging . . . . . . . . . . . . . . . . . . . . . . . .272.3.3.4Translation Lookaside Buffers. . . . . . . . . . . . . . .282.4Calls, Interrupts and Exceptions. . . . . . . . . . . . . . . . . . . . . . .282.4.1Near Calls . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .292.4.2Far Calls. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .302.4.2.1A Syntactic Digression. . . . . . . . . . . . . . . . . . .302.7ISemantics of Mixed C and x86 Assembly393Introduction414A Minimal C-like Language434.1Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .434.2Labels . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .454.3Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .474.3.1Memory Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . .484.3.2Transition Systems . . . . . . . . . . . . . . . . . . . . . . . . . . .494.3.3Semantics of Lvalues and Expressions. . . . . . . . . . . . . . . .494.3.4Semantics of Statements . . . . . . . . . . . . . . . . . . . . . . . .514.3.4.1Transition Relation. . . . . . . . . . . . . . . . . . . . .524.3.4.1.1 Blocks . . . . . . . . . . . . . . . . . . . . . . . . .524.3.4.1.2 Conditional Branching . . . . . . . . . . . . . . . .534.3.4.1.3 Loop Statements . . . . . . . . . . . . . . . . . . .534.3.4.1.4 Assignments. . . . . . . . . . . . . . . . . . . . .5402.4.2.3 特权级调用 . . . . . . . . . . . . . . . . . . . . . 3102.5 任务 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3402.5.2 任务寄存器 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3502.6 系统调用 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3602.6.2 传递参数 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37CONTENTSvii4.3.4.1.5 Declarations. . . . . . . . . . . . . . . . . . . . .544.3.4.1.6 Return Statements . . . . . . . . . . . . . . . . . .554.3.4.1.7 Function Calls. . . . . . . . . . . . . . . . . . . .564.3.4.2Initial States . . . . . . . . . . . . . . . . . . . . . . . . .574.4Comparison with Real C and Thoughts. . . . . . . . . . . . . . . . . . .584.4.1The Place of Undefined, Unspecified and Implementation-DefinedBehaviors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .584.4.2Desugaring C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .594.4.3A Computability Digression . . . . . . . . . . . . . . . . . . . . . .604.4.4Non-determinism and Memory Usage. . . . . . . . . . . . . . . .615The Assembly Language635.1Structure of x86 Assembly Language . . . . . . . . . . . . . . . . . . . . .645.2Memory Model for Assembly. . . . . . . . . . . . . . . . . . . . . . . . .655.3The Reduced Instruction Set. . . . . . . . . . . . . . . . . . . . . . . . .685.4A Very Concrete Semantics . . . . . . . . . . . . . . . . . . . . . . . . . .695.5A More Symbolic Semantics . . . . . . . . . . . . . . . . . . . . . . . . . .775.6Comparison of Semantics. . . . . . . . . . . . . . . . . . . . . . . . . . .807Pathological and Didactic Examples917.1Assembly Returning from Another Function . . . . . . . . . . . . . . . . .917.2Irregular Usages of Assembly RET . . . . . . . . . . . . . . . . . . . . . . .927.3Dynamic Jump . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .947.4Sub-registers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .977.5Peroration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .988Semantics of Mixed C and Assembly998.1The Formal Language. . . . . . . . . . . . . . . . . . . . . . . . . . . . .998.2Memory Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1038.3Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1058.3.1Where it is Legal to Write . . . . . . . . . . . . . . . . . . . . . . . 1058.3.2Pure C and Pure Assembly Statements. . . . . . . . . . . . . . . 1068.3.2.1Pure Assembly Statements . . . . . . . . . . . . . . . . . 10606 C和汇编的非语义方面 81 6.1 汇编块的语法 . . . . . . . . . . . . . . . . . . . . . . . . . . 8106.2.1 全局变量 . . . . . . . . . . . . . . . . . . . . . . . . . . . 8206.2.3 静态局部变量 . . . . . . . . . . . . . . . . . . . . . . . . . 8306.3 共享符号 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8506.5 调用约定 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87viiiCONTENTS8.3.2.2Pure C Statements . . . . . . . . . . . . . . . . . . . . . . 1078.3.3Entering and Leaving Blocks. . . . . . . . . . . . . . . . . . . . . 1088.3.3.1Entering Blocks. . . . . . . . . . . . . . . . . . . . . . . 1088.3.3.2Leaving Blocks . . . . . . . . . . . . . . . . . . . . . . . . 1098.3.3.3Bridging Blocks. . . . . . . . . . . . . . . . . . . . . . . 1098.3.4Mixed Calls . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1108.3.4.1Calls from C to Assembly . . . . . . . . . . . . . . . . . . 1108.3.4.1.1 Calling. . . . . . . . . . . . . . . . . . . . . . . . 1108.3.4.1.2 Returning . . . . . . . . . . . . . . . . . . . . . . . 1128.3.4.2Calls from Assembly to C . . . . . . . . . . . . . . . . . . 1148.3.4.2.1 Calling. . . . . . . . . . . . . . . . . . . . . . . . 1148.3.4.2.2 Returning . . . . . . . . . . . . . . . . . . . . . . . 1158.3.5Other Control Statements . . . . . . . . . . . . . . . . . . . . . . . 1168.4Summary and Extension . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1179Amical1219.1The x86 Instruction Encoding . . . . . . . . . . . . . . . . . . . . . . . . . 1239.3Disassembling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127IIAbstract Interpretation and the Astrée Analyzer13111 Abstract Interpretation Theory13711.1 Ordering and Lattices. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13711.3 Concretization Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . 14912.2 Reduced Product . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15812.3 Partially Reduced product . . . . . . . . . . . . . . . . . . . . . . . . . . . 15913.2 Composite Abstract Domain. . . . . . . . . . . . . . . . . . . . . . . . . 16513.2.3 The Stack of Domains . . . . . . . . . . . . . . . . . . . . . . . . . 16713.3 The Iterator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16909.2 组装 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12509.4 更简洁的规则组装语法 . . . . . . . . . . . . . . . . 128010 引言 133011.2 Galois 连接框架 . . . . . . . . . . . . . . . . . . . . . . . 145012 抽象域的乘积 155 12.1 示例：需要简化的情况 . . . . . . . . . . . . . . . . . . . . 156013 Astrée 163 13.1 架构概述 . . . . . . . . . . . . . . . . . . . . . . . . . 164013.2.1 非关系型数值域的树 . . . . . . . . . . . . 166 13.2.2 关系型数值域的树 . . . . . . . . . .. . . 167CONTENTSixIIIAbstraction of Mixed C and x86 Assembly17114 Abstraction of Arithmetic and Logic Statements17314.1 Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17314.2 Register Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17514.3 Partitioning According to EFLAGS . . . . . . . . . . . . . . . . . . . . . . 17714.4 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17814.5 Envisaged Improvements . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17914.5.1 Precision Improvements . . . . . . . . . . . . . . . . . . . . . . . . 17914.5.1.1 Reduction of Both Register Representations. . . . . . . 17914.5.1.2 Wrapped Interval Domain . . . . . . . . . . . . . . . . . . 18014.5.2 Performance Optimization . . . . . . . . . . . . . . . . . . . . . . . 18114.5.2.1 Minimizing Partitioning . . . . . . . . . . . . . . . . . . . 18114.5.2.2 Lazy Evaluation of Flags . . . . . . . . . . . . . . . . . . 18215 Stack Abstraction18315.1 Abstracting Stack in a Single Assembly Block . . . . . . . . . . . . . . . . 18315.1.1 Informal Explanation. . . . . . . . . . . . . . . . . . . . . . . . . 18315.1.2 Formal Details. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18615.1.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18715.1.4 Evolution Possibilities . . . . . . . . . . . . . . . . . . . . . . . . . 18715.2 Abstracting Successions of Call Frames . . . . . . . . . . . . . . . . . . . . 18815.2.1 Recall on Mixed Calls and Calling Conventions . . . . . . . . . . . 18815.2.2 The Idea. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19015.2.3 Formalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19115.2.4 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19315.3 Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19416 Other Non-control Statements19516.116.5 String Instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 204016.1.1 作用域 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195016.2 动态代码 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 199016.3 浮点指令 . . . . . . . . . . . . . . . . . . . . . . . . . . 202017 控制语句和迭代器修改 207 17.1 计算目标 . . . . . . . . . . . . . . . . . . . . . . . . . . 207 17.2函数内跳转 . . . . . . . . . . . . . . . . . . . . . . . . . . . 21217.2.2 Handling Assembly Jumps . . . . . . . . . . . . . . . . . . . . . . . 21717.3 Inter-function Near Jumps . . . . . . . . . . . . . . . . . . . . . . . . . . . 21717.4 Mixed Calls . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22417.5 Far Jumps and Task Switches . . . . . . . . . . . . . . . . . . . . . . . . . 225IVA Reduced Product with Ghost Variables22718 Introduction22918.1 Motivation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23018.1.1 Pointers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23018.1.2 GDT Entries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23118.1.3 Linear Combinations of Pointers. . . . . . . . . . . . . . . . . . . 23418.2 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23418.3 Difficulties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23519 Concrete Framework23719.1 Abstraction Level and Expressions . . . . . . . . . . . . . . . . . . . . . . 23719.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24119.3 Ghost Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24419.4 Ghost Constraints. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24720 Generic Abstract Domains and Reduced Product25320.1 Generic Abstract Domain . . . . . . . . . . . . . . . . . . . . . . . . . . . 25320.1.1 A Detailed Execution of an Example with Ghost Variables. . . . 25320.1.2 Generic Abstract Domain Signature. . .
我的内容管理
展开
