SMT Security Policies

Problem Class	Solver	Key APIs	Links
Propositional Logic & SMT	Z3 (@ohtaman/washi/solvers/z3)	m.bool(), m.integer(), implies(), m.constraint(), expr, m.check()	Open in Playground Source Code

Satisfiability Modulo Theories (SMT) combines propositional logic (Boolean SAT) with first-order theories (linear integer arithmetic, real inequalities).

This example demonstrates how to formally verify and deduce system states in an IoT home security system using WaSHI and the Z3 solver engine.

The Scenario

We model a security rule system with sensor readings and logic rules:

1. When ambient light $\le 50$, it implies night time (isNight).
2. When motion is detected at night and the alarm is armed, the siren must sound.
3. If the alarm is armed, the front door must never be unlocked.
4. When motion is detected at night, comfort lights should turn on.

Implementation in WaSHI

import { Model, implies, not, expr } from "@ohtaman/washi";
import "@ohtaman/washi/solvers/z3";

async function verifySecurityRules() {
  const m = new Model({ name: "SmartHomeSecurity", solver: "z3" });

  // 1. Boolean Propositional Variables
  const isNight = m.bool("isNight");
  const motionDetected = m.bool("motionDetected");
  const alarmArmed = m.bool("alarmArmed");
  const frontDoorUnlocked = m.bool("frontDoorUnlocked");
  const sirenActive = m.bool("sirenActive");
  const lightsOn = m.bool("lightsOn");

  // 2. Arithmetic metric (lux sensor)
  const luxLevel = m.integer("luxLevel", { lb: 0, ub: 1000 });

  // Rule 1: luxLevel <= 50 implies isNight
  m.constraint(implies(expr`${luxLevel} <= 50`, isNight), "dark_implies_night");

  // Rule 2: (motionDetected AND isNight AND alarmArmed) => sirenActive
  m.constraint(
    motionDetected.and(isNight).and(alarmArmed).implies(sirenActive),
    "intrusion_rule"
  );

  // Rule 3: alarmArmed => NOT(frontDoorUnlocked)
  m.constraint(alarmArmed.implies(not(frontDoorUnlocked)), "lock_safety_rule");

  // Rule 4: (motionDetected AND isNight) => lightsOn
  m.constraint(motionDetected.and(isNight).implies(lightsOn), "comfort_lights");

  // 3. Observed Context
  m.constraint(expr`${luxLevel} <= 20`, "sensor_reading_dark");
  m.constraint(alarmArmed, "user_armed_alarm");
  m.constraint(motionDetected, "sensor_motion_triggered");

  // Check satisfiability and deduce state
  const res = await m.check({ solver: "z3" });

  console.log(`Status: ${res.status}`);
  console.log(`Siren Active : ${sirenActive.value}`);
  console.log(`Lights On    : ${lightsOn.value}`);
  console.log(`Door Locked  : ${frontDoorUnlocked.value ? "No" : "Yes"}`);
  console.log(`Is Night     : ${isNight.value}`);

  // 4. Formal Safety Verification (Counterexample Search):
  // Prove that the siren CANNOT remain off under these sensor readings
  m.constraint(not(sirenActive), "counterexample_siren_off");
  const proof = await m.check({ solver: "z3" });
  console.log(`Can siren stay off? ${proof.status} (Proven safe when Unsat)`);
  console.log(`Active proof core : ${(proof.conflicts ?? []).join(", ")}`);
}

verifySecurityRules();

Open in Playground →

Practical Notes

• Proof by Refutation (Counterexample Search): A single Sat check shows that a valid assignment exists. To formally prove that a safety property $P$ (such as sirenActive) must hold in every valid state, assert its negation not(P) and verify that m.check() returns "Unsat". If it returns "Sat", the solver's variable values give you a concrete counterexample (security loophole).
• One-Way Implication (implies) vs. Equivalence: In classical logic, implies(expr`${luxLevel} <= 50`, isNight) only constrains isNight when luxLevel <= 50. During daytime (luxLevel > 50), isNight is unconstrained ("open-world" assumption) and could be assigned either true or false unless you also add the converse rule implies(expr`${luxLevel} >= 51`, not(isNight)).