Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Recurso digital |
| Langue: | |
| Publié: |
Zenodo
2026
|
| Sujets: | |
| Accès en ligne: | https://doi.org/10.5281/zenodo.19040720 |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866901073012195328 |
|---|---|
| author | Musselman, Blake |
| author_facet | Musselman, Blake |
| contents | <p>We identify and characterize a class of verification blind spots in AST-pattern-based static analysis tools: safety-critical constraints that become invisible when program semantics shift from control flow to arithmetic. Using three benchmark programs that encode division-by-zero protection, forbidden-value filtering, and bounded state cycling without any conditional branching, we demonstrate that a representative constraint scanner -- which successfully detects all three constraints in their branched equivalents -- finds zero constraints in the branchless forms. Z3 SMT proofs confirm mathematical equivalence between each branchless program and its branched counterpart, establishing that the constraints are preserved in the code's semantics but lost in the tool's detection model. We formalize the control-flow assumption, present a taxonomy of constraint survivability, survey five widely-used tools that share the blind spot, and demonstrate a dual-sort AST-to-Z3 conversion technique that recovers full constraint visibility.</p> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_19040720 |
| institution | Zenodo |
| language | |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Verification Blind Spots: When Branchless Code Defeats Static Analysis Musselman, Blake static analysis branchless programming SMT solving software safety constraint detection <p>We identify and characterize a class of verification blind spots in AST-pattern-based static analysis tools: safety-critical constraints that become invisible when program semantics shift from control flow to arithmetic. Using three benchmark programs that encode division-by-zero protection, forbidden-value filtering, and bounded state cycling without any conditional branching, we demonstrate that a representative constraint scanner -- which successfully detects all three constraints in their branched equivalents -- finds zero constraints in the branchless forms. Z3 SMT proofs confirm mathematical equivalence between each branchless program and its branched counterpart, establishing that the constraints are preserved in the code's semantics but lost in the tool's detection model. We formalize the control-flow assumption, present a taxonomy of constraint survivability, survey five widely-used tools that share the blind spot, and demonstrate a dual-sort AST-to-Z3 conversion technique that recovers full constraint visibility.</p> |
| title | Verification Blind Spots: When Branchless Code Defeats Static Analysis |
| topic | static analysis branchless programming SMT solving software safety constraint detection |
| url | https://doi.org/10.5281/zenodo.19040720 |