FFI / unsafe-boundary obligations (priority hardening)
Goal
FFI / unsafe-boundary obligations (priority hardening). Facet of the UB-disposition model: every miri-enumerated UB class in this section’s scope is dispositioned and (where claimed foreclosed) pinned.
Implementation Sketch
Populate the coverage matrix rows owned by this section; ground every disposition in actual Ori spec/source (cite file:line or spec clause); add the pin / verification surface the disposition claims.
Spec References
- spec Clause 4.5 (04-conformance.md:32) — no silent UB
- missions.md §AIMS, §Compiler
- spec Clause 26 (26-ffi.md) — FFI boundary; Clause 26.5 — Unsafe capability
Cross-plan alignment — plans/ffi-boundary-safety/
This section’s ffi-unsafe-boundary dispositions catalogue the current state (foreclosure stops at the FFI boundary; a real violation is caught by the sanitizer/leak surface). Their compile-time hardening is the deliverable set of plans/ffi-boundary-safety/ (Deep FFI Part 2), which shares this plan’s missions.md §AIMS “memory safety across all surface incl. FFI” anchor. The matrix rows and that plan are kept cross-aligned per the table below; when a ffi-boundary-safety section lands, the corresponding matrix row moves from ffi-unsafe-boundary (boundary-checked) toward foreclosed-typesystem / aims-obligation (compile-time-foreclosed).
| Matrix UB class (this section) | ffi-boundary-safety hardening | Compile-time error |
|---|---|---|
AbiMismatchArgument / AbiMismatchReturn | §02 header signature validation + §03 #verify_layout struct-layout diff | E4016 / E4015 |
ForeignPointerLifetime (returned-pointer UAF) | §04 #borrow_from(p) lifetime check (Locality::Borrowed(p)) | E4018 |
| FFI RC balance (zero spurious RC at the boundary) | §01 AIMS FFI MemoryContract extension | — |
| callback capability UB (a callback using undeclared capabilities) | §05 callback capability subset check | E4019 |
UnterminatedCString / DerefFunctionPointer / InvalidFunctionPointer | §06 FFI-aware diagnostics + the Unsafe-capability boundary (26.5) | E4015–E4025 family |
Reciprocal: plans/ffi-boundary-safety/00-overview.md cross-references this catalogue as the UB-disposition tracking surface for its mission. Edits to either side keep both consistent (the user’s cross-alignment goal).
Work Items
- Enumerate the FFI/unsafe-boundary obligation classes (FFI preconditions, extern unchecked arithmetic, CPtr deref, unsafe-block invariants) and the missing test surface (no CPtr null/dangling tests, no FFI-lifetime tests).
- Wire ASan/UBSan (sanitizer-smoke.sh / sanitizer.rs) + valgrind regressions so each FFI/unsafe obligation class has a test that FAILS on violation; add the missing CPtr/extern regressions.
Fresh intel (regenerated)
{ “schema_version”: 1, “target”: { “kind”: “plan-section”, “ref”: “ub-safety-threat-model/s-05ad0260” }, “generated_at”: “2026-06-25T20:25:14.709348+00:00”, “graph_state”: { “head_sha”: “481a34c7”, “last_code_import_at”: “2026-06-25T20:24:57.773Z”, “embedding_stale”: false, “insights_stale”: false, “cpg_stale”: false }, “surfaces”: {}, “summary”: “intel-package[plan-section:ub-safety-threat-model/s-05ad0260] agent-authored dossier”, “degraded”: false, “dossier”: { “objective_symbols”: [], “tiers”: {}, “agent_authored”: true, “difficulty”: { “class”: “routine”, “research_online”: false, “research_mode”: “auto”, “signals”: [], “plan_dir”: “/home/eric/projects/ori_lang/plans/ub-safety-threat-model” } } }
(full dossier: ffi-unsafe-boundary—s-05ad0260.intel.json)