What has been tested, and what has not
We would rather show you the limits of our evidence than overstate it. Everything below was done by the Altavane team in software and simulation. No independent party has verified these results yet.
Done so far (software and simulation)
- Formal analysis of the key exchange in the Tamarin prover: 7 of 7 properties checked.
- Model-checking of the failover logic: no violations found across up to approximately 1.4 million states.
- Fuzz testing: approximately 10 million malformed inputs to the message parser and approximately 6 million to live sessions, with no crashes and no wrongly accepted commands.
- A simulation campaign of 38,000 missions in which no hostile command was executed.
- The core code runs on an emulated Cortex-M7 processor (25 of 25 checks) and against ArduPilot's ArduCopter flight code in a software-in-the-loop setup (60 of 60 checks).
Not done yet
- Testing on a physical hardware bench.
- A flight trial on a drone.
- Operation over a real LEO satellite link.
- An independent security assessment.
- Patents and certifications.
The next milestone is a hardware test bench, followed by a flight trial and an independent security assessment.