STM32H743 - وحدة التحكم في الوصول الفعلي Ada/SPARK

يعمل STM32H743 بمثابة وحدة تحكم في الوصول الفعلي مع ضمانات التحقق الرسمية. تمت كتابته في Ada 2022 مع تعليقات SPARK التوضيحية وطبقة Aurora HAL المخصصة، وهو يوفر دليلًا رياضيًا على صحة العمليات الأمنية الحرجة (التحكم في الترحيل) أثناء الوصول إلى الأجهزة الطرفية الحقيقية STM32H7 (مسرع HASH، GPIO، ADC، RNG).

دور في الهندسة المعمارية

المواصفات الفنية

ميزة	التفاصيل
MCU	STM32H743 (ARM Cortex-M7، 480 ميجاهرتز، الإصدار المزدوج)
كبش	512 كيلو بايت AXI-SRAM + 128 كيلو بايت DTCM + 128 كيلو بايت SRAM1–4
فلاش	2 ميجا بايت (الذاكرة المعينة عند 0x0800_0000)
لغة	Ada 2022 مع التحقق الرسمي من SPARK 2014
وقت التشغيل	`light-tasking-stm32h7` (GNAT، يمكّن `delay`)
التشفير	مسرع التجزئة (جهاز SHA-256)، ECDSA P-256 (برنامج mbedTLS)
الاتصال	إيثرنت (LWIP TCP + mbedTLS TLS + MQTT 3.1.1)
تخزين المفاتيح	منطقة OTP (0x1FF0_F000، الكتابة مرة واحدة)
هال	Aurora_HAL (SPARK_Mode Off) — GPIO، وADC، وHASH، وRNG، وTCP، وTLS
فاصل زمني للحلقة	5 ثواني

لماذا آدا/سبارك؟

ميزة	أدا/سبارك	ج	Rust
التحقق الرسمي	GNATprove (الدليل الرياضي)	فراما-سي (معقد)	غير متوفر
سلامة وقت التشغيل	لا يوجد تجاوزات في المخزن المؤقت (ثبت)	يدوي	وقت الترجمة (Rust)
التصميم بموجب العقد	أصلي (قبل/بعد/النوع_غير المتغير)	القائمة على المكتبة	ليس مواطنا
في الوقت الحالى	الملف الشخصي Ravenscar (حتمية)	لا ضمانات	لا ضمانات
DO-178C / IEC 61508	معتمد	يمكن التصديق عليها	ليس بعد
اعتماد الصناعة	السكك الحديدية والفضاء والدفاع	عالمي	تزايد

بالنسبة لوحدة التحكم التي تفتح/تغلق الأبواب المادية، فإن الدليل الرياضي على الصحة ليس رفاهية - بل هو أحد متطلبات السلامة. قد يؤدي وجود خلل في التحكم في التتابع إلى حبس الأشخاص داخل مبنى محترق.

التحكم في التتابع المعتمد من SPARK

تحتوي وحدة التحكم في الترحيل على عقود رسمية يتحقق منها GNAT رياضيًا:

-- 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;

ما ضمانات GNATprove

تشغيل gnatprove على هذا الكود يثبت رياضيًا:

من المستحيل إغلاق التتابع بدون شهادة صالحة — الشرط المسبق يمنع ذلك في وقت الترجمة
تفتح الشهادة الملغاة دائمًا التتابع — الشرط اللاحق يضمن ذلك
لا توجد استثناءات لوقت التشغيل — لا يوجد قسمة على صفر، ولا يوجد تجاوز، ولا توجد مصفوفة خارج الحدود
لا توجد متغيرات غير مهيأة — تتم تهيئة كافة المسارات قبل الاستخدام

الحلقة الرئيسية

-- 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

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;

يستخدم STM32 الأجهزة الطرفية لعمليات التشفير:

عملية	الأجهزة	غاية
علامة ECDSA P-256	برنامج mbedTLS (STM32H7 يفتقر إلى PKA)	توقيعات الشهادة
شا-256	مسرع التجزئة	تجزئة البرامج الثابتة
تخزين المفاتيح	منطقة مكتب المدعي العام	المفتاح الخاص (الكتابة مرة واحدة)
شهادة	قسم الفلاش	Vault-إصدار x.509

كشف العبث

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;

حدث	طريقة الكشف	خطورة
`Case_Open`	مفتاح ميكانيكي على PA0 (سحب لأعلى، منخفض نشط)	تحذير
`Wire_Cut`	حلقة الاستمرارية على PA1 (سحب لأعلى، انخفاض نشط)	شديد الأهمية
`Voltage_Anomaly`	ADC1 ch4 على PA4 (نافذة 2.8–3.3 فولت، 12 بت)	تحذير
`Temperature_Anomaly`	مستشعر درجة الحرارة الداخلي عبر ADC3 ch18 (-20 إلى +70 درجة مئوية)	شديد الأهمية

الناشر MQTT

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;

يتصل STM32 بـ mTLS باستخدام شهادات x.509 الصادرة عن Vault:

شهادة العميل: ECDSA P-256، الصادرة عن Vault PKI
شهادة CA: Vault root CA
إصدار TLS: 1.3

بناء النظام

# 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

مستويات مقاومة الشرارة

مستوى	ما يثبت	وقت
0	تحليل التدفق (لا توجد قراءات غير مهيأة)	ثواني
1	+ لا توجد استثناءات في وقت التشغيل (التجاوز، النطاق)	دقائق
2	* استيفاء العقود (الشروط المسبقة/اللاحقة)	دقائق
3	+ ثبت جميع التأكيدات	ساعات
4	+ صحة وظيفية كاملة	ساعات+

يستخدم AuroraSOC المستوى 2 - وهو ما يكفي لإثبات ثبات سلامة التتابع.

دور في الهندسة المعمارية​

المواصفات الفنية​

لماذا آدا/سبارك؟​

التحكم في التتابع المعتمد من SPARK​

ما ضمانات GNATprove​

الحلقة الرئيسية​

شهادة Vault​

كشف العبث​

الناشر MQTT​

بناء النظام​

مستويات مقاومة الشرارة​