STM32与华为LiteOS如何共同打造物联网的未来

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解决方案。