Gardado en:
| Autor Principal: | |
|---|---|
| Formato: | Recurso digital |
| Idioma: | |
| Publicado: |
Zenodo
2026
|
| Acceso en liña: | https://doi.org/10.5281/zenodo.19475806 |
| Tags: |
Engadir etiqueta
Sen Etiquetas, Sexa o primeiro en etiquetar este rexistro!
|
Table of Contents:
- <h1>PySyMex v0.1.0a3</h1> <p>Latest alpha release. Builds on <code>v0.1.0a2</code> by introducing a hardened sandbox architecture that moves isolation from a supporting safeguard into a first-class part of the analysis pipeline. With a dedicated sandbox subsystem, platform-aware backend selection, and sandboxed target loading enabled by default across core CLI workflows, PySyMex closes a major gap between powerful symbolic analysis and safe execution of untrusted targets.</p> <p>This release also includes deeper architectural cleanup across the security stack, expanded formal strictness gates, and multiple soundness and adversarial edge-case fixes across the engine.</p> <h2>What's New</h2> <p><strong>Hardened Sandbox Subsystem (<code>pysymex.sandbox</code>)</strong></p> <ul> <li>Dedicated Sandbox Architecture: Introduces a full <code>pysymex.sandbox</code> package with explicit runner, validation, execution, bridge, and isolation layers, replacing the older monolithic security path with a cleaner and more extensible design.</li> <li>Multi-Backend Isolation Dispatcher: Automatically validates host capabilities and selects the most appropriate sandbox backend. Backends include:<ul> <li><strong>Linux Namespace Backend:</strong> Process isolation, filesystem jailing, and platform-aware containment for strict Linux execution.</li> <li><strong>Windows Job Object Backend:</strong> Hardened Windows process containment with safer startup handling and memory-limit enforcement.</li> <li><strong>Subprocess Compatibility Backend:</strong> Controlled fallback path for environments where stricter isolation modes are unavailable.</li> <li><strong>WASM-Oriented Fallback Path:</strong> Additional compatibility-oriented isolation route for constrained or unsupported hosts.</li> </ul> </li> <li>Fail-Closed Security Posture: Weak backends are rejected by default unless compatibility fallback is explicitly enabled, making secure isolation the architectural default rather than an optional add-on.</li> </ul> <p><strong>Filesystem & Process Containment</strong></p> <ul> <li>Strict Path Sanitization: Sandbox file staging now rejects absolute paths, Windows drive-prefixed paths, traversal markers such as <code>..</code>, and dangerous leading <code>-</code> path segments before any file enters the jail.</li> <li>Resolved-Path Containment Enforcement: Isolation backends verify that resolved output targets remain inside the sandbox root before writes occur, preventing host overwrite through redirection and symlink-style escape tricks.</li> <li>Hardened Resource Controls: Windows sandbox startup paths now include stronger fallback behavior and enforce Job Object memory-limit flags derived from sandbox configuration.</li> </ul> <p><strong>Sandbox-by-Default CLI Integration</strong></p> <ul> <li>Core CLI Sandboxing: <code>scan</code>, <code>verify</code>, and <code>concolic</code> now route target loading and compilation through the sandbox bridge by default.</li> <li>Explicit Trusted-Code Opt-Out: <code>--no-sandbox</code> remains available for trusted local workflows without weakening the secure default path.</li> <li>Sandbox-Aware Scan Heuristics: Scanner worker selection and execution flow were adjusted to stay conservative under sandboxed compilation workloads and reduce avoidable memory spikes.</li> </ul> <p><strong>Architectural Changes & Verification</strong></p> <ul> <li>Separation of Concerns: Validation, harness execution, backend orchestration, and platform-specific isolation are now separated into distinct modules under <code>pysymex/sandbox/</code>, making the containment stack easier to reason about and maintain.</li> <li>Security Architecture References: Added dedicated documentation for the new security and performance architecture, including <code>SANDBOX_SECURITY.md</code>, <code>SMT_SLICING.md</code>, and <code>ROOFLINE.md</code>.</li> <li>Expanded Formal Strictness Gates: Added broader formal verification coverage across solver, detectors, integration, patterns, resources, and loops.</li> </ul> <p><strong>Tests & Stability</strong></p> <ul> <li>Adversarial Sandbox Regression Coverage: Expanded regression tests for escape attempts, backend fallback behavior, startup and cleanup behavior, and containment invariants.</li> <li>CLI Sandbox Routing Tests: Added focused test coverage to ensure sandbox defaults and opt-out flags behave consistently across major command paths.</li> <li>Core Soundness & Edge-Case Fixes: Includes 12 bug fixes across core soundness issues and adversarial edge cases.</li> </ul>