0
  • 聊天消息
  • 系统消息
  • 评论与回复
登录后你可以
  • 下载海量资料
  • 学习在线课程
  • 观看技术视频
  • 写文章/发帖/加入社区
会员中心
创作中心

完善资料让更多小伙伴认识你,还能领取20积分哦,立即完善>

3天内不再提示

鉴源论坛 · 观模丨形式化验证——以操作系统任务调度算法验证为案例

上海控安 来源:上海控安 蔡雄 作者:上海控安 蔡雄 2022-11-09 11:25 次阅读

作者 |蔡雄上海控安可信软件创新研究院研发工程师

版块 |鉴源论坛 · 观模

形式化方法是基于严格的数学基础,通过采用数学逻辑证明来对计算机软硬件系统进行建模、规约、分析、推理和验证,是用于保证计算机软硬件系统正确性以及安全性的一种重要方法。形式化方法是基于严格定义的数学概念和语言,其描述软件及其性质的语言是无歧义的,构造和验证方法是严格的。加上形式化方法在开发过程具备良好的可重复性,并且相应的模型软件也具有比较强的可分析性和可验证性,可以很好地支持抽象模型建立、系统精化、模型和证明重用,有效地提高和保障系统的可信性。

poYBAGNrGgmAW2TaAAGl1JCJppw308.png

图1验证与分析框架

其中主要将验证与分析框架划分为三个部分:

(1)利用VCC做单元级别的函数验证,基于软件架构设计规范及软件详细设计规范等文档,选取适用的审查、分析或测试等方法,验证软件单元设计和实施的正确性和一致性;

(2)利用CBMC做多个函数的集成验证,集成验证主要是针对软件高层设计进行验证,一般来说是对模块和子系统为单位进行验证,验证每个函数调用其他函数时,调用者的规范能否满足;

(3)利用PAT做系统验证,确认整个系统是否满足了软件规格说明中的功能性和非功能性的各项需求,以及满足的程度,系统验证应能够发现和找出因需求不正确、不完整或实现与需求之间的不一致而引起的失效,并识别在没有文档化时或被遗失的那些需求,验证系统在运行时能否满足要求的性质。

01

VCC

VCC(Verified C Compiler)是一个针对C语言程序的验证工具。VCC提供了用于描述C语言函数的前置条件、后置条件、不变式等函数规约的接口。VCC是在原始C语言的基础上进行撰写函数约束对C代码进行进一步的完善C语言更深层次的属性。其对约束内容可以划分为对一阶逻辑表达式的约束和指针的约束。

为了验证程序的正确性,VCC使用演绎验证模式。它生成一定数量的数学表达式(称为验证条件),并试图使用一个自动定理验证器来验证这些数学表达式。如果验证失败,VCC会将失败的原因反映到用户的程序代码身上。因此,用户通常是在代码和程序状态层面与VCC交互的。通常情况下,用户可以忽略在VCC内部的数学推理。例如,如果待验证的程序使用了除法,如果VCC无法证明除数一定非零,它会报告待验证的程序有(潜在的)错误。这并不意味着程序必然是不正确的。通常,可以通过增加注释和断言来解决这个“错误”。不过这可能又会导致其他的错误报告,迫使用户添加更多的注释。所以实际的验证是一个迭代的过程。

如图2所示,VCC的主要工作过程分为两个步骤。

第一步,VCC工具将注释的C代码转换为用于验证的 BoogiePL中间语言,然后通过Boogie工具将其继续转化为一阶逻辑表达式。其中,BoogiePL 是一种带有嵌入式断言的简单命令式语言,它很容易生成一组一阶逻辑公式,表明程序应该满足性质,这里以断言的形式呈现。

第二步,利用 SMT 求解器 Z3(自动化定理证明器)对转换后的一阶逻辑表达式进行验证。Z3 求解器会返回两种结果:(1)一阶逻辑表达式通过验证;(2)Z3 返回一个反例或者提示超时。

poYBAGNrGoOAVOCoAABs3SMPcm0899.png

图2VCC的工作流程

VCC可以自动验证函数是否满足用户书写函数规约。用户使用时操作步骤如下:

(1)根据设计规约,利用VCC提供的接口,编写前置条件、后置条件等函数契约;

(2)使用VCC自动验证函数是否满足这些契约;

(3)如果VCC报告验证失败,那么根据错误报告,修改代码,或重写函数契约;

(4)如果VCC报告验证成功,则说明函数符合契约。

以下一个返回两者之间更小的数的一个函数为例,进一步分析如何使用VCC工具对一个C语言代码进行单元验证。

poYBAGNrGv2AXvcgAABPw0BCGOU451.png

