August 31st Research Briefing

Contents

1. Drishti: audit a 5G core until the AMF dies
2. PolyFlow: taint that crosses a language boundary
3. liblzma in VST: the kernel checks the proof

Drishti: audit a 5G core until the AMF dies

Researchers audited Open5GS and free5GC with Drishti, an AI-led, human-directed method, until the process died.

This matters because the scarce work is verification, reachability, impact, and whether a shipped patch actually closes the class, not whether models find more candidates.

Three findings:

1. A pre-authentication NULL dereference in the Open5GS NRF multipart parser. The maintainer fixed it. The authors requested a CVE from MITRE.
2. An ASN.1-PER memory amplification in free5GC's NGAP decoder. A 2-byte malformed NGSetupRequest from a rogue gNodeB made the AMF OOM-kill in 6.2 seconds (256 MB cgroup, 48 workers).
3. The v1.2.3 patch for CVE-2025-69248 stops the original AMF panic, then adds a defense-in-depth check that never runs. Two coding errors make the block dead on the pre-authentication path. Seven unit tests accept inputs the new check was meant to reject.

Authors: Sriram Ramachandran, Levente Csikor, and Dinil Mon Divakaran (paper, pdf). Csikor: GitHub, LinkedIn. Divakaran: LinkedIn. Workshop: 8th Joint Workshop on CPS & IoT Security and Privacy, The Hague, 2026.

PolyFlow: taint that crosses a language boundary

PolyFlow recovered source-to-sink taint paths across Python-C and Java-C, and the paper reports 17 previously unknown cross-language vulnerabilities that none of the baselines found.

This matters because static analyzers usually stop at a foreign-function call, and dynamic tools only see the tests you ran. PolyFlow keeps a cross-language control-flow graph, asks models only for the language features that graph cannot see (Python decorators, C function pointers, Java reflection), and checks those answers with a multi-model panel.

On 29 real Python-C and Java-C systems, the authors report 76.8% precision on recovered source-to-sink paths. One assigned CVE they cite is CVE-2025-55562. Another is a confirmed aubio fix (PR). The paper also ships xFlowBench, a micro-benchmark with ground-truth cross-language flows.

Authors: Haoran Yang, Zhixuan Zhong, Jiawei Guo, and Haipeng Cai (paper, pdf). Cai: GitHub, LinkedIn, ORCID.

liblzma in VST: the kernel checks the proof

Researchers verified decoder pieces of liblzma (the library under xz-utils) in the Verified Software Toolchain, proving existing production C.

This matters because AI agents close proof goals, while humans still own models and function contracts. The Rocq kernel checks the terms. 22 closed semax_body theorems cover the LZMA2 state machine, the LZMA1 core, the outer path, and the sliding-window dictionary. The largest body, lzma_decode, is 338 source lines and 183,268 lines of proof script.

The proof also exposed undefined behavior on the raw LZMA1 zero-input path: range-decoder macros add zero to a null pointer and subtract two null pointers. That is outside C's defined pointer arithmetic. The 2024 xz backdoor (CVE-2024-3094) was a supply-chain attack, not this class of bug. The authors are measuring a different trust problem: whether the decoder itself is memory-safe under a stated contract.

Authors: Prokhor Shlyakhtun, Alexander Gryzlov, Vladimir Kukharenko, Vasilii Nesterov, Nikolai Vasiliev, Kirill Ziborov, Eugene Zolotarev, and Alex Pokras (paper, pdf, artifact).