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

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

形式化驗證的驗證方式

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

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

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

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

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

根據(jù)上下文推導出，只有滿足以下2種條件，才能滿足規(guī)約：

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

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

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

形式化驗證和軟件測試的區(qū)別

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

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

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

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

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

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

通過使用形式化驗證等手段，用數(shù)學證明Huawei LiteOS操作系統(tǒng)內核安全，為物聯(lián)網(wǎng)智能硬件安全保駕護航。

華為LiteOS與STM32合作歷程

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

I-CUBE-HUAWEI

I-CUBE-HUAWEI 是華為聯(lián)合意法半導體合作推出的支撐意法開發(fā)板快速連接華為云物聯(lián)網(wǎng)平臺的SDK。

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