LLVM中间表示语言的空间记忆安全的类型依赖系统

可在www.sciencedirect.com在线获取理论计算机科学电子笔记324（2016）3-13www.elsevier.com/locate/entcsTýr：LLVM中空间记忆安全的类型依赖系统Vítor Bujés Ubatuba De Araújoa、Álvaro Freitas Moreiraa和Rodrigo Machadoa信息学研究所-南里奥格兰德联邦大学（UFRGS）Caixa Postal 15.064 - 91.501-970 -阿雷格里港- RS -巴西摘要式本文为LLVM中间表示语言提出了一个类型依赖系统，用于跟踪指针绑定信息。该系统采用了静态分析和运行时检查的组合，以避免空间内存安全漏洞，这是一个很好的缓冲区溢出。 在LLVM上工作IR，该系统为在可以编译的语言中确保空间存储器安全性提供了基础。到LLVM，如C和C++。关键词：空间内存、相关类型、类型安全性、LLVM1介绍性C和C++编程语言不强制执行空间内存安全：它们不保证内存是通过指针访问内存中的一个对象的，因此是一个数组，实际上属于该对象。相反，程序员负责跟踪分配和绑定信息，并确保只有有效的内存访问才能被程序破坏，这是一个很好的解决方案。一方面，它提供了灵活性：程序员可以完全控制内存中数据的布局，以及何时执行检查。另一方面，这是C和C++程序中常见的错误来源，其后果从崩溃和静默数据损坏到安全漏洞（如Heartbleed）不等[7]。已经提出了许多技术来提供C中的存储器安全性[8，11，10]。典型地，这样的系统保持它们自己的边界信息，并指示程序确保存储器安全性没有被破坏。一种名为Deputy [6]的不同方法使用依赖类型来使程序员能够记录在C程序中手动保存的现有绑定信息，以便编译器可以识别它并插入检查以确保其正确使用。因为编译器插入的检查使用与编译器编写的检查相同的元数据。http://dx.doi.org/10.1016/j.entcs.2016.09.0031571-0661/© 2016作者。出版商：Elsevier B.V.这是CC BY许可证（http://creativecommons.org/licenses/by/4.0/）下的开放获取文章。4V.B.U. 来自Araujo等人。/理论计算机科学电子笔记324（2016）3⟨⟩程序员、编译器优化通常可以证明插入的检查是冗余的，从而降低了该技术的性能损失使用CIL框架的代表[12]用于程序转换。由于CIL不支持C++，因此不能使用Deputy来检查C++程序的内存安全性这项工作提出了一个新的系统，称为Týr，它为LLVM的代理提供了类似的功能，LLVM是一个围绕抽象机器的类型化类汇编语言（LLVM IR）设计的语言不可知的编译框架。Týr由LLVM IR的一个依赖类型系统组成，该系统允许将点与其对应的元数据相关联，以及一组对LLVM IR代码的转换，以使其在空间上内存安全。通过在LLVM IR级别提供此功能，Týr可以用作以LLVM为目标的编译器（如Clang[5] C/C++编译器）的空间内存安全的基础。本文档按以下内容组织。第2节介绍了这项工作的背景。第3节介绍LLVM IR语言。第4节描述了所提出的系统、它如何适应LLVM环境以及它实现的类型规则和转换。第5节介绍了结论和未来工作。2背景2.1内存安全性广义地说，如果一个程序只能访问当前分配给某些程序对象的内存区域，则该程序被称为内存安全的。一种语言或环境被说成是内存安全的，如果它保证它的程序是内存安全的。有不同类型的内存安全性。临时内存安全性指的是不尝试访问已被解除分配或尚未分配的内存的属性，而空间内存安全性指的是不尝试访问对象边界之外的内存的属性。[10][11]为每个人提供保险的方法是不同的。此工作仅解决空间存储器安全性问题。其他mecha-nisms，如保守的垃圾收集[4]，可以补充使用来保证C语言中的临时内存安全性在考虑内存安全性时，它的粒度也各不相同。一些作品，如[3]，将整个数据结构视为内存的基本单元，因此，如果访问仍在同一数据结构中，则超过数据结构中字段的限制的访问不被视为违规。这限制了由缓冲区溢出或过读造成的损害，但并不能完全消除它们。其他工作，如副，地址存储器安全在单变量和结构文件的水平。目前的工作使用这个更严格版本的内存安全。2.2相关类型[编辑]依赖类型系统[1]是一个类型可以由at中的术语索引的系统价值水平。对于实例，从属类型使其可以定义一个类型。V ec τ，n表示τ型n个元素的向量。通过允许类型由值参数化，而不是像在参数多态性的情况下那样仅由其他类型参数化，V.B.U. 来自Araujo等人。/理论计算机科学电子笔记324（2016）35依赖类型使我们能够为程序分配更丰富、更精确的类型，从而允许对程序的更多属性进行机械验证，无论是静态验证还是运行时验证。依赖类型系统在其表达度上是不同的一些类型相关的编程语言允许任何表达式出现在类型中，这可能会导致不可判定性，因为表达式可能无法终止[2]。其他语言-允许表达式的子集在类型中使用，因此以牺牲表达性为代价来避免不可判定大多数类型相关的语言都需要类型检查才能在编译时完全发生。这通常是通过限制类型表达式以使它们更适合于静态类型检查来实现的，或者通过在语言中构建一些证明机制来实现的。相比之下，当某些系统无法在编译时检查某些属性时，它们允许将类型检查推迟到运行时。通过这种方式，他们提供了更大的灵活性，而交易或静态保证。2.3副警长Deputy [6]是C编程语言的一个类型依赖系统，它允许可编程人员在其边界上添加相关指针的注释。对于in-stance，函数可以声明为：int f（int* ount（len）数组， intlen）这意味着函数f的数组参数是到透镜积分器的区域的指针。当程序编译时，Deputy会在代码中插入声明，以确保指针在使用之前就在声明的边界内。第二次编译传递，然后查找可以在编译时被证明为真的断言，这些断言可以被安全地删除，从而降低了检查的性能影响。它还查找在编译时可能被证明为假的断言，这些断言被报告为编译时错误给程序员，因此在可能的情况下提供静态检查。可以以依赖类型出现的表达式仅限于局部变量、常量和算术表达式，这些表达式通常是C程序中描述绑定的最佳条件2.4LLVM编译器基础设施的开发LLVM是一个广泛使用的与语言无关的框架，用于程序编译、分析和转换，围绕统一中间表示（LLVM IR）设计，LLVM IR是一种用于抽象机的类类型汇编语言。存在用于将LLVM IR转换为不同体系结构的机器代码的各种后端。使用统一的、定义明确的语言进行代码表示使得用新的解析和转换步骤扩展LLVM相对容易Clang是LLVM项目提供的C/C++编译器。它采用C/C++源代码并发出LLVMIR，然后由LLVM优化并翻译为机器代码图1显示了C语言代码片段的示例及其可能性6V.B.U. 来自Araujo等人。/理论计算机科学电子笔记324（2016）3**int f（int *x，inti）{ int result;如果（i0）结果=i+i：：type类型E-ptR► ►τ：：类型►Llo：Ptr<τ，_，_>►χLhi：Ptr<τ，_，_►Ptr<τ，lo，hi>：：type图6。 格式良好的类型的规则。传递到LLVM汇编程序以生成机器可执行代码。4.2类型系统我们通过用两个新的类型构造函数替换指针类型构造函数，将依赖类型引入LLVM IR语言（图5）。 Ptr τ，lo，hi表示地址lo（包括）和hi（不包括）之间类型τ的元素序列的指针。LocalV ar<τ>表示由alloca语句创建的堆栈中类型为τ的局部变量的指针可以表现为指针类型的边界的表达式类型仅限于常量、寄存器、堆栈中的局部变量，以及涉及整数和指针的算术表达式（见图1）。它排除了指向非本地数据的任意指针，因为以其他方式跟踪依赖于值的变异将需要完全混叠信息，即，将变异跟踪到依赖于值的变异将需要完全混叠信息。可以统计地告诉任何两个指针指向同一个存储器区域的位置。图6显示了类型的良好形式的规则。最后两条规则是平凡的：它们说i32是一个有效类型，并且可以从任何类型τ构造一个LocalV ar τ类型。第三条规则表示类型τ的指针必须由类型τ的其他指针绑定，这可能是使用本地环境Gamma的表达式，但指针的基类型必须在空环境中有效。[10][11]这个限制已经存在于Deputy中，是必要的，因为一般（非LocalV ar）指针可以逸出它们创建的函数，因此在局部变量的作用域之前;此外，我们需要完美的混叠信息来确保我们可以找到所有这样的逸出指针，当它们的类型通过它所依赖的局部变量的变异而失效时。4.3类型检查。图7显示了可能出现在从属类型中的表达式的类型规则。图8显示了相关指针类型的类型规则llvm-ptr-10V.B.U. 来自Araujo等人。/理论计算机科学电子笔记324（2016）3▶⟨⟩L本地-INT►Ln：i32l本地-ptR-aRItH本地-RE gΓ（%r）=τL%r：τ本地化-添加►Le1：i32►Le2：i32►Le1+e2：i32►χLe1：Ptr<τ，lo，hi►χLe2：i32►χLe1e2：Ptr<τ，lo，hilOCAL-lOCALVAR-dERE f►Le：LocalV ar<τ>## ：τ图。7. 从属类型表达式的类型规则IV M-INTn：i32LLV M-CMP-INTLlV m-REgΓ（%r）=τγ%r：τllV m-Int-aRI tH第1集：第32第2集：第32►Gamma%r= addval1，val2：i32LLV M-CMP-PTR第1集：第32第2集：第32Ω%r=cmp或 pval1，val2：i1llV m-ptR-aRI tH第1集：Ptr<τ，_，_第2章：Ptr<τ，_，_Ω%r=cmp或 pval1，val2：i1第1集：Ptr<τ，lo，hi>第2集：i32►Gamma%r=getelementptrval1，val2：Ptr<τ，lo，hi>我会的，我会的。L1V M-LO D►Gammaval：Ptr<τ，lo，hi>Ω%r=有效载荷值：τυval/=0≤val≥lo ≤valhiΩ%r=有效载荷值：τ第1集：τ第二章：Ptr<τ，lo，hi第1版，第2版val2/= 0≤val2 ≥lo ≥val2

下载后可阅读完整内容，剩余1页未读，立即下载