Skip to main content
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

AD Tier Model

Implement Microsoft’s tiered administrative model to reduce privilege escalation risk.

AD Security Audit

Comprehensive security auditing for privilege escalation, Kerberos, and ADCS vulnerabilities.

Dependency Mapping

Visualize and manage component interconnections across your enterprise architecture.

Tabletop Exercises

Create and conduct cybersecurity tabletop exercises based on CISA standards.

Formal Models

Mathematical specifications proving tier model safety using TLA+ and Alloy.

​
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 for verifying temporal safety invariants and Alloy specifications 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)

AD Tier Model Manager

Desktop application for managing tiered administration in Active Directory.

AD Security Audit

Comprehensive AD security auditing platform built with Rust and React.

Dependency Mapping Tool

Desktop application for mapping enterprise architecture dependencies.

Tabletop Framework

Electron app for running cybersecurity tabletop exercises.