STM32F429 — Ada/SPARK Physical Access Controller

The STM32F429 serves as a physical access controller with formal verification guarantees. Written in Ada with SPARK annotations, it provides mathematical proof that security-critical operations (relay control) are correct.

Role in the Architecture

Technical Specifications

Feature	Detail
MCU	STM32F429 (ARM Cortex-M4F, 180MHz)
RAM	256KB SRAM + 64KB CCM
Flash	2MB
Language	Ada 2022 with SPARK formal verification
Crypto	Hardware PKA (ECDSA P-256), HASH accelerator (SHA-256)
Connectivity	Ethernet (LWIP + MQTT)
Key Storage	OTP (One-Time Programmable) area
Loop interval	5 seconds

Why Ada/SPARK?

Feature	Ada/SPARK	C	Rust
Formal verification	GNATprove (mathematical proof)	Frama-C (complex)	Not available
Runtime safety	No buffer overflows (proven)	Manual	Compile-time (Rust)
Design by Contract	Native (Pre/Post/Type_Invariant)	Library-based	Not native
Real-time	Ravenscar profile (deterministic)	No guarantees	No guarantees
DO-178C / IEC 61508	Certified	Certifiable	Not yet
Industry adoption	Rail, aerospace, defense	Universal	Growing

For a controller that opens/closes physical doors, mathematical proof of correctness isn't a luxury — it's a safety requirement. A bug in relay control could lock people inside a burning building.

SPARK-Proven Relay Control

The relay control module has formal contracts that GNATprove mathematically verifies:

-- relay_control.ads (specification)
package Relay_Control with SPARK_Mode is

   type Relay_State is (Open, Closed);
   type Attestation_Status is (Not_Verified, Verified, Revoked);

   -- PRECONDITION: Relay can only be Closed if attestation is Verified
   procedure Set_Relay (
      State  : in Relay_State;
      Attest : in Attestation_Status
   ) with
      Pre  => (if State = Closed then Attest = Verified),
      Post => (if Attest = Revoked then Current_State = Open);

   function Current_State return Relay_State;

end Relay_Control;

-- relay_control.adb (implementation)
package body Relay_Control with SPARK_Mode is

   Internal_State : Relay_State := Open;

   procedure Set_Relay (
      State  : in Relay_State;
      Attest : in Attestation_Status
   ) is
   begin
      -- Safety override: ALWAYS open relay if attestation revoked
      if Attest = Revoked then
         Internal_State := Open;
         GPIO.Write_Pin (RELAY_PIN, GPIO.Low);
         return;
      end if;

      -- Normal operation
      Internal_State := State;
      case State is
         when Open   => GPIO.Write_Pin (RELAY_PIN, GPIO.Low);
         when Closed => GPIO.Write_Pin (RELAY_PIN, GPIO.High);
      end case;
   end Set_Relay;

   function Current_State return Relay_State is (Internal_State);

end Relay_Control;

What GNATprove Guarantees

Running gnatprove on this code mathematically proves:

It's impossible to close the relay without valid attestation — the precondition prevents it at compile time
Revoked attestation always opens the relay — the postcondition guarantees it
No runtime exceptions — no division by zero, no overflow, no array out-of-bounds
No uninitialized variables — all paths initialize before use

Main Loop

-- main.adb
procedure Main is
   Attest_Status : Relay_Control.Attestation_Status;
   Tamper        : Tamper_Detection.Tamper_Event;
