Deeply nested input raises uncaught `RecursionError` in v0.14.6 and earlier (fixed in v0.15.0 by #448)

[LukeW1999]

Summary

In amazon.ion 0.14.6 and earlier, a deeply nested Ion value makes simpleion.load/loads raise an uncaught RecursionError when the pure-Python reader is used. #448, released in v0.15.0, fixed this: the same input now raises IonException.

The v0.15.0 release notes list #448 as a behaviour change. They do not say that it affects applications that parse untrusted Ion, so users of earlier versions have no signal to upgrade. This issue asks for that to be made explicit.

Affected

• Versions: 0.14.6 and earlier. We tested 0.14.6 on CPython 3.10.12 with the default recursion limit.
• The pure-Python reader is affected. simpleion.load/loads uses it when a catalog is passed, even if the C extension is installed. It is also used when the C extension is unavailable or disabled.
• The default C-extension path without a catalog rejects the same input with IonException and is not affected.

Reproduction

import amazon.ion.simpleion as s
from amazon.ion.symbols import SymbolTableCatalog

text = "[" * 5000 + "]" * 5000  # valid Ion, about 10 KB

s.loads(text)                                # IonException (C extension)
s.loads(text, catalog=SymbolTableCatalog())  # 0.14.6: RecursionError
                                             # 0.15.0: IonException

The input is valid Ion, so the failure is not limited to malformed data. Nested annotation wrappers in binary Ion reach the same failure through reader_binary.py.

Impact

A caller that deserialises untrusted Ion and handles only IonException does not catch the error, so the thread or request fails. RecursionError is a subclass of RuntimeError, so a caller with a broad except survives. We therefore see this as a denial-of-service concern of limited severity rather than a critical one.

Role of formal verification

We found the defect by reading reader_binary.py and confirmed it by running crafted payloads against the unmodified library. We then modelled the recursive descent in _annotation_handler and checked it with the ESBMC bounded model checker (8.4.0, Python frontend, Bitwuzla and Z3 agreeing).

• The recursion has no bound. On the model of the shipped code, ESBMC's recursion unwinding assertion fails with no property written by us. Its counterexample chooses an annotation wrapper at every level, which is the payload that crashes the real library.
• A depth cap removes the failure for every input. On the same model with a maximum depth added, k-induction returns a proof that no input exceeds the limit. The result is not limited to inputs up to a fixed depth.

The proof covers a model with a depth cap, not the #448 implementation, which catches RecursionError and re-raises it as IonException. The model uses a small stand-in for CPython's recursion limit to keep the check tractable. We are happy to share the models.

Requests

1. Add a note to the v0.15.0 release, or publish a GitHub security advisory, saying that users who parse untrusted Ion should upgrade.
2. If an advisory is published, please credit the reporters listed below.

Background

We reported this privately to AWS Security on 27 August 2026, following CONTRIBUTING.md. AWS Security validated the report and referred it to the Amazon CNA. #448 was merged on 10 September and released in v0.15.0 on 11 September. We are opening this issue because the fix is now public and no advisory or upgrade guidance has followed.

Weiqi Wang (University of Manchester)
Lucas C. Cordeiro (University of Manchester)

[tgregg]

Security advisory: GHSA-93q6-f8hx-vv7f