表 1

在表1中,表左边展示的是使用VCC标记过的源代码,表右边展示的是C语言转化后的BoogiePL中间语言,其中为源代码添加了一个前置条件和后置条件。前置条件表示在进入函数前假定满足的条件,后置条件表示在执行完函数后所需要满足的条件。BoogiePL中间语言转化过程会将返回结果赋值给result;将前置条件转化成assume语句来假定前置条件满足;将后置条件转化成assert语句对提出的后置条件进行验证。

02

CBMC

CBMC是Bounded Model Checker for ANSI-C and C++ programs的缩写,CBMC是C和C ++程序的绑定模型检查器。CBMC实现了一种称为边界模型检查(BMC,Bounded Model Checker)的技术。在BMC中,通过联合解开复杂状态机的转换关系及其规范以获得布尔公式,然后使用有效的SAT程序检查布尔公式的可满足性。如果该公式是可满足的,则从SAT过程的输出中提取一个反例。如果公式无法满足要求,则可以展开更多程序以确定是否存在更长的反例。

在许多工程领域中,实时保证是严格的要求。例如是嵌入在汽车控制器中的软件,这些类型的程序中的循环构造通常对迭代次数有严格的限制。CBMC能够通过展开断言来严格验证这种范围。建立迭代次数的界限后,CBMC便可以证明是否存在错误。

CBMC能够验证内存安全性(包括数组范围检查和指针是否安全使用的检查)、检查异常、检查未定义行为的各种变体以及用户指定的断言。通过展开程序中的循环并将结果方程式传递到决策程序来执行验证。CBMC像编译器一样,从命令行接收.c命名的文件,然后编译程序并将不同文件定义的函数组合起来。但CBMC不像编译器生成可执行二进制代码,而是符号执行程序。

CBMC 的目标是分析 C/C++ 或者 JAVA 程序。CBMC 分析的过程是将输入程序,生成对应的控制流图,当获取到程序的CFG时,就可以获取每条路径对应的公式 ,也就是说路径能够执行的条件是使路径对应的公式能够成立。然后针对获得的公式,使用SAT求解命题逻辑,其中分析流程如图3所示。

poYBAGNrG3mACPXnAABN58AW6VM583.png

图3CBMC的验证流程

使用CBMC工具进行分析的过程可以划分成如下四步:

(1)对源代码进行插桩,放入部分约束或者标签

(2)将程序解析为语法树,并基于语法树转换成CFG;

(3)在获得程序的CFG后,我们计划通过收集程序路径,得到路径对应的公式;

(4)结合程序插桩信息,进而通过SMT求解器得到验证结果。

表2所示的是一个CBMC的示例,往代码中注入了一个error标签,可按照其CFG到断言并建立与路径对应的一阶路径进行验证。

pYYBAGNrG5eAUQgbAACrQXpNPaY436.png

表 2

对于上表所示的代码片段,构建的CFG,如图4所示。

pYYBAGNrG76ABHMTAACJyBtWdrk472.png

图4 CFG图示

poYBAGNrG9GAOs6bAACSENWZ9r8049.png

图5 路径图示

对于图5所示的标红路径,可以得到公式0 ≤ t ≤ 79 ∧ t/20 != 0 ∧ t/20 == 1 ∧ TEMP2 = B ⊕ C ⊕ D ∧ TEMP3 = K 2,将这组公式放入SMT求解器进行求解时,可以得到一组解。当我们针对error标签进行可达性验证时、可以得到公式 0 ≤ t ≤ 79 ∧ t/20 != 0 ∧ t/20 != 1∧ t/20 != 2 ∧ t/20 != 3,使用SMT求解器进行求解时发现该公式不能得到满足,即该路径不可达。

03

PAT

PAT是Process Analysis Toolkit的简称,是由新加坡国立大学开发的一款形式化建模与验证工具集,支持进程代数、实时进程代数、时间自动机等多种建模语言。此外,PAT工具的人机交互界面友好,支持多种验证方法,包括精化验证、死锁验证、可达性验证、LTL性质验证等。以PAT工具中最常使用的是语言CSP#为例,对如何使用PAT建模进行讲解。

PAT的进程代数(Communication Sequential Process, 简称CSP)模块。该模块使用CSP#,作为建模语言,描述待验证的系统。

CSP#在经典的CSP的基础上,增加了数据状态与相关的操作,使得建模更加方便、直观。CSP#描述的系统主要包括下面三个部分:

(1)全局量:定义常量和全局变量,支持多维数组;

(2)进程:定义系统中的各个进程;

(3)断言:描述系统应当满足的性质,可以使用全局定义中的变量。