begin
   -- Initialize hardware
   MQTT_Publisher.Connect (Host => "mosquitto", Port => 8883);

   loop
      -- 1. Verify firmware attestation (every loop = every 5s)
      Attest_Status := Vault_Attestation.Verify_Device_Certificate;

      -- 2. Control relay based on attestation
      if Attest_Status = Relay_Control.Verified then
         Relay_Control.Set_Relay (Closed, Attest_Status);
      else
         Relay_Control.Set_Relay (Open, Attest_Status);
      end if;

      -- 3. Publish status
      MQTT_Publisher.Publish (
         Topic   => "aurora/sensors/stm32_pac_01/status",
         Payload => Build_Status_Payload (Attest_Status),
         QoS     => At_Least_Once
      );

      -- 4. Check tamper sensors
      Tamper := Tamper_Detection.Check_Tamper;
      if Tamper /= Tamper_Detection.None then
         MQTT_Publisher.Publish (
            Topic   => "aurora/sensors/stm32_pac_01/alerts",
            Payload => Build_Tamper_Alert (Tamper),
            QoS     => Exactly_Once
         );
      end if;

      -- 5. Publish telemetry
      MQTT_Publisher.Publish (
         Topic   => "aurora/sensors/stm32_pac_01/telemetry",
         Payload => Build_Telemetry_Payload,
         QoS     => At_Least_Once
      );

      -- Wait 5 seconds
      delay 5.0;
   end loop;
end Main;

Vault Attestation

package Vault_Attestation with SPARK_Mode is

   type Attestation_Result is (Success, Failure, Timeout);
   subtype Hash_String is String (1 .. 64);  -- SHA-256 hex
   subtype Device_ID is String (1 .. 20);

   function Verify_Device_Certificate return Relay_Control.Attestation_Status;
   function Get_Firmware_Hash return Hash_String;
   function Get_Boot_Count return Natural;

end Vault_Attestation;

The STM32 uses hardware peripherals for cryptographic operations:

Operation	Hardware	Purpose
ECDSA P-256 Sign/Verify	PKA (Public Key Accelerator)	Attestation signatures
SHA-256	HASH accelerator	Firmware hashing
Key Storage	OTP area	Private key (write-once)
Certificate	Flash partition	Vault-issued x.509

Tamper Detection

package Tamper_Detection is

   type Tamper_Event is (None, Case_Open, Wire_Cut, Voltage_Anomaly, Temperature_Anomaly);
   type Tamper_Severity is (Normal, Warning, Critical);

   function Check_Tamper return Tamper_Event;
   function Get_Severity (Event : Tamper_Event) return Tamper_Severity;

end Tamper_Detection;

Event	Detection Method	Severity
`Case_Open`	Mechanical switch (GPIO interrupt)	Critical
`Wire_Cut`	Continuity loop (GPIO pull-up)	Critical
`Voltage_Anomaly`	ADC monitoring (±10% threshold)	Warning
`Temperature_Anomaly`	Internal temp sensor (>85°C)	Warning

MQTT Publisher

package MQTT_Publisher is

   type QoS_Level is (At_Most_Once, At_Least_Once, Exactly_Once);

   procedure Connect (Host : String; Port : Positive);
   procedure Disconnect;
   procedure Publish (Topic : String; Payload : String; QoS : QoS_Level);

end MQTT_Publisher;

The STM32 connects with mTLS using Vault-issued x.509 certificates:

Client certificate: ECDSA P-256, issued by Vault PKI
CA certificate: Vault root CA
TLS version: 1.3

Build System

# Build with GNAT (Ada compiler)
gprbuild -P firmware/stm32/stm32_aurora.gpr -XBUILD=release

# Run SPARK formal verification
gnatprove -P firmware/stm32/stm32_aurora.gpr --level=2 --prover=z3

# Flash via ST-Link
st-flash write firmware/stm32/bin/main.bin 0x08000000

SPARK Proof Levels

Level	What it proves	Time
0	Flow analysis (no uninitialized reads)	Seconds
1	+ No runtime exceptions (overflow, range)	Minutes
2	+ Contracts satisfied (pre/post conditions)	Minutes
3	+ All assertions proven	Hours
4	+ Full functional correctness	Hours+

AuroraSOC uses level 2 — sufficient to prove the relay safety invariant.

Role in the Architecture​

Technical Specifications​

Why Ada/SPARK?​

SPARK-Proven Relay Control​

What GNATprove Guarantees​

Main Loop​

Vault Attestation​

Tamper Detection​

MQTT Publisher​

Build System​

SPARK Proof Levels​