Mathematical Engine

System Architecture & Solver Pipeline

Discover how PosturaNet translates cloud architecture policies into first-order logic formulas. We mathematically verify safety properties using Z3 theorem solvers.

Core Engine Pipeline

Verification Pipeline Visualizer

Click through the pipeline nodes below to trace how raw code gets compiled and attested.

PIPELINE STATE VIEW

IaC Ingress Parsing

Engine stack: Terraform Parser, AWS SDK

resource "aws_security_group" "db" {
  name   = "db-sg"
  vpc_id = aws_vpc.main.id

  ingress {
    from_port   = 3306
    to_port     = 3306
    protocol    = "tcp"
    cidr_blocks = ["0.0.0.0/0"] # Open database exposure
  }
}

Pipeline status: active, latency 2.4s

Interactive Sandbox

SMT solver code comparative workspace

Compare raw infrastructure-as-code (Terraform) with its compiled SMT-LIB logic equations, and run the solver check.

Terraform configuration (Input)

resource "aws_security_group" "rds_sg" {
  name        = "rds-prod-sg"
  description = "Permit database ingress"
  vpc_id      = aws_vpc.prod.id

  ingress {
    description = "MySQL Port"
    from_port   = 3306
    to_port     = 3306
    protocol    = "tcp"
    cidr_blocks = ["0.0.0.0/0"] # VULNERABILITY: Public databases must be private
  }
}

Compiled Z3 SMT-LIB constraints

; SMT-LIB Equation Set
(declare-const db_port Int)
(declare-const ingress_cidr String)
(declare-const db_exposed Bool)

(assert (= db_port 3306))
(assert (= ingress_cidr "0.0.0.0/0"))

; Security Invariant: Public access to database is forbidden
(assert (= db_exposed (and (= db_port 3306) (= ingress_cidr "0.0.0.0/0"))))
(assert db_exposed) ; Query solver to verify if this state is reachable

(check-sat)
(get-model)

Z3 Logic Engine Output

Click "Execute Z3 Logic Verification" to compile, verify, and run solver proof assertions.