iam-axiom-verifier 0.1.0b3

A Neuro-Symbolic Inference Engine for AWS Security & FinOps — combines LLM routing with Z3 SMT/ILP solvers for formal IAM verification and financial blast radius analysis.

🛡️ IAM Axiom Verifier

A Neuro-Symbolic Inference Engine for AWS Security & FinOps

IAM Axiom Verifier is a mathematical auditing tool for AWS environments. It combines the flexibility of Large Language Models (LLMs) for semantic routing with the absolute rigor of SMT solvers (Formal Verification) to evaluate IAM policies.

Instead of relying on regular expressions, heuristics, or AI hallucinations, this engine translates the AWS state into a system of inequalities and boolean logic, mathematically demonstrating risk vectors.

---

🚨 Disclaimer - Proof of Concept (PoC)

[!CAUTION] This code/application is a proof of concept. It is NOT ready for production. It may contain bugs and SEVERE security vulnerabilities. Its purpose is purely demonstrative and/or experimental.

---

🚨 The Problem

• AI Hallucinates: LLMs cannot reliably reason about complex permission graphs or service quotas. An error in a security audit is unacceptable.
• Static Calculators Fail: Calculating the financial "Blast Radius" of a compromised credential is not a simple summation; it is a combinatorial optimization problem (NP-Hard) crossed with AWS quota constraints and IAM boolean logic.
• Transitive Depth: While the ultimate goal is to implement "infinite depth" reachability analysis (detecting multi-hop privilege escalation), the current implementation operates at Depth = 1. It evaluates direct access based on exact permissions assigned to the specific entity.

---

✨ The Solution (Key Features)

This project implements a "2-in-1" Neuro-Symbolic architecture:

🔒 Module 1: Formal Access Verifier (SAT Solver)

Translates AWS policies (explicit and implicit Allows/Denies) into boolean theorems. It demonstrates if a logical path exists for a role to access a critical resource.

The equation evaluated by Z3: $$Permission_Granted = Has_Allow \land \neg Has_Explicit_Deny$$

💸 Module 2: Financial Blast Radius Optimizer (Max-SAT / ILP)

Cross-references IAM permissions with the offline AWS Pricing catalog and Service Quotas. It uses Integer Linear Programming (ILP) to find the exact combination of instances and regions an attacker would use to inflict maximum economic damage.

The objective function: $$\max C = \sum_{i=1}^{n} (c_i \cdot x_i \cdot P_i)$$

Subject to: $$\sum_{i=1}^{n} (v_i \cdot x_i \cdot P_i) \le Q \quad \land \quad 0 \le x_i \le max_qty_i$$

---

🧠 Architecture (How it works)

The system enforces a strict boundary between probabilistic reasoning (LLM) and deterministic execution (Z3). Furthermore, it is completely offline and air-gapped from the AWS environment during the inference phase.

┌─────────────────────────────────────────────────────────────┐ │ User Question │ └───────────────────────────┬─────────────────────────────────┘ ▼ ┌─────────────────────────────────────────────────────────────┐ │ Layer 1: Intent (LLM - Gemini / OpenAI) │ │ → Semantic Router: extracts role, action, target resource │ │ → Pydantic validates strict JSON (LLMIntent) │ └───────────────────────────┬─────────────────────────────────┘ ▼ ┌─────────────────────────────────────────────────────────────┐ │ Layer 2: Deterministic Fetcher (Local State) │ │ → Reads frozen IAM policies from /data/ JSON fixtures │ │ → Loads local Service Quotas and public prices │ └───────────────────────────┬─────────────────────────────────┘ ▼ ┌─────────────────────────────────────────────────────────────┐ │ Layer 3: Compilation (IAM → SMT) │ │ → Parses IAM JSON to typed PolicyStatements │ │ → Cross-references permissions with offline price catalog │ └──────────┬────────────────────────────────────┬─────────────┘ ▼ ▼ ┌────────────────────────┐ ┌──────────────────────────────┐ │ Layer 4a: SAT Solver │ │ Layer 4b: ILP Solver │ │ Access Verification │ │ Financial Blast Radius │ │ → UNSAT = Impossible │ │ → SAT = Maximum cost │ └────────────────────────┘ └──────────────────────────────┘

---

🔄 Standard Execution Flow (The 2-Step Process)

To adhere to strict security practices, data extraction is completely decoupled from the mathematical inference engine.

Step 1: Extract & Freeze AWS State (Requires Credentials)

First, an auditor uses the standalone extraction tool. This connects to AWS via read-only APIs, downloads the policies and quotas, and freezes them into local JSON files inside the src/data/ directory.

python tools/sync_aws.py --profile axiom-auditor --regions us-east-1 eu-west-1

Step 2: Configure the LLM Router

The engine is provider-agnostic. Copy the .env.example file to .env and configure your preferred AI provider (Google Gemini or OpenAI) to power the Semantic Router. You can also enable a USE_MOCK_LLM="true" mode for completely offline, air-gapped testing.

Step 3: Offline Mathematical Audit (Air-Gapped)

Once the data is frozen and the router is configured, you run the engine. The math engine strictly reads the local JSON state and applies mathematical proofs.

Run the automated demonstration suite

iam-axiom-verifier demo

---

💻 Usage Examples (Interactive CLI)

The package exposes an interactive natural language interface. You can ask complex security questions, and the LLM will translate them into exact parameters for the Z3 SMT solver.

