Formally Verifying Undetectability in Hidden Communication Systems with Maude-HCS

Submitted by Katie Dey on

ABSTRACT

A hidden communication system (HCS) embeds hidden messages within ordinary network activity by repurposing existing protocols as subliminal channels. Although prior work provides useful tools for assessing the detectability of the HCS, there is no general and modular framework that both formalizes what it means for an HCS to be undetectable and formally verifies that a concrete implementation satisfies this property.

Autonomous Formal Methods

Submitted by Katie Dey on

ABSTRACT

In this talk I will describe HOARDE — the Hierarchical Orchestration of Autonomous Rigorous Digital Entities — built by my company, Sigil Logic, since our founding in September, 2025. HOARDE realizes what we call the NINJA methodology (Non-Intrusive Judicious Assurance): rigorous engineering with applied formal methods, made accessible to every engineering team through AI agents.

Subscribe to