9月13日，2020 STM32全國研討會（深圳站），華為LiteOS架構師苗欣做了題為“STM32攜手華為LiteOS共筑物聯網未來—— 使物聯網更安全”的演講，向外界分享了華為LiteOS形式化驗證的安全實踐，在物聯網操作系統領域，使用形式化驗證還是首次提出。

操作系統的穩定、安全是運行在之前的物聯網業務的保障，目前保證系統正確性的手段主要有測試、仿真和形式化驗證等。其中測試大家接觸的比較多，是通常采用的方法，也容易操作和上手。而形式化驗證用的相對較少，是指用某種數學形式來描述規約、設計和實現，根據程序語義來分析和驗證程序特性，用數學證明的方式保證系統的安全，能夠很深入的檢測到系統中存在的缺陷或者錯誤。

形式化驗證的驗證方式

軟件測試無法證明系統不存在缺陷，也不能證明它符合一定的屬性。形式化驗證可以證明一個系統不存在某個缺陷或符合某個或某些屬性。

通過以上的介紹和對比，我們了解到了什么是形式化驗證，形式化驗證和軟件測試的區別。

下面通過一個例子，介紹形式化驗證是如何確保系統安全的：

以下圖中access接口為例，在第8行buf[x] = 0操作時，當x >= SIZE或x < 0，會產生數組越界，針對x >= SIZE的場景：

可以得到一個規約：若運行至第8行時， x < SIZE，則不存在該風險；

根據上下文推導出，只有滿足以下2種條件，才能滿足規約：

index < 1024，第6行進入ture分支，x = index + 1，此時仍然能夠保障x < 1024；

index >= 1024，第6行進入false分支；

如果驗證系統中所有調用access接口的路徑都能滿足以上條件，則表示不存在該風險，若存在不滿足條件的路徑，則這些路徑中存在風險；

形式化驗證和軟件測試的區別

目前主要有兩類驗證方式。

一、功能性驗證：驗證的性質復雜，能夠全面驗證軟件是否滿足設計的目的，可取代單元測試。證明過程復雜，需要人工插入驗證條件。

二、基礎性質驗證：驗證條件可自動生成；自動化程度高。但無法驗證軟件復雜性質的可滿足性。

LiteOS的形式化驗證先從基礎性質驗證出發，逐步加入功能驗證。

形式化驗證 用數學證明華為LiteOS內核安全

LiteOS使用定理證明的方法，即定義基本公理和邏輯推理系統，用計算機程序來保證推導過程的正確性，證明力優于其他形式化方法。業界常用工具有HOL/Isabelle, PVS, Coq, ACL2等。我們使用定理證明的方法對LiteOS基礎內核進行形式化驗證，證明的屬性包括“無不受控的數據翻轉溢出/除零錯誤/數據截斷/指針強轉/數組越界”等風險，用數學證明Huawei LiteOS內核安全。

通過使用形式化驗證等手段，用數學證明Huawei LiteOS操作系統內核安全，為物聯網智能硬件安全保駕護航。

華為LiteOS與STM32合作歷程

Huawei LiteOS是華為自研的輕量級物聯網操作系統，自開源社區發布以來，圍繞物聯網市場從技術、生態、解決方案等多維度使能合作伙伴，構建開源的物聯網生態，與STM32一直保持緊密合作關系，LiteOS內核目前已支持STM32（L0、L4、F4、F1、F7等）系列芯片和開發版。

I-CUBE-HUAWEI

I-CUBE-HUAWEI 是華為聯合意法半導體合作推出的支撐意法開發板快速連接華為云物聯網平臺的SDK。

I-CUBE-HUAWEI是一款部署在具備廣域網能力、對功耗/存儲/計算資源有苛刻限制的終端設備上的輕量級互聯互通中間件，支持設備快速接入到物聯網平臺，減少開發周期和接入難度，快速構建IoT解決方案。