fix(z3): close string-based evasions of the AST attribute denylist

QA probes found two solver-code escapes that pass the gate and execute:
z3.__dict__['__builtins__']['__import__']('os').system(...) and
z3.__getattribute__('__spec__').loader... — __dict__/__getattribute__
turn every denied attribute into a constant-string lookup, and a
module's __dict__ exposes its real __builtins__ (dir(z3) contains
__builtins__, so the namespace dump in execute_code_in_process()
already replaces the restricted builtins with the full ones).
getattr/setattr reach the same attributes via constant strings and
resolve at runtime.

- Deny getattr/setattr/delattr calls
- Deny __dict__/__getattribute__/__getattr__/__setattr__/__delattr__
  attributes
- Add 6 regression tests (suite: 35 passed); allow-cases unchanged

Author: akushonkamen

optillm/z3_solver.py

@@ -20,21 +20,26 @@ class TimeoutException(Exception):
 # exactly the modules execute_code_in_process() makes available.
 _ALLOWED_SOLVER_IMPORTS = {'z3', 'sympy', 'math', 'itertools', 'fractions'}
 
-# Calls that provide arbitrary execution or file/IO access; the declared
-# solver subset has no use for any of them.
+# Calls that provide arbitrary execution or file/IO access, or that reach the
+# same denied attributes through string arguments (getattr/setattr/delattr);
+# the declared solver subset has no use for any of them.
 _DENIED_SOLVER_CALLS = {
     'eval', 'exec', 'compile', '__import__', 'open', 'input', 'breakpoint',
-    'globals', 'locals', 'vars',
+    'globals', 'locals', 'vars', 'getattr', 'setattr', 'delattr',
 }
 
 # Dunder attributes used in classic module-object traversal escapes (e.g.
-# z3.__loader__, ().__class__.__bases__[0].__subclasses__()). A fixed
-# denylist instead of banning every dunder so legitimate solver code that
-# touches z3/sympy internals by name is not rejected.
+# z3.__loader__, ().__class__.__bases__[0].__subclasses__()). __dict__ and
+# __getattribute__ are denied because they turn every other denied attribute
+# into a string lookup (z3.__dict__['__loader__'],
+# z3.__getattribute__('__spec__')), and a module's __dict__ exposes its real
+# __builtins__. A fixed denylist instead of banning every dunder so legitimate
+# solver code that touches z3/sympy internals by name is not rejected.
 _DENIED_SOLVER_ATTRS = {
     '__class__', '__bases__', '__subclasses__', '__mro__', '__globals__',
     '__builtins__', '__init__', '__code__', '__closure__', '__loader__',
-    '__spec__', '__import__', '__reduce__',
+    '__spec__', '__import__', '__reduce__', '__dict__', '__getattribute__',
+    '__getattr__', '__setattr__', '__delattr__',
 }
 
 def _validate_solver_ast(tree: ast.AST) -> None:

tests/test_z3_solver_guard.py

@@ -60,6 +60,16 @@ def _response(content, completion_tokens=10):
     ("sympy.__spec__", "__spec__"),
     ("f = z3.Bool.__init__", "__init__"),
     ("import z3\nz3.__builtins__", "__builtins__"),
+    # String-based evasions of the attribute denylist (QA finding): getattr
+    # reaches the same objects via a constant argument, and __dict__ /
+    # __getattribute__ turn every dunder into a string lookup. A module's
+    # __dict__ also exposes its real __builtins__.
+    ("getattr(z3, '__loader__')", "getattr()"),
+    ("setattr(z3, '__loader__', None)", "setattr()"),
+    ("delattr(z3, 'Int')", "delattr()"),
+    ("z3.__dict__['__builtins__']['__import__']('os')", "__dict__"),
+    ("z3.__getattribute__('__spec__')", "__getattribute__"),
+    ("sympy.__getattr__('_load')", "__getattr__"),
 ])
 def test_guard_rejects(code, violation):
     with pytest.raises(ValueError) as excinfo: