一句话:提出 FlashRegex 框架,从示例合成或修复出抗 ReDoS 的正则表达式。
正则表达式广泛用于编程语言、字符串处理和数据库,但已有合成/修复工具未考虑 ReDoS 漏洞:若正则具有超线性最坏复杂度,攻击者可构造输入触发拒绝服务。本文提出基于示例编程的框架 FlashRegex,首次将正则合成与修复同 ReDoS 感知结合。它通过降低正则歧义,并借助布尔可满足性(SAT)或邻域搜索(NS)推导抗 ReDoS 正则。作者与五个先进工具对比:现有工具在数秒至一小时内生成了多达 394 个易受攻击正则,而 FlashRegex 约五秒内未生成超线性正则;修复易受攻击正则时,修复后抗 ReDoS 正则比现有工具和人类专家多 4 个,且无需裁剪或重排序,体现通用性、自动化与易用性。
Regular expressions (regexes) are widely used in different fields of computer science such as programming languages, string processing and databases. However, existing tools for synthesizing or repairing regexes were not designed to be resilient to Regex Denial of Service (ReDoS) attacks. Specifically, if a regex has super-linear (SL) worst-case complexity, an attacker could provide carefully-crafted inputs to launch ReDoS attacks. Therefore, in this paper, we propose a programming-by-example framework, FlashRegex, for generating anti-ReDoS regexes by either synthesizing or repairing from given examples. It is the first framework that integrates regex synthesis and repair with the awareness of ReDoS-vulnerabilities. We present novel algorithms to deduce anti-ReDoS regexes by reducing the ambiguity of these regexes and by using Boolean Satisfiability (SAT) or Neighborhood Search (NS) techniques. We evaluate FlashRegex with five related state-of-the-art tools. The evaluation results show that our work can effectively and efficiently generate anti-ReDoS regexes from given examples, and also reveal that existing synthesis and repair tools have neglected ReDoS-vulnerabilities of regexes. Specifically, the existing synthesis and repair tools generated up to 394 ReDoS-vulnerable regex within few seconds to more than one hour, while FlashRegex generated no SL regex within around five seconds. Furthermore, the evaluation results on ReDoS-vulnerable regex repair also show that FlashRegex has better capability than existing repair tools and even human experts, achieving 4 more ReDoS-invulnerable regex after repair without trimming and resorting, highlighting the usefulness of FlashRegex in terms of the generality, automation and user-friendliness.