policy.smt2

;; ------------------------------------------------------------
;; POLICY: RCE Vulnerability Signature
;; ------------------------------------------------------------

;; Rule: A vulnerability exists if:
;; 1. The action is INSERT_OR_UPDATE (we care about new/modified headers)
;; 2. The table is sys_ws_operation (Scripted REST Resource)
;; 3. The script contains a flow from User Input to Dangerous Sink

(declare-const vulnerability_detected Bool)

(assert (= vulnerability_detected
    (and
        (= Action STR_INSERT_OR_UPDATE)
        (= Table STR_SYS_WS_OPERATION)
        script_source_is_user_input
        script_sink_is_dangerous
        script_flow_exists
    )
))

;; Verification Goal: Is the vulnerability detected?
(assert vulnerability_detected)

(check-sat)
(get-model)