Repairing DoS Vulnerability of Real-World Regexes

Repairing DoS Vulnerability of Real-World Regexes
复制标题

DOI:
10.1109/sp46214.2022.9833597
复制
发表时间:
2020-10
期刊:
2022 IEEE Symposium on Security and Privacy (SP)
影响因子:
--
通讯作者:
Nariyoshi Chida;Tachio Terauchi
Nariyoshi Chida;Tachio Terauchi
中科院分区:
其他
文献类型:
--
作者:
Nariyoshi Chida;Tachio Terauchi

文献摘要

相似文献

在从示例合成和修复正则表达式(简称正则表达式)方面已经做了很多工作。这些按示例编程(PBE)方法通过让用户通过示例反映他们的意图来帮助用户编写正则表达式。然而,现有的方法可能会生成正则表达式,其匹配可能需要超线性时间,并且容易受到正则表达式拒绝服务(Redos)攻击。本文提出了第一种PBE修复方法,该方法保证只产生抗毁性的正则性。重要的是,我们的方法可以处理包含环回和反向引用的真实正则表达式。由于这些扩展,现有的只考虑纯正则表达式的redos漏洞的正式定义是不够的。因此,我们首先给出了一种新的形式语义和现实世界正则表达式回溯匹配算法的复杂性,并在此基础上首次给出了现实世界正则表达式重做漏洞的形式定义。接下来,我们提出了一个新的条件,称为实世界强1-无歧义,它充分保证了真实世界正则表达式的抗毁性,并形式化了相应的PBE修复问题。最后,我们给出了一个解决修复问题的算法。该算法建立并扩展了以前的PBE方法,以处理现实世界的扩展,并使用约束来实施现实世界的强1-无二义性条件。
There has been much work on synthesizing and repairing regular expressions (regexes for short) from examples. These programming-by-example (PBE) methods help the users write regexes by letting them reflect their intention by examples. However, the existing methods may generate regexes whose matching may take super-linear time and are vulnerable to regex denial of service (ReDoS) attacks. This paper presents the first PBE repair method that is guaranteed to generate only invulnerable regexes. Importantly, our method can handle real-world regexes containing lookarounds and backreferences. Due to the extensions, the existing formal definitions of ReDoS vulnerabilities that only consider pure regexes are insufficient. Therefore, we first give a novel formal semantics and complexity of backtracking matching algorithms for real-world regexes, and with them, give the first formal definition of ReDoS vulnerability for real-world regexes. Next, we present a novel condition called real-world strong 1-unambiguity that is sufficient for guaranteeing the invulnerability of real-world regexes, and formalize the corresponding PBE repair problem. Finally, we present an algorithm that solves the repair problem. The algorithm builds on and extends the previous PBE methods to handle the realworld extensions and with constraints to enforce the real-world strong 1-unambiguity condition.