UC-08 · Aviation use case

Zero-Trust and Formally Assured Architecture

Building drone software architectures with zero-trust patterns, and proving whether attacks are possible with a theorem prover.

TC3CollinsVanderbilt

The problem

High-density urban airspace connects many ground control stations, aircraft, and service suppliers built by different organizations. Security assessments of such systems are traditionally expert reasoning exercises: hard to review, easy to leave undocumented, and costly to repeat whenever the architecture changes.

Our approach

  • Zero-trust design patterns. Collins Aerospace identified new zero-trust patterns for urban airspace (a zero-trust controller, public key infrastructure, a trusted cryptographic engine, and data-leak protection) and updated existing patterns, modeling them in the Architecture Analysis and Design Language (AADL).
  • Assessments you can re-run. Collins and Vanderbilt are building a toolchain in which a large language model proposes candidate theorems about an architecture and the Lean theorem prover checks them. The result is a machine-checked, re-executable argument about whether a specific attack is possible.
  • From analysis to implementation. The same architecture used for attack reasoning also guides deployment on the seL4 microkernel, so what is analyzed is what is built.
  • Explainable assurance. Joint Vanderbilt–Collins work makes explicit why a design meets its requirements and why safety and security concerns are mitigated.

Looking ahead

The team is growing a library of formalized attacks and defenses that supports security analysis across the project’s use cases.

Figures

From the research

Flow from a system architecture into Lean theorems with LLM assistance, producing a yes or no verdict on attack feasibility.
Collins · VanderbiltSecurity assessment as machine-checked proof. An LLM proposes theorems over the architecture and the Lean theorem prover checks them, giving repeatable evidence of whether an attack is possible.
AADL block diagram of a policy enforcement point with engine, admin, and policy manager components.
CollinsA zero-trust policy enforcement point pattern, updated for high-density urban airspace to support dynamic reconfiguration and continuous monitoring.
AADL architecture diagram of a ground station, mission computer, and flight controller with their interfaces.
Collins · VanderbiltRepresentative small UAS architecture modeled in AADL, used both for attack reasoning and to guide deployment on the seL4 microkernel.

Publications

  1. Towards Automated Design-Time Explainability of Assurance Cases and Trade Spaces

    B. Bjorkman, B. C. Ward, S. Hasan

    International Workshop on Explainability of Real-time Systems and their Analysis (ERSA), IEEE RTSS, 2025