mirror of
https://github.com/hanzoai/bot-formal-models.git
synced 2026-10-30 18:46:45 +00:00
40 lines
995 B
Plaintext
40 lines
995 B
Plaintext
--------------- MODULE IndirectPromptInjectionBoundaryHarness_BadTaintBypass ---------------
|
|
EXTENDS Naturals
|
|
|
|
(******************************************************************************
|
|
* Negative model:
|
|
* BUG: tainted content bypasses approval and can execute sensitive tools.
|
|
******************************************************************************)
|
|
|
|
VARIABLES
|
|
tainted,
|
|
approved,
|
|
executed
|
|
|
|
Init ==
|
|
/\ tainted \in BOOLEAN
|
|
/\ approved \in BOOLEAN
|
|
/\ executed = FALSE
|
|
|
|
\* BUG: ignores approval entirely
|
|
CanExecuteSensitive == TRUE
|
|
|
|
ExecuteSensitive ==
|
|
/\ ~executed
|
|
/\ CanExecuteSensitive
|
|
/\ executed' = TRUE
|
|
/\ UNCHANGED <<tainted, approved>>
|
|
|
|
NoOp ==
|
|
/\ executed' = executed
|
|
/\ UNCHANGED <<tainted, approved>>
|
|
|
|
Next == ExecuteSensitive \/ NoOp
|
|
|
|
Inv_NoExecFromTaintedWithoutApproval ==
|
|
(tainted /\ ~approved) => ~executed
|
|
|
|
Spec == Init /\ [][Next]_<<tainted, approved, executed>>
|
|
|
|
=============================================================================
|