Robert Allan James
422ef2fa29
Isabelle toolchain replaced (was genuinely 2011, 14+ years stale) and every theory file fixed to actually compile -- most had apparently never been checked under a working Isabelle at all. Fixed the vm_state self-reference in StarForth_Base.thy properly (word_table is now a free-standing global constant, not a circular record field), corrected the word_physics_transparent axiom (was claiming full state equality from mere exec-equivalence, provably too strong), and worked through 14 years of HOL-Library drift plus several missing-hypothesis bugs across the physics-loop and ACL theories. Two genuine (non-tactical) bugs found and left oops-flagged rather than silently resolved: forth_roll's index arithmetic disagrees with both its own test lemma and the real C ROLL implementation (three-way inconsistency), and pm_wf isn't actually preserved by pm_record_hit/pm_record_miss. Both need a decision, not a proof-script fix. Full writeup in FABRIC-2.md item 5.2.
152 lines
7.1 KiB
Plaintext
152 lines
7.1 KiB
Plaintext
theory ACL_Emergency_Bypass
|
|
imports ACL_Pin_Monotone
|
|
begin
|
|
|
|
(* =========================================================================
|
|
ACL_Emergency_Bypass — emergency_console=True OR zuse_session=True
|
|
bypasses ALL ACL checks
|
|
|
|
Mirrors: include/vm.h (VM.emergency_console, VM.zuse_session)
|
|
src/vm.c (execute_colon_word, vm_interpret_word ACL guards)
|
|
src/vm.c (acl_recheck — sets emergency_console=1 on entry)
|
|
src/word_source/starforth_words.c (ZUSE-AUTHENTICATE sets zuse_session=1)
|
|
capsules/zuse.4th (ACL-ZUSE-BOOT calls ZUSE-AUTHENTICATE)
|
|
|
|
Two bypass conditions exist:
|
|
(a) emergency_console=1: fault handler / acl_recheck re-entrancy guard;
|
|
written only by C (acl_recheck, sk_repl); active during error recovery.
|
|
(b) zuse_session=1: superuser authenticated; written only by the
|
|
ZUSE-AUTHENTICATE C primitive; grants god-mode — all ACL checks skipped.
|
|
|
|
○ CODE-MUST-MATCH: src/vm.c execute_colon_word:
|
|
if (w && !vm->emergency_console && !vm->zuse_session) {
|
|
if (w->acl_ttl == 0) acl_recheck(vm, w);
|
|
else w->acl_ttl--;
|
|
if (!w->acl_allow) { ... vm->error = 1; return; }
|
|
}
|
|
|
|
○ CODE-MUST-MATCH: src/vm.c vm_interpret_word:
|
|
if (!vm->emergency_console && !vm->zuse_session) { ... ACL check ... }
|
|
|
|
○ CODE-MUST-MATCH: src/vm.c acl_recheck():
|
|
uint8_t saved_ec = vm->emergency_console;
|
|
vm->emergency_console = 1;
|
|
... call ACL-RECHECK ...
|
|
vm->emergency_console = saved_ec;
|
|
Restores emergency_console on exit; does NOT touch zuse_session.
|
|
|
|
⚠ HUMAN-REVIEW: Verify that acl_recheck() always restores emergency_console
|
|
to saved_ec even when ACL-RECHECK itself errors (the error-recovery path
|
|
in acl_recheck must include the restore).
|
|
======================================================================== *)
|
|
|
|
(* =========================================================================
|
|
Section 1: ACL check model
|
|
======================================================================== *)
|
|
|
|
(* Model of the two-level ACL check that guards each word execution.
|
|
Returns True iff execution is permitted.
|
|
Both emergency_console and zuse_session independently bypass all checks. *)
|
|
definition acl_check_permits :: "vm_state \<Rightarrow> dict_entry \<Rightarrow> bool" where
|
|
"acl_check_permits vm e \<longleftrightarrow>
|
|
emergency_console vm \<or> zuse_session vm \<or> de_acl_allow e"
|
|
|
|
(* =========================================================================
|
|
Section 2: Emergency bypass lemmas
|
|
======================================================================== *)
|
|
|
|
(* Core guarantee: when emergency_console is True, every word is permitted
|
|
regardless of its acl_allow field. *)
|
|
lemma emergency_bypass_unconditional:
|
|
"emergency_console vm = True \<Longrightarrow>
|
|
acl_check_permits vm e = True"
|
|
by (simp add: acl_check_permits_def)
|
|
|
|
(* Denied word (acl_allow=False) becomes permitted under emergency_console. *)
|
|
lemma denied_word_permitted_under_emergency:
|
|
"emergency_console vm = True \<Longrightarrow>
|
|
de_acl_allow e = False \<Longrightarrow>
|
|
acl_check_permits vm e = True"
|
|
by (simp add: acl_check_permits_def)
|
|
|
|
(* =========================================================================
|
|
Section 2b: Zuse session bypass lemmas
|
|
======================================================================== *)
|
|
|
|
(* Core guarantee: when zuse_session is True, every word is permitted
|
|
regardless of its acl_allow field (god-mode). *)
|
|
lemma zuse_bypass_unconditional:
|
|
"zuse_session vm = True \<Longrightarrow>
|
|
acl_check_permits vm e = True"
|
|
by (simp add: acl_check_permits_def)
|
|
|
|
(* Denied word becomes permitted under zuse_session. *)
|
|
lemma denied_word_permitted_under_zuse:
|
|
"zuse_session vm = True \<Longrightarrow>
|
|
de_acl_allow e = False \<Longrightarrow>
|
|
acl_check_permits vm e = True"
|
|
by (simp add: acl_check_permits_def)
|
|
|
|
(* Either bypass condition alone is sufficient for full permission. *)
|
|
lemma either_bypass_sufficient:
|
|
"(emergency_console vm = True \<or> zuse_session vm = True) \<Longrightarrow>
|
|
acl_check_permits vm e = True"
|
|
by (auto simp: acl_check_permits_def)
|
|
|
|
(* Without either bypass, the word's own acl_allow is definitive. *)
|
|
lemma no_bypass_check_follows_allow:
|
|
"emergency_console vm = False \<Longrightarrow>
|
|
zuse_session vm = False \<Longrightarrow>
|
|
acl_check_permits vm e = de_acl_allow e"
|
|
by (simp add: acl_check_permits_def)
|
|
|
|
(* Legacy alias kept for backward compatibility with existing proof scripts *)
|
|
lemma no_emergency_check_follows_allow:
|
|
"emergency_console vm = False \<Longrightarrow>
|
|
zuse_session vm = False \<Longrightarrow>
|
|
acl_check_permits vm e = de_acl_allow e"
|
|
by (simp add: acl_check_permits_def)
|
|
|
|
(* =========================================================================
|
|
Section 3: acl_recheck re-entrancy protection
|
|
======================================================================== *)
|
|
|
|
(* Model of emergency_console save/restore around an ACL-RECHECK call.
|
|
○ CODE-MUST-MATCH: acl_recheck() saves, sets True, runs RECHECK, restores. *)
|
|
definition with_emergency_bypass :: "vm_state \<Rightarrow> (vm_state \<Rightarrow> vm_state) \<Rightarrow> vm_state" where
|
|
"with_emergency_bypass vm f =
|
|
(let saved = emergency_console vm
|
|
in (f (vm\<lparr>emergency_console := True\<rparr>))\<lparr>emergency_console := saved\<rparr>)"
|
|
|
|
(* Save/restore is transparent: emergency_console returns to its original value. *)
|
|
lemma emergency_bypass_restores:
|
|
"emergency_console (with_emergency_bypass vm f) = emergency_console vm"
|
|
by (simp add: with_emergency_bypass_def Let_def)
|
|
|
|
(* All other VM fields modified by f are preserved (the save/restore only
|
|
touches emergency_console). *)
|
|
lemma emergency_bypass_preserves_stacks:
|
|
"data_stack (with_emergency_bypass vm f) =
|
|
data_stack (f (vm\<lparr>emergency_console := True\<rparr>))"
|
|
by (simp add: with_emergency_bypass_def Let_def)
|
|
|
|
(* Nested calls: with_emergency_bypass is safe to nest; the inner call sets
|
|
emergency_console=True (already True), and outer save/restore still works. *)
|
|
lemma emergency_bypass_idempotent_on_console:
|
|
"with_emergency_bypass (vm\<lparr>emergency_console := True\<rparr>) f =
|
|
(f (vm\<lparr>emergency_console := True\<rparr>))\<lparr>emergency_console := True\<rparr>"
|
|
by (simp add: with_emergency_bypass_def Let_def)
|
|
|
|
(* =========================================================================
|
|
Section 4: Invariant — bypass cannot escalate acl_pinned
|
|
======================================================================== *)
|
|
|
|
(* The bypass only affects the CHECK (execution gate); it cannot change any
|
|
ACL field of any DictEntry. Dictionary state is unchanged by the bypass
|
|
mechanism itself (though the executed FORTH code may change it). *)
|
|
lemma emergency_bypass_preserves_dictionary:
|
|
"dictionary (with_emergency_bypass vm (\<lambda>v. v)) = dictionary vm"
|
|
by (simp add: with_emergency_bypass_def Let_def)
|
|
|
|
end
|