STM32H743 — Ada/SPARK Physical Access Controller

The STM32H743 serves as a physical access controller with formal verification guarantees. Written in Ada 2022 with SPARK annotations and a dedicated Aurora HAL layer, it provides mathematical proof that security-critical operations (relay control) are correct while accessing real STM32H7 peripherals (HASH accelerator, GPIO, ADC, RNG).

Role in the Architecture

Technical Specifications

Feature	Detail
MCU	STM32H743 (ARM Cortex-M7, 480 MHz, dual-issue)
RAM	512 KB AXI-SRAM + 128 KB DTCM + 128 KB SRAM1–4
Flash	2 MB (memory-mapped at 0x0800_0000)
Language	Ada 2022 with SPARK 2014 formal verification
Runtime	`light-tasking-stm32h7` (GNAT, enables `delay`)
Crypto	HASH accelerator (SHA-256 hardware), ECDSA P-256 (mbedTLS software)
Connectivity	Ethernet (LWIP TCP + mbedTLS TLS + MQTT 3.1.1)
Key Storage	OTP area (0x1FF0_F000, write-once)
HAL	Aurora_HAL (SPARK_Mode Off) — GPIO, ADC, HASH, RNG, TCP, TLS
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 — SPARK-proven relay specification
package Relay_Control with SPARK_Mode is
   type Relay_State is (Open, Closed);
   type Attestation_Status is (Not_Verified, Verified, Revoked);

   Current_State       : Relay_State        := Open;
   Current_Attestation : Attestation_Status := Not_Verified;

   procedure Set_Relay
     (State  : in Relay_State;
      Status : in Attestation_Status)
   with
     Global => (Output => (Current_State, Current_Attestation)),
     Pre    => (if State = Closed then Status = Verified),
     Post   => (if Status = Revoked then Current_State = Open);

   function Get_State return Relay_State
   with Global => (Input => Current_State);

   function Get_Attestation return Attestation_Status
   with Global => (Input => Current_Attestation);
end Relay_Control;

-- relay_control.adb — SPARK body with non-SPARK GPIO wrapper
with Aurora_HAL;
package body Relay_Control with SPARK_Mode is
   --  Local non-SPARK procedure writes hardware GPIO register
   procedure Write_Relay_GPIO with SPARK_Mode => Off is
   begin
      case Current_State is
         when Open   => Aurora_HAL.GPIO_Write
              (Aurora_HAL.Relay_Port, Aurora_HAL.Relay_Pin, Aurora_HAL.Low);
         when Closed => Aurora_HAL.GPIO_Write
              (Aurora_HAL.Relay_Port, Aurora_HAL.Relay_Pin, Aurora_HAL.High);
      end case;
   end Write_Relay_GPIO;

   procedure Set_Relay
     (State : in Relay_State; Status : in Attestation_Status)
   is
   begin
      if Status = Revoked then
         Current_State := Open;
      else
         Current_State := State;
      end if;
      Current_Attestation := Status;
      Write_Relay_GPIO;   --  non-SPARK GPIO register access
   end Set_Relay;

   function Get_State return Relay_State is (Current_State);
   function Get_Attestation return Attestation_Status is (Current_Attestation);
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
with Aurora_HAL;
procedure Main with SPARK_Mode is
   Attestation : Relay_Control.Attestation_Status;
   Tamper      : Tamper_Detection.Tamper_Event;
begin
   --  Initialize hardware: RCC clocks, GPIO, ADC, HASH, RNG
   Aurora_HAL.System_Init;
   Aurora_HAL.ADC_Init;
   Aurora_HAL.GPIO_Configure (Aurora_HAL.Relay_Port, Aurora_HAL.Relay_Pin,
                               Aurora_HAL.Output, Aurora_HAL.No_Pull);
   Aurora_HAL.GPIO_Configure (Aurora_HAL.Case_Open_Port, Aurora_HAL.Case_Open_Pin,
                               Aurora_HAL.Input, Aurora_HAL.Pull_Up);
   Aurora_HAL.GPIO_Configure (Aurora_HAL.Wire_Cut_Port, Aurora_HAL.Wire_Cut_Pin,
                               Aurora_HAL.Input, Aurora_HAL.Pull_Up);
   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,
       Abstract_State => Attestation_State
is
   subtype Hash_String is String (1 .. 64);  --  SHA-256 hex (64 chars)

   procedure Verify_Device_Certificate
     (Result : out Relay_Control.Attestation_Status)
   with Global => (In_Out => Attestation_State);

   function Get_Firmware_Hash return Hash_String
   with Global => null;   --  pure flash read via non-SPARK HAL

   function Get_Boot_Count return Natural
   with Global => (Input => Attestation_State);
end Vault_Attestation;

The STM32 uses hardware peripherals for cryptographic operations:

Operation	Hardware	Purpose
ECDSA P-256 Sign	mbedTLS software (STM32H7 lacks PKA)	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 on PA0 (pull-up, active low)	Warning
`Wire_Cut`	Continuity loop on PA1 (pull-up, active low)	Critical
`Voltage_Anomaly`	ADC1 ch4 on PA4 (2.8–3.3 V window, 12-bit)	Warning
`Temperature_Anomaly`	Internal temp sensor via ADC3 ch18 (−20 to +70 °C)	Critical

MQTT Publisher

package MQTT_Publisher
  with SPARK_Mode,
       Abstract_State => Connection_State
is
   type QoS_Level is (At_Most_Once, At_Least_Once, Exactly_Once);

   procedure Connect (Host : in String; Port : in Natural)
   with Global => (Output => Connection_State);

   procedure Publish
     (Topic   : in String;
      Payload : in String;
      QoS     : in QoS_Level := At_Least_Once)
   with Global => (In_Out => Connection_State);

   procedure Disconnect
   with Global => (In_Out => Connection_State);

   function Is_Connected return Boolean
   with Global => (Input => Connection_State);
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/aurora_stm32.gpr -XBUILD=release

# Run SPARK formal verification
gnatprove -P firmware/stm32/aurora_stm32.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​