> ## Documentation Index
> Fetch the complete documentation index at: https://docs.alchemicalchef.io/llms.txt
> Use this file to discover all available pages before exploring further.

# Introduction

> Documentation for enterprise security, architecture mapping, and incident response tools

First off, welcome to my site.

The purpose of this site is to highlight my research and cover the tools and frameworks I've built to help secure enterprise environments, map infrastructure dependencies, and practice incident response.

The blog is mostly my rants and areas of research.

Each tool is open source, MIT Licensed, and designed to address what I understand to be real gaps in enterprise security workflows. Since I specialize in identity systems and binary analysis, a lot of my work is centered in those areas, but occasionally I venture into other areas of research.

Where applicable, you'll find formal specifications alongside the code to mathematically verify security properties.

## Available Tools

<CardGroup cols={2}>
  <Card title="AD Tier Model" icon="shield-halved" href="/ad-tier-model/overview">
    Implement Microsoft's tiered administrative model to reduce privilege escalation risk.
  </Card>

  <Card title="AD Security Audit" icon="magnifying-glass" href="/ad-tier-model/security-audit">
    Comprehensive security auditing for privilege escalation, Kerberos, and ADCS vulnerabilities.
  </Card>

  <Card title="Dependency Mapping" icon="diagram-project" href="/process-tools/dependency-mapping">
    Visualize and manage component interconnections across your enterprise architecture.
  </Card>

  <Card title="Tabletop Exercises" icon="users" href="/tabletop-framework/overview">
    Create and conduct cybersecurity tabletop exercises based on CISA standards.
  </Card>

  <Card title="Formal Models" icon="square-root-variable" href="/formal-models/overview">
    Mathematical specifications proving tier model safety using TLA+ and Alloy.
  </Card>
</CardGroup>

## Why Formal Verification?

Unlike traditional testing that can only find bugs, formal verification mathematically proves that security properties hold. As an example, the AD Tier Model includes [TLA+ specifications](/formal-models/tla-specification) for verifying temporal safety invariants and [Alloy specifications](/formal-models/alloy-specification) for detecting privilege escalation attack paths. As does most of the tools that I've built, some don't make sense to model out, but for those that do you'll always find one included with it (eventually, it is time intensive)

## Quick Links

<CardGroup cols={2}>
  <Card title="AD Tier Model Manager" icon="github" href="https://github.com/AlchemicalChef/ADTierModel-Rust">
    Desktop application for managing tiered administration in Active Directory.
  </Card>

  <Card title="AD Security Audit" icon="github" href="https://github.com/AlchemicalChef/ADSecurityAudit-Rust">
    Comprehensive AD security auditing platform built with Rust and React.
  </Card>

  <Card title="Dependency Mapping Tool" icon="github" href="https://github.com/AlchemicalChef/DependencyMappingTool">
    Desktop application for mapping enterprise architecture dependencies.
  </Card>

  <Card title="Tabletop Framework" icon="github" href="https://github.com/AlchemicalChef/Tabletop-Framework">
    Electron app for running cybersecurity tabletop exercises.
  </Card>
</CardGroup>