From 283c4780e4507dc12c1b8a5bef11deb212aee357 Mon Sep 17 00:00:00 2001 From: Robert Allan James Date: Fri, 14 Aug 2026 14:09:41 -0400 Subject: [PATCH] proof/: add StarForth_System_Words.thy (system_words.c coverage) 10 of 16 registered words modeled (COLD/WARM/BYE/WORDS/VLIST/PAGE/NOP/ QUIT/ABORT/EXECUTE guard-shape), plus the internal (ABORT") runtime helper. Deferred: ( and \ (TIB dependency), SAVE-SYSTEM (real file I/O), 79-STANDARD (reads a non-per-VM global), ABORT" compile-time half (TIB + codegen), SEE (TIB + raw threaded-code pointer walk). Two findings. (1) system_running/forth_79_standard are file-scope C statics doing per-VM-shaped work -- the 5th and 6th occurrence of this bug pattern in the sweep (previously: control_words.c's cf_stack, dictionary_manipulation_words.c's state_variable, string_words.c's word_scratch_addr). (2) EXECUTE casts a popped FORTH cell straight to a DictEntry host pointer and calls through it (entry->func(vm)), gated only by a null check -- same hazard class as format_words.c's ?/DUMP but far more consequential since EXECUTE is a core, ubiquitous primitive rather than a diagnostic word. Flagged as the highest-severity finding this sweep has produced. --- proof/ROOT | 1 + proof/StarForth_System_Words.thy | 311 +++++++++++++++++++++++++++++++ 2 files changed, 312 insertions(+) create mode 100644 proof/StarForth_System_Words.thy diff --git a/proof/ROOT b/proof/ROOT index c638666..57969f8 100644 --- a/proof/ROOT +++ b/proof/ROOT @@ -18,6 +18,7 @@ session "StarForth" = "HOL-Library" + StarForth_IO_Words StarForth_Editor_Words StarForth_Format_Words + StarForth_System_Words StarForth_Mutex StarForth_Transition StarForth_Loop1_Heat diff --git a/proof/StarForth_System_Words.thy b/proof/StarForth_System_Words.thy new file mode 100644 index 0000000..5c03bb6 --- /dev/null +++ b/proof/StarForth_System_Words.thy @@ -0,0 +1,311 @@ +theory StarForth_System_Words + imports StarForth_Base +begin + +(* ========================================================================= + POST-14: System Words + Mirrors: src/word_source/system_words.c (16 registered words, plus the + internal (ABORT") runtime helper) + + ── Genuine finding, not fixed: two MORE file-scope C statics doing + per-VM-shaped work (5th and 6th occurrence of this pattern) ───────── + `system_running` (written by every COLD/WARM via `reset_vm_state`) and + `forth_79_standard` (read by `79-STANDARD`) are both `static int` at + file scope in system_words.c -- not `struct VM` fields. Same bug class + already found in control_words.c's `cf_stack`, dictionary_manipulation_ + words.c's `state_variable`, and string_words.c's `word_scratch_addr` + (StarForth_Control_Words.thy, StarForth_Dictionary_Manipulation_Words.thy, + StarForth_String_Words.thy) -- in the Tripod multi-VM fleet, one VM's + COLD silently resets every other VM's "is the system running" flag, and + 79-STANDARD reports one shared compliance flag for all VMs regardless + of which one asked. Five occurrences now; still worth the aggregated + write-up the earlier files' notes flagged. Neither is modeled below + (not per-VM state, nothing in vm_state corresponds to it) -- + `forth_79_standard` is instead threaded through as an explicit + parameter, see `forth_79_standard_word` below. + + ── Genuine finding, not fixed: EXECUTE dereferences a raw host pointer + from an attacker-controlled FORTH cell -- the most consequential + instance of this sweep's raw-pointer-cast pattern ───────────────── + `system_word_execute` casts the popped cell straight to a `DictEntry` + host pointer (a C-style pointer cast, same shape as format_words.c's + `?`/`DUMP`) then calls `entry->func(vm)` -- an indirect function-pointer + CALL through + a pointer built directly from a popped FORTH cell, gated only by a null + check. This is the same category as format_words.c's `?`/`DUMP` + (StarForth_Format_Words.thy) and this file's own `SEE`/`system_word_see` + (which walks compiled threaded-code the same way), but strictly worse: + `?`/`DUMP` are diagnostic corner words; EXECUTE is a core, ubiquitous + FORTH-79 primitive (used by `'`/`DEFER`/every indirect-call idiom). Any + FORTH code that computes, corrupts, or is tricked into supplying a bad + "xt" value gets an unchecked indirect call through it -- not just an + out-of-bounds read (the format_words.c findings) but arbitrary-code- + execution shaped. Worth flagging to Bob as the highest-severity finding + this sweep has produced so far. Also a plumbing/model mismatch: this + suite's `word_table :: nat \ vm_state \ vm_state` (StarForth_Base.thy) + models dispatch as word_id-indexed, but EXECUTE's real dispatch is via + raw DictEntry pointers smuggled through cell_t values, not word_ids -- + the two dispatch pictures don't actually correspond for this word. + + MODELED (10 words): COLD, WARM, BYE, WORDS, VLIST, PAGE, NOP, QUIT, + ABORT, EXECUTE (guard shape only, not dispatch), plus the internal + `(ABORT")` runtime helper. + + NOT MODELED (7 words), each for a documented reason: + - `(` / `\` (comments): parse via `vm_parse_word`/`input_pos` -- the + same TIB/input-subsystem dependency string_words.c already deferred. + - `SAVE-SYSTEM`: real host filesystem I/O (`fopen`/`fwrite` to + "forth_system.img") -- entirely outside vm_state. + - `79-STANDARD`: reads the file-scope static, see finding above. + - `ABORT"` (compile-time immediate half): TIB-dependent message parsing + PLUS compile-time codegen (`vm_allot`/`vm_compile_literal`/ + `vm_compile_call`), the same category as control_words.c's deferred + compile-time half. Its interpret-mode runtime companion, `(ABORT")`, + IS modeled (it has no TIB dependency -- flag/addr/len already on the + stack by the time it runs). + - `SEE`: TIB-dependent name parsing PLUS a raw-pointer threaded-code + walk (same hazard class as EXECUTE, see finding above). + - `REBOOT`: guard clauses modeled (see `forth_reboot_guards_*` below); + the effectful tail is platform-branching -- real UEFI NVRAM writes + and `ResetSystem` on `__STARKERNEL__` (genuine hardware I/O, no + vm_state analog at all), vs. `vm_halted := True` on the hosted build + (modeled, see `reboot_hosted_success_halts`). + ======================================================================== *) + +(* ── reset_vm_state helper (shared by COLD/WARM/ABORT/(ABORT")) ─────────── *) + +definition reset_vm_state :: "bool \ vm_state \ vm_state" where + "reset_vm_state cold_start vm = + (let vm1 = vm\data_stack := [], return_stack := [], + vm_error := False, vm_mode := ModeInterpret\ + in if cold_start \ here vm1 > 1024 then vm1\here := 1024\ else vm1)" + +lemma reset_vm_state_clears_stacks: + "data_stack (reset_vm_state c vm) = []" + "return_stack (reset_vm_state c vm) = []" + by (simp_all add: reset_vm_state_def Let_def) + +lemma reset_vm_state_clears_error_and_interprets: + "vm_error (reset_vm_state c vm) = False" + "vm_mode (reset_vm_state c vm) = ModeInterpret" + by (simp_all add: reset_vm_state_def Let_def) + +lemma reset_vm_state_warm_preserves_here: + "here (reset_vm_state False vm) = here vm" + by (simp add: reset_vm_state_def Let_def) + +lemma reset_vm_state_cold_clamps_here: + assumes "here vm > 1024" + shows "here (reset_vm_state True vm) = 1024" + using assms by (simp add: reset_vm_state_def Let_def) + +lemma reset_vm_state_cold_preserves_small_here: + assumes "here vm \ 1024" + shows "here (reset_vm_state True vm) = here vm" + using assms by (simp add: reset_vm_state_def Let_def) + +(* ── COLD / WARM ( -- ) ───────────────────────────────────────────────── *) + +definition forth_cold :: "vm_state \ vm_state" where + "forth_cold vm = reset_vm_state True vm" + +definition forth_warm :: "vm_state \ vm_state" where + "forth_warm vm = reset_vm_state False vm" + +lemma cold_is_reset_true: "forth_cold vm = reset_vm_state True vm" + by (simp add: forth_cold_def) +lemma warm_is_reset_false: "forth_warm vm = reset_vm_state False vm" + by (simp add: forth_warm_def) + +(* ── BYE ( -- ) ───────────────────────────────────────────────────────── *) + +definition forth_bye :: "vm_state \ vm_state" where + "forth_bye vm = vm\vm_halted := True\" + +lemma bye_halts: "vm_halted (forth_bye vm) = True" + by (simp add: forth_bye_def) +lemma bye_preserves_stacks: + "data_stack (forth_bye vm) = data_stack vm" + "return_stack (forth_bye vm) = return_stack vm" + by (simp_all add: forth_bye_def) + +(* ── WORDS / VLIST / PAGE / NOP ( -- ) : pure I/O or true no-ops ────────── *) + +definition forth_words :: "vm_state \ vm_state" where "forth_words vm = vm" +definition forth_vlist :: "vm_state \ vm_state" where "forth_vlist vm = vm" +definition forth_page :: "vm_state \ vm_state" where "forth_page vm = vm" +definition forth_nop :: "vm_state \ vm_state" where "forth_nop vm = vm" + +lemma words_is_identity: "forth_words vm = vm" by (simp add: forth_words_def) +lemma vlist_is_identity: "forth_vlist vm = vm" by (simp add: forth_vlist_def) +lemma page_is_identity: "forth_page vm = vm" by (simp add: forth_page_def) +lemma nop_is_identity: "forth_nop vm = vm" by (simp add: forth_nop_def) + +(* ── 79-STANDARD ( -- flag ) : reads a non-per-VM global, see finding ───── *) +(* Threaded through as an explicit parameter rather than pretending it's + vm_state, since it genuinely is not (file-scope C static). *) + +definition forth_79_standard_word :: "bool \ vm_state \ vm_state" where + "forth_79_standard_word compliant vm = + vm\data_stack := (if compliant then forth_true else forth_false) # data_stack vm\" + +lemma standard_pushes_flag: + "data_stack (forth_79_standard_word compliant vm) = + (if compliant then forth_true else forth_false) # data_stack vm" + by (simp add: forth_79_standard_word_def) + +(* ── QUIT ( -- ) : IMMEDIATE, forbidden inside a compiling definition ───── *) + +definition forth_quit :: "vm_state \ vm_state" where + "forth_quit vm = + (if vm_mode vm = ModeCompile then set_error vm + else vm\return_stack := [], vm_mode := ModeInterpret, vm_error := False\)" + +lemma quit_in_compile_mode_errors: + assumes "vm_mode vm = ModeCompile" + shows "vm_error (forth_quit vm)" + using assms by (simp add: forth_quit_def set_error_def) + +lemma quit_in_interpret_mode_resets: + assumes "vm_mode vm = ModeInterpret" + shows "return_stack (forth_quit vm) = []" + and "vm_mode (forth_quit vm) = ModeInterpret" + and "vm_error (forth_quit vm) = False" + using assms by (simp_all add: forth_quit_def) + +lemma quit_preserves_data_stack: + "data_stack (forth_quit vm) = data_stack vm" + by (simp add: forth_quit_def set_error_def) + +(* ── ABORT ( -- ) : full reset + abort_req flag, NOT an error ───────────── *) + +definition forth_abort :: "vm_state \ vm_state" where + "forth_abort vm = (reset_vm_state False vm)\abort_req := True\" + +lemma abort_sets_abort_req: + "abort_req (forth_abort vm) = True" + by (simp add: forth_abort_def) +lemma abort_clears_error: + "vm_error (forth_abort vm) = False" + by (simp add: forth_abort_def reset_vm_state_def Let_def) +lemma abort_clears_stacks: + "data_stack (forth_abort vm) = []" + "return_stack (forth_abort vm) = []" + by (simp_all add: forth_abort_def reset_vm_state_def Let_def) + +(* ── (ABORT") runtime ( flag addr len -- ) : interpret-only stack helper ── *) +(* Address/length bounds check inlined the same way StarForth_IO_Words.thy's + TYPE does (concrete VM_MEMORY_SIZE comparison), not the Memory_Words.thy + `valid_addr` placeholder (which is unconditionally True and would make + the bounds-fail branch unreachable in this model). *) + +definition forth_runtime_abortq :: "vm_state \ vm_state" where + "forth_runtime_abortq vm = + (case data_stack vm of + len # addr # flag # rest \ + if flag = 0 then vm\data_stack := rest\ + else if addr len word_of_nat VM_MEMORY_SIZE data_stack := rest\) + else (reset_vm_state False (vm\data_stack := rest\)) + | _ \ set_error vm)" + +lemma runtime_abortq_underflow: + assumes "length (data_stack vm) < 3" + shows "vm_error (forth_runtime_abortq vm)" + using assms + by (auto simp add: forth_runtime_abortq_def set_error_def split: list.split) + +lemma runtime_abortq_false_flag_is_noop_pop: + assumes "data_stack vm = len # addr # 0 # rest" + shows "data_stack (forth_runtime_abortq vm) = rest" + and "vm_error (forth_runtime_abortq vm) = vm_error vm" + using assms by (simp_all add: forth_runtime_abortq_def) + +lemma runtime_abortq_bounds_fail_errors: + assumes "data_stack vm = len # addr # flag # rest" "flag \ 0" + assumes "addr len word_of_nat VM_MEMORY_SIZE 0" + assumes "\ (addr len word_of_nat VM_MEMORY_SIZE vm_state" where + "forth_execute vm = + (case data_stack vm of + [] \ set_error vm + | xt # rest \ + if xt = 0 then set_error (vm\data_stack := rest\) + else vm\data_stack := rest\) \ \indirect call via raw pointer, unmodelled -- see finding\" + +lemma execute_underflow: "data_stack vm = [] \ vm_error (forth_execute vm)" + by (simp add: forth_execute_def set_error_def) +lemma execute_null_xt_errors: + "data_stack vm = 0 # rest \ vm_error (forth_execute vm) \ data_stack (forth_execute vm) = rest" + by (simp add: forth_execute_def set_error_def) +lemma execute_pops_one: + "data_stack vm = xt # rest \ data_stack (forth_execute vm) = rest" + by (simp add: forth_execute_def) + +(* ── REBOOT ( addr len -- ) : guards modeled; hosted success tail modeled ─ *) + +definition KERNEL_ARGS_CMDLINE_MAX :: nat where "KERNEL_ARGS_CMDLINE_MAX = 512" + \ \○ CODE-MUST-MATCH: #define KERNEL_ARGS_CMDLINE_MAX 512 in + include/starkernel/kernel_args.h\ + +definition forth_reboot_guards_ok :: "vm_state \ bool" where + "forth_reboot_guards_ok vm = + (vm_mode vm \ ModeCompile \ length (data_stack vm) \ 2 \ + (case data_stack vm of len # addr # _ \ + 0 len + \ (addr len word_of_nat VM_MEMORY_SIZE False))" + +(* No single total `forth_reboot` is defined -- only the guard predicate + and the two named error/success facts below -- since the effectful tail + genuinely branches on a compile-time #ifdef that has no single vm_state + transition to name. The four REBOOT guard-failure facts, each + independent of the others: *) + +lemma reboot_guard_compile_mode: + "vm_mode vm = ModeCompile \ \ forth_reboot_guards_ok vm" + by (simp add: forth_reboot_guards_ok_def) + +lemma reboot_guard_underflow: + "length (data_stack vm) < 2 \ \ forth_reboot_guards_ok vm" + by (simp add: forth_reboot_guards_ok_def) + +lemma reboot_guard_len_range: + assumes "data_stack vm = len # addr # rest" + assumes "\ (0 len forth_reboot_guards_ok vm" + using assms by (auto simp add: forth_reboot_guards_ok_def) + +lemma reboot_guard_addr_bounds: + assumes "data_stack vm = len # addr # rest" + assumes "addr len word_of_nat VM_MEMORY_SIZE forth_reboot_guards_ok vm" + using assms by (auto simp add: forth_reboot_guards_ok_def) + +(* Hosted-build success tail (the `#else` branch of the C `#ifdef + __STARKERNEL__`): prints a stub message, then halts. The kernel-build + branch (EFI NVRAM write + ResetSystem) has no vm_state analog and is + not modeled at all. *) + +definition forth_reboot_hosted_tail :: "vm_state \ vm_state" where + "forth_reboot_hosted_tail vm = vm\data_stack := drop 2 (data_stack vm), vm_halted := True\" + +lemma reboot_hosted_success_halts: + assumes "forth_reboot_guards_ok vm" + shows "vm_halted (forth_reboot_hosted_tail vm) = True" + using assms by (simp add: forth_reboot_hosted_tail_def) + +end