{"id":"palomar/PALOMAR-2026-10-23-000008","url":"https://github.com/GregoryMorse/smcdynirredloops/tree/41400824a9980a186a4f481c9a9075d44dea42fc/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000008-v1.json","repo":"https://github.com/GregoryMorse/smcdynirredloops","tags":["cs.CR","cs.LO","msc:68N30","msc:68R10","msc:94A60","program-analysis","control-flow-obfuscation","formalization"],"score":0,"title":"Control flow obfuscation with irreducible loops and self-modifying code","trust":"high","domain":"cs.CR","source":"palomar","authors":["Gregory Morse"],"reviews":0,"subject":"cs.CR","summary":"Lean 4 development (no Mathlib) of the mathematics, algorithms and security statements of Morse, Alqaradaghi and Kozsik, \"Control flow obfuscation with irreducible loops and self-modifying code\": a self-modifying-code solver for 2-SAT and the planted instance generator as an algorithm, the extremal numbers of irreducible loops and multiple-entry edges (the families Kn and Mn), the irreducible-loop transformations of Figures 5 and 6, the Boolean control-flow graphs of AES, and the security statements of Section 5.1 relative to an explicit structural threat model. Two Challenges are submitted…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"Control flow obfuscation with irreducible loops and self-modifying code","identifier":"doi:10.5486/PMD.2022.Suppl.5","relationship":"adapts"}]}