CASE 1: Formal Access Verification (Specific ARNs) You can query if a role has access to specific cloud resources:

iam-axiom-verifier ask "Can junior developers delete the instance arn:aws:ec2:us-east-1:123456789012:instance/i-prod999?"

> ❌ UNSAT: Mathematically proven. The role does not have any Allow

> for 'ec2:TerminateInstances' on that specific ARN.

CASE 2: Financial Damage Optimization (Blast Radius) Ask the engine to calculate the worst-case scenario if a role is compromised:

iam-axiom-verifier ask "If a hacker gets into the DataEng-Team account, what's the worst financial damage they can do?"

> ⚠️ SAT (Max-Cost): Maximum damage is $13,729/day ($572.04/hour).

> Optimal attack vector calculated by Z3:

> → 15× g5.48xlarge ($244.32/h, 2880 vCPUs)

> → 10× p4d.24xlarge ($327.72/h, 960 vCPUs)

---

🔐 AWS Configuration (Least Privilege)

To perform Step 1 (Data Extraction) securely, the tool uses a dedicated IAM user with read-only permissions. Never use your administrator user.

1. Create the permission policy

The file docs/iam-axiom-readonly-policy.json contains the minimum necessary policy.

What the policy DOES allow:

• IAM Role Audit: List roles, view role details, and read attached policies.
• Price Query: Use the AWS Pricing service to obtain details about EC2 costs.
• Quota Query: Review the account's service limits via Service Quotas.
• EC2 Metadata: Describe instance types to dynamically fetch vCPU limits.

What it DOES NOT allow (Implicit restrictions):

• No Modifying anything: It has zero "Write" permissions.
• No Data Plane Access: It cannot access S3 objects, EC2 instances, or RDS databases.
• No Billing Access: It cannot view actual monthly bills or account consumption.

[!CAUTION] This policy is read-only. The extraction tool cannot create, modify, or delete any resource in your AWS account.

2. Configure the local profile

Create an IAM User with the policy above, generate Access Keys for CLI, and run:

aws configure --profile axiom-auditor

---

📂 Project Structure

iam-axiom-verifier/ ├── .env.example # Template for API Keys (Google Gemini / OpenAI) ├── .gitignore # Ignores /venv, pycache, .env and local caches ├── LICENSE # Project license ├── README.md # Main documentation ├── requirements.txt # Strict dependencies ├── engine.py # Entrypoint: Offline Inference Engine & CLI │ ├── tools/ # Utilities requiring internet/credentials │ └── sync_aws.py # Connects to AWS & freezes state to /src/data │ ├── src/ # Core Source Code │ ├── init.py │ ├── models.py # Data Contracts (Pydantic v2) │ ├── aws/ # Layer 2: Deterministic Fetcher (Local JSON) │ │ ├── init.py │ │ ├── fetcher.py # Boto3 logic (Used by tools/sync_aws.py) │ │ └── parser.py # Parses local IAM JSON to typed objects │ ├── core/ # Layers 3-4: Mathematical Inference │ │ ├── init.py │ │ └── smt_solver.py # SAT and ILP engines (Z3) │ └── llm/ # Layer 1: Probabilistic AI │ ├── init.py │ └── router.py # Semantic Router (LLM Translator) │ │ ├── data/ # Local cache and frozen Mocks │ │ ├── policy_devteam.json
│ │ ├── policy_dataeng.json
│ │ └── aws_prices_quotas.json
│ └── docs/ # Technical and security documentation └── iam-axiom-readonly-policy.json

---

🔧 Tech Stack

Component	Technology
Logic Core	z3-solver (Microsoft Research)
Cloud Integration	boto3 (AWS SDK)
AI Router	Google GenAI SDK (gemini-2.5-flash) / OpenAI API
Data Contracts	pydantic v2
Environment	python-dotenv

---

⬇️ Installation

Install the latest beta release from PyPI:

pip install --pre iam-axiom-verifier

[!NOTE] This package is currently in beta. The --pre flag is required to install pre-release versions.

---

⚖️ License

This project is licensed under the MIT License. See the LICENSE file for the full text.

⚠️ Disclaimer

[!CAUTION] This code/application is a proof of concept. It is NOT ready for production. It may contain bugs and SEVERE security vulnerabilities. Its purpose is purely demonstrative and/or experimental.

USE AT YOUR OWN RISK. This software is provided "AS IS", without warranty of any kind, express or implied, including but not limited to the warranties of merchantability, fitness for a particular purpose, and noninfringement. See the MIT License for full terms.

By using this software, you acknowledge and agree that:

1. No Liability. The authors and contributors are not responsible for any security breaches, financial losses, unexpected AWS charges, data loss, or any other damages arising from the use of this tool.

2. Principle of Least Privilege. You must always follow the principle of least privilege when configuring AWS credentials for this tool. Never grant more permissions than strictly necessary. Use the minimal read-only policy provided in docs/iam-axiom-readonly-policy.json.

3. Audit Before Use. You are solely responsible for reviewing, understanding, and validating the code before deploying it in any environment. Do not run this tool against production AWS accounts without first auditing its behavior in a sandboxed environment.

4. Not a Substitute for Professional Security Audits. This tool is intended as a supplementary analysis aid and does not replace a comprehensive security assessment performed by qualified professionals.