Collins · Cedar Rapids, IA

Collins Aerospace

Industry partner contributing aerospace expertise, zero-trust architecture patterns, and formally verified security assessment.

Zero-trust design patternsFormal methodsLean theorem provingAvionics expertise

Collins Aerospace is the project’s industry partner, represented by Isaac Amundson and Heber Herencia-Zapana. Collins contributes aerospace subject-matter expertise and focuses on security assessment for high-density urban airspace: zero-trust design patterns for UAS architectures, and a toolchain that pairs large language models with the Lean theorem prover so that security reasoning is captured formally and can be re-run when an architecture changes. Collins collaborates with Vanderbilt and hosts university students as summer interns.

Research thrusts

  1. 01

    Zero-trust design patterns

    New and updated zero-trust patterns for high-density urban airspace, modeled in AADL as building blocks for secure UAS systems.

    UC-08

  2. 02

    LLM-assisted formal security assessment

    A toolchain in which a language model proposes theorems about an architecture and the Lean theorem prover checks them, producing repeatable, machine-checked evidence.

    UC-08with Vanderbilt

  3. 03

    Industry partnership

    Avionics subject-matter expertise through invited technical deep dives, and summer research internships for university students.

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.

Use cases

Where Collins contributes

People

Former members

  • Saqib HasanCo-Investigator

Publications

Publications

1 published or accepted paper

  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

    WorkshopVanderbiltCollinsUC-08