• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IEEE/ACM International Conference on Software Engineering >IntEQ: Recognizing Benign Integer Overflows via Equivalence Checking across Multiple Precisions
【24h】

IntEQ: Recognizing Benign Integer Overflows via Equivalence Checking across Multiple Precisions

机译：Intiq：通过多个诊断识别良性整数溢出溢出溢出

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Integer overflow (IO) vulnerabilities can be exploited by attackers to compromise computer systems. In the meantime, IOs can be used intentionally by programmers for benign purposes such as hashing and random number generation. Hence, differentiating exploitable and harmful IOs from intentional and benign ones is an important challenge. It allows reducing the number of false positives produced by IO vulnerability detection techniques, helping developers or security analysts to focus on fxing critical IOs without inspecting the numerous false alarms. The difficulty of recognizing benign IOs mainly lies in inferring the intent of programmers from source code. In this paper, we present a novel technique to recognize benign IOs via equivalence checking across multiple precisions. We determine if an IO is benign by comparing the effects of an overflowed integer arithmetic operation in the actual world (with limited precision) and the same operation in the ideal world (with sufficient precision to evade the IO). Specifically, we first extract the data flow path from the overflowed integer arithmetic operation to a security-related program point (i.e., sink) and then create a new version of the path using more precise types with sufficient bits to represent integers so that the IO can be avoided. Using theorem proving we check whether these two versions are equivalent, that is, if they yield the same values at the sink under all possible inputs. If so, the IO is benign. We implement a prototype, named IntEQ, based on the GCC compiler and the Z3 solver, and evaluate it using 26 harmful IO vulnerabilities from 20 real-world programs, and 444 benign IOs from SPECINT 2000, SPECINT 2006, and 7 real-world applications. The experimental results show that IntEQ does not misclassify any harmful IO bugs (no false negatives) and recognizes 355 out of 444 (about 79.95%) benign IOs, whereas the state of the art can only recognize 19 benign IOs.
机译：攻击者可以利用整数溢出（IO）漏洞来危及计算机系统。与此同时，iOS可以由程序员故意用于良性目的，例如散列和随机数生成。因此，从故意和良性的人中区分利用和有害的iOS是一个重要的挑战。它允许减少IO漏洞检测技术产生的误报的数量，帮助开发人员或安全分析师专注于fxing关键iOS而不检查众多误报。认识到良性iOS的难度主要是推断从源代码中推断程序员的意图。在本文中，我们提出了一种新颖的技术来通过跨多个精度的等价检查来识别良性IOS。我们通过比较IO通过比较实际世界中的溢出整数算术运算的影响（具有有限的精度）和理想世界中的操作（具有足够的精度来避开IO）来确定IO是否是良性的。具体地，我们首先将来自溢出的整数算术运算的数据流路径提取到安全相关的节目点（即，inrin），然后使用具有足够位的更精确的类型来创建新版本的路径来表示整数，以表示IO。可以避免。使用定理证明我们检查这两个版本是否等同，即，如果它们在所有可能的输入下在接收器处产生相同的值。如果是这样，IO是良性的。我们根据GCC编译器和Z3求解器实现名为INTEQ的原型，并使用来自20个现实世界的26个有害的IO漏洞进行评估，444个良性IOS来自Specint 2000，Specint 2006和7个现实世界应用程序。实验结果表明，INTEQ不会错误分类任何有害的IO虫（没有假否定），并认可444中的355名（约79.95％）良性IOS，而最先进的国家只能识别19个良性iOS。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号