Secure code generation improved through counterexample verification feedback
Secure Agentic Coding through Counterexample-Grounded Feedback
Cryptography and SecurityArtificial Intelligence
Summary
Generating secure computer code is hard because tools that check code security can be tricked into thinking code is safe when it is not. The authors propose a new method called Falcon, which separates the search for attacks on the code from checking how the code actually behaves against those attacks. This method uses the code’s execution traces to provide more reliable feedback, helping tools repair security vulnerabilities better while keeping the code functional. Experiments show Falcon works better than other approaches in generating secure and functional code.
What this means in practice
- •For software development teams: Improve automated code generation tools to produce more secure and functional code by integrating counterexample-grounded feedback.
- •For security testing teams: Enhance security verification processes by using execution trace-based feedback to more accurately find and fix vulnerabilities in code.
Authors
Tue Le, Anh Nguyen Hoang, Gabriel Sasseville, Doseok Jang, Pierre-Luc Bacon, Nghi D. Q. Bui
Abstract
As coding models and agent harnesses become more capable, reliable security verification is becoming a central bottleneck. Improving secure code generation requires a signal whose reported progress remains aligned with actual program behavior under optimization; otherwise, an optimizer can improve the signal's verdict without removing the underlying vulnerability. Existing model-based approaches require models to either infer program behavior from source code or specify correct outcomes for adversarial tests, placing substantial reasoning demands on the security signal. We introduce \falcon{}, a counterexample-grounded verification framework that separates attack exploration from behavioral verification and connects them through execution traces of the program under test. In test-time repair, \falcon{} yields substantially stronger held-out functional-security gains than alternative security signals across secure code generation benchmarks, while preserving or improving functionality. As an RL reward, \falcon{} also outperforms static-analysis and learned rewards on held-out functional-security, even when all policies successfully optimize their respective training rewards. Combining \falcon{} with either proxy reward further improves held-out performance, suggesting that execution-grounded feedback can mitigate reward overoptimization while preserving useful guidance from existing security signals.