NTT Paper Accepted for CAV 2026, a Premier International Conference in Formal Verification

A paper from NTT Laboratories has been accepted for presentation at the 38th International Conference on Computer Aided Verification (CAV 2026), which will be held in Lisbon, Portugal, from July 26 to 29, 2026. CAV is one of the premier international conferences in the field of formal verification, where cutting-edge research is presented on technologies for mathematically and automatically verifying that hardware and software operate correctly and safely as designed, including model checking, theorem proving, static analysis, and program verification. CAV 2026 is also known as a highly selective conference, receiving 311 submissions and accepting approximately 26% of them.

Repairing Regex-Dependent String-Manipulation Programs

Nariyoshi Chida, Distinguished Researcher, NTT Social Informatics Laboratories; and Tachio Terauchi, Waseda University

Background

The emergence of generative AI has accelerated the discovery and exploitation of vulnerabilities, creating a greater need than ever for rapid responses (*1). Automated repair using generative AI is one effective approach, but it may introduce unintended changes, making it essential to ensure the quality of repair results. Technologies are therefore needed that can quickly identify the causes of vulnerabilities and generate repairs that align with developers’ intent.

Research Results

This research establishes a technology that automates the process from root-cause identification to repair for errors in string-manipulation programs that may lead to information leakage and other vulnerabilities. In conventional automated repair technologies, automating root-cause identification, which accounts for approximately 46.3% of repair work (*2), has been a challenge. The proposed technology enables developers to concisely describe their intended behavior for how input strings should be processed and output by using a specification called “origin.” For example, by specifying that “the input password must not be included in the output,” developers can clearly express processing requirements that are difficult to capture with ordinary test cases alone. When a vulnerability is discovered, the technology identifies the processing step that caused the problem based on this specification and automatically generates a repair candidate that is consistent with the developer’s intent. Through this process, it automates the workflow from identifying the cause of vulnerabilities arising from string manipulation to repairing them, thereby enabling both rapid response and reliable repair quality.

Future Outlook

Going forward, NTT will expand the range of vulnerabilities to which this technology can be applied and work toward realizing technologies that can automatically repair vulnerabilities while ensuring the quality of repair results in software development that leverages generative AI.

^*1National Cyber Office (NCO), Project YATA-Shield 20260518_AI_CS_gaiyou.pdf

^*2https://arxiv.org/pdf/2103.12447