Core Verification

Bedrock

Formal proof below the OS.

Formal vulnerability analysis for firmware, bootloaders, UEFI drivers, and embedded MCU code — the attack surface below operating system visibility. Bedrock lifts binary or C source to extract function call graphs, then applies Z3 to prove stack overflow conditions, unsafe call paths, and integer arithmetic failures in memory operations.

UEFI

DXE Drivers

MCU

Embedded

angr

Binary Lift

§ SPECIFICATION

Input

Firmware binary (ELF / UEFI PE32+ / raw) or C source
Optional: base address for raw firmware
Optional: known safe call whitelist

Constraints Verified

MCU stack safety: call depth ≤ 32 frames (4KB stack)
Unsafe libc calls without bounds enforcement
Integer overflow in size × count allocation patterns
UEFI protocol interface safety

Output

Call graph with dangerous function paths
Stack depth overflow proofs per function
Integer overflow in allocation arithmetic
Unsafe call inventory (strcpy, gets, sprintf, etc.)
Wick-compatible firmware proof artifact

§ SAMPLE PROOF ARTIFACT

ARTIFACT // BDR-UEFI-01FAILURE DETECTED

// SAMPLE PROOF — BEDROCK ENGINE

UEFI DXE driver — stack overflow via deep call chain

TargetCustom UEFI DXE driver

Conditioncall_depth = 47 > MAX_SAFE_DEPTH (32) on 4KB MCU stack

VerdictSAT

SummaryStack overflow reachable in firmware init path. Witness: chain depth 47, budget 32.

StatusReview-ready

→ View full artifact repository

§ FIELD VALIDATION

#	Target	Vulnerability Class	Status
01	UEFI DXE Driver Stack Overflow	Stack Overflow	Z3 Proof
02	MCU Firmware Integer Overflow	Integer Overflow	Alloc Path

Run Bedrock on your system.

Formal engagement starts with a technical intake. We scope, configure, and deliver a proof artifact within the agreed SLA.

Request Briefing →