进程的定义如下:

poYBAGNrHCWAET_1AABCl_Ea6V0170.png

图 6

其中事件前缀可以和数据操作组合使用,例如:

P= add{x=x+1;}→Skip;

其中P是一个进程,add代表一个事件,x是全局变量,伴随着事件add的发生, 执行赋值操作x=x+1。在PAT的建模过程中,我们广泛使用这种机制表示数据的传输。

此处解释关于外部选择以及内部选择:

(1)对于一个外部选择:

P[]Q

选择运算符[]指出可以执行P或Q。但该选择由环境解决,如果P中事件首先发生,那么由P接管进程,否则是由Q接管进程。

(2)对于一个内部选择:

P<>Q

其中P或Q可以执行。该选择是内部确定的,意味着随机执行进程P或者 Q。在建模阶段,它对于隐藏不相关的信息很有用。它可以用于对黑盒过程的行为进行建模,而不用了解黑盒的具体实现。

对于内部选择和外部选择可以写出它们的广义形式:

[]x:{1..n}@ P(x) 等价于 P(1)[]...[]P(n)

<>x:{1..n}@ P(x) 等价于 P(1)<>...<>P(n)

pYYBAGNrHFGADsw-AAQFRkSoeng158.png

图 7

在PAT工具中,创建CSP#模型之后,然后就可以进行验证。待验证的性质可以划分为两类,一类是LTL性质,另一类是refine性质。PAT工具将验证性质是否满足。如果不满足,可以查看反例。图7展示的是一个操作系统任务调度算法建模的模型。模型中详细描述了操作系统任务调度过程中创建进程、进程执行、进程抢占、进程挂起、进程中断、进程调度等过程,以及进程各个状态之间的迁移关系。并且在使用PAT工具进行验证的时候,也可以验证出该模型存在死锁,并针对死锁情况给出了一系列行为对应的反例,在此操作系统的任务调度算法中没有发现死锁,因此也不会给出反例。

04

基于形式化验证与分析框架的应用

此套形式化验证与分析框架曾用于某操作系统的调度算法验证。在使用VCC工具进行验证的合计77个函数、其中64个验证通过,13个验证不通过。在13个验证不通过的函数中有6个类型不匹配问题、6个数组溢出问题以及一个指针内容可能为空问题。在使用CBMC工具进行验证的77个函数中,其中21个未添加约束验证通过,7个提示内存不足无法验证,2个验证崩溃。在添加了约束后77个函数中75个验证成功、2个验证崩溃。在使用PAT工具对其建模后,对操作系统内的调度算法进行了无死锁验证,在模拟6935684了状态后得到了该操作系统无死锁的结论。

参考资料

[1] Ankit S , Arnab B , Lakshmanan K , et al. An overview of model checkers and CBMC as a tool. , 2017.

[2] Liu, Y., Sun, J., Dong, J. S.: Developing model checkers using PAT. In: International symposium on automated technology for verification and Analysis, pp. 371–377. Springer, Berlin, Heidelberg (2010).

[3]Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies. 2009. VCC: A Practical System for Verifying Concurrent C. In TPHOLs (LNCS, Vol. 5674). Springer, 23–42.

[4]缪淮扣,陈怡海.《软件形式规格说明语言—Z》,清华大学出版社出版,2012年11月.

[5]Wing J M. A specifier's introduction to formal methods[J]. Computer, 1990, 23(9): 8-22.

[6]Miao, W. and S. Liu, A Formal Engineering Framework for Service-Based Software Modeling. IEEE Transactions on Services Computing, 2013. 6(4): p. 536-550.

审核编辑 黄昊宇

声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
  • 操作系统
    +关注

    关注

    37

    文章

    6808

    浏览量

    123287
  • C语言
    +关注

    关注

    180

    文章

    7604

    浏览量

    136707
  • Vcc
    Vcc
    +关注

    关注

    2

    文章

    305

    浏览量

    35963
  • 任务调度算法

    关注

    0

    文章

    3

    浏览量

    5728
收藏 人收藏

    评论

    相关推荐

    使用CSL来补充操作系统调度程序处理级联中断

    电子发烧友网站提供《使用CSL来补充操作系统调度程序处理级联中断.pdf》资料免费下载
    发表于 10-16 10:12 0次下载
    使用CSL来补充<b class='flag-5'>操作系统</b><b class='flag-5'>调度</b>程序处理级联中断

    面向功能安全应用的汽车开源操作系统解决方案

    在SAE 2024国际汽车安全大会上,Elektrobit的Linux专家王红燕在操作系统与芯片技术的分论坛大家带来了“面向功能安全应用的汽车开源操作系统解决方案”主题演讲。
    的头像 发表于 09-27 09:21 461次阅读
    面向功能安全应用的汽车开源<b class='flag-5'>操作系统</b>解决方案

    教学验证BUCK电路仿真验证

    方案匹配您的科研/教学模式。今天大家分享的是基于EasyGo实时仿真平台的PPEC-HIL BUCK仿真实验,并将其与BUCK电路的实际实验进行对比测试,验证EasyGo实时仿真平台仿真
    发表于 09-05 10:47

    开启全新AI时代 智能嵌入式系统快速发展——“第六届国产嵌入式操作系统技术与产业发展论坛”圆满结束

    嵌入式系统是电子信息产业的基础,是智能系统的核心。大模型催生AI走入千家万户、唤醒端侧AI的需求爆发。机器人、无人驾驶和智能制造代表的智能嵌入式
    发表于 08-30 17:24

    简单认识RTOS实时操作系统

    RTOS(Real Time Operating System,实时操作系统)是一种专门设计用于在严格时间限制内处理任务操作系统。它以其高实时性、多任务处理能力和资源管理能力在工业自
    的头像 发表于 08-20 11:20 2697次阅读

    教学验证PPEC+HIL 单相逆变仿真验证

    实验,配备完备的课程实验指导书,提供多种方案匹配您的科研/教学模式。今天大家分享的是“基于EasyGo实时仿真平台的PPEC-HIL单相逆变仿真实验与真实单相逆变电路实验的对比测试”,验证EasyGo
    发表于 08-09 10:25

    第六届国产嵌入式操作系统技术与产业发展论坛议程发布

    每年一度的国产嵌入式操作系统论坛即将在杭州滨江举办,今年是第六届了,又是中国嵌入式系统新朋老友相聚的时刻。大模型催生AI走人千家万户、唤醒端侧AI的需求爆发。机器人、无人驾驶和智能制造
    发表于 07-26 10:54

    3568F-翼辉SylixOS国产操作系统演示案例

    、VxWorks操作系统的应用程序可方便快捷地移植到SylxOS 系统上运行。 SylixOS作为抢占式多任务硬实时操作系统,具有如下功能特点: (1)兼容IEEE1003(ISO/E
    发表于 07-25 15:52

    教学验证PPEC+HIL DAB仿真验证

    ,接下来大家分享本次实验详情。一、设备信息实际设备:PPEC控制单元、DAB功率电路板仿真设备:EasyGo实时仿真器NetBox其他设备:万用表、直流电压、上位机等二、验证说明 真实系统
    发表于 07-18 14:38

    教学验证PPEC+HIL LLC拓扑仿真验证

    ,提供多种方案匹配您的科研/教学模式。今天大家分享的是基于PPEC控制单元和EasyGo实时仿真平台,对LLC谐振电路进行的真实系统测试及仿真测试。 便于进行比较测试实验,控制部分统一采用携带PPEC
    发表于 06-11 13:45

    K折交叉验证算法与训练集

    K折交叉验证算法与训练集
    的头像 发表于 05-15 09:26 547次阅读

    论坛轨交软件测试技术详述

    作者 |刘艳青 上海控安安全测评部测试经理 版块 |论坛 · 通 社群 |添加微信号“TICPShanghai”加入“上海控安51fusa安全社区” 01 集成测试技术要求 1.
    的头像 发表于 05-14 16:38 335次阅读
    <b class='flag-5'>鉴</b><b class='flag-5'>源</b><b class='flag-5'>论坛</b><b class='flag-5'>丨</b>轨交软件测试技术详述

    带你认识实时操作系统(rtos)

    实时操作系统(RTOS)是嵌入式系统和实时应用提供一个稳定、可预测和高效运行环境的操作系统。实时操作系统确保了
    的头像 发表于 04-16 16:30 1251次阅读
    带你认识实时<b class='flag-5'>操作系统</b>(rtos)

    鸿蒙OS 分布式任务调度

    鸿蒙OS 分布式任务调度概述 在 HarmonyO S中,分布式任务调度平台对搭载 HarmonyOS 的多设备构筑的“超级虚拟终端”提供统一的组件管理能力,
    的头像 发表于 01-29 16:50 489次阅读

    详解实时操作系统和非实时操作系统

    实时操作系统,当外界事件和数据产生时,系统能以足够快的速度予以处理,其处理结果能在规定的时间内控制生产结果或对系统做出响应,并控制所有实时任务协调一致运行的
    的头像 发表于 12-26 09:54 4746次阅读
    详解实时<b class='flag-5'>操作系统</b>和非实时<b class='flag-5'>操作系统</b>