Update Set Formal Verifier

This is a proof-of-concept tool to detect Remote Code Execution (RCE) patterns in ServiceNow Update Sets using formal verification (SMT2/Z3) rather than regex.

Note

This is a personal project created in my free time using my own resources. It is NOT an official ServiceNow project or product.

How it works

1. Parse: verifier.js extracts potentially dangerous JavaScript from the XML update set.
2. Analyze: It converts the script's logic into an SMT2 model (model.smt2), specifically tracking if user input flows to dangerous sinks (like eval or GlideScopedEvaluator).
3. Verify: We pass this model + a safety policy (policy.smt2) into the Z3 theorem prover.
   • sat = Vulnerability Found.
   • unsat = Safe.

Usage

Prerequisites

• Node.js
• Z3 (installed and in your path)

Running the Verifier

# 1. Generate the SMT model from your update set
node verifier.js path/to/update_set.xml > model.smt2

# 2. Check against the policy
cat definitions.smt2 model.smt2 policy.smt2 | z3 -in

Files

• verifier.js: The "compiler" that turns XML/JS into SMT logic.
• definitions.smt2: Shared types and constants.
• policy.smt2: The definition of what constitutes an RCE vulnerability.
• rce_update_set.xml: A vulnerable example file.
• safe_update_set.xml: A safe example file.