STM32與華為L(zhǎng)iteOS如何共同打造物聯(lián)網(wǎng)的未來(lái)

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

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

形式化驗(yàn)證的驗(yàn)證方式

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

通過(guò)以上的介紹和對(duì)比，我們了解到了什么是形式化驗(yàn)證，形式化驗(yàn)證和軟件測(cè)試的區(qū)別。

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

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

可以得到一個(gè)規(guī)約：若運(yùn)行至第8行時(shí)， x < SIZE，則不存在該風(fēng)險(xiǎn)；

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

index < 1024，第6行進(jìn)入ture分支，x = index + 1，此時(shí)仍然能夠保障x(chóng) < 1024；

index >= 1024，第6行進(jìn)入false分支；

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

形式化驗(yàn)證和軟件測(cè)試的區(qū)別

目前主要有兩類(lèi)驗(yàn)證方式。

一、功能性驗(yàn)證：驗(yàn)證的性質(zhì)復(fù)雜，能夠全面驗(yàn)證軟件是否滿足設(shè)計(jì)的目的，可取代單元測(cè)試。證明過(guò)程復(fù)雜，需要人工插入驗(yàn)證條件。

二、基礎(chǔ)性質(zhì)驗(yàn)證：驗(yàn)證條件可自動(dòng)生成；自動(dòng)化程度高。但無(wú)法驗(yàn)證軟件復(fù)雜性質(zhì)的可滿足性。

LiteOS的形式化驗(yàn)證先從基礎(chǔ)性質(zhì)驗(yàn)證出發(fā)，逐步加入功能驗(yàn)證。

形式化驗(yàn)證 用數(shù)學(xué)證明華為L(zhǎng)iteOS內(nèi)核安全

LiteOS使用定理證明的方法，即定義基本公理和邏輯推理系統(tǒng)，用計(jì)算機(jī)程序來(lái)保證推導(dǎo)過(guò)程的正確性，證明力優(yōu)于其他形式化方法。業(yè)界常用工具有HOL/Isabelle, PVS, Coq, ACL2等。我們使用定理證明的方法對(duì)LiteOS基礎(chǔ)內(nèi)核進(jìn)行形式化驗(yàn)證，證明的屬性包括“無(wú)不受控的數(shù)據(jù)翻轉(zhuǎn)溢出/除零錯(cuò)誤/數(shù)據(jù)截?cái)?指針強(qiáng)轉(zhuǎn)/數(shù)組越界”等風(fēng)險(xiǎn)，用數(shù)學(xué)證明Huawei LiteOS內(nèi)核安全。

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

華為L(zhǎng)iteOS與STM32合作歷程

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

I-CUBE-HUAWEI

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

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