FreeRTOS 内存安全证明基于 CBMC 对 TaskPrioritySet 的形式化验证深度解析【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS本指南以 FreeRTOS 仓库中 CBMC 证明目录下的TaskPrioritySet证明文档FreeRTOS/Test/CBMC/proofs/Task/TaskPrioritySet/README.md为核心系统讲解如何用 C Bounded Model CheckerCBMC形式化验证 FreeRTOS 任务优先级设置函数vTaskPrioritySet的内存安全性。文章覆盖证明原理、harness 测试代码、任务列表初始化、证明假设、构建配置与运行方法帮助读者掌握 FreeRTOS 官方 CBMC 证明基础设施的用法并理解嵌入式 RTOS 内核函数静态形式化验证的完整工程实践。一、为什么需要为 TaskPrioritySet 编写 CBMC 证明FreeRTOS 的vTaskPrioritySet用于在运行时修改任务优先级其实现涉及多个全局链表就绪列表pxReadyTasksLists等的插入、移除与排序操作。这类函数直接操作指针与链表一旦出现越界、空指针解引用、未初始化内存访问或整数溢出将导致内核内存破坏且难以通过常规运行时测试完整覆盖。CBMCC Bounded Model Checker是开源的静态分析工具它把 C 程序翻译成布尔逻辑表达式通过符号执行与 SAT/SMT 求解在给定界内穷举所有可能执行路径从而可以证明目标函数不会发生诸如数组越界、空指针解引用、非法内存访问等内存安全问题。FreeRTOS 官方在 FreeRTOS/Test/CBMC/README.md 中说明仓库的持续集成系统会对每一个 pull request 运行这些证明开发者也可以在本机复现。本证明的目标入口是vTaskPrioritySet由 TaskPrioritySet_harness.c 中的harness()调用证明它在此前初始化的任务列表与随机构造的任务控制块TCB上执行时内存安全。二、证明的整体思路与关键设计2.1 核心挑战任务句柄可能为 NULL原文档明确指出证明的初始化与任务句柄的取值紧密相关任务句柄TaskHandle_t可能为 NULL此时vTaskPrioritySet内部会退而使用全局变量pxCurrentTCB作为操作对象。这一分支是内存安全分析的关键路径因此在 harness 中必须同时构造句柄非空与句柄为空两类场景。2.2 证明假设三个被信任的函数原文档列出以下三个函数被假定为内存安全且对目标函数的内存安全不产生相关副作用vPortEnterCriticalvPortExitCriticalvPortGenerateSimulatedInterrupt这符合 CBMC 证明的常规工程折中临界区进入/退出与中断模拟属于平台相关代码如果对其逐条建模会大幅增加求解负担而它们既不影响vTaskPrioritySet的链表操作逻辑也不触及被证明函数管理的内存区域。同时在 cbmc-viewer.json 的expected-missing-functions列表中这三个函数与pxPortInitialiseStack、xPortStartScheduler、vTaskSuspendAll、xTaskPriorityInherit、xTaskPriorityDisinherit等二十余个函数一起被登记为预期缺失函数即由 Stub 或未解析符号替代视为内存安全。2.3 当前状态Work-in-Progress原文档明确说明该证明是进行中work-in-progress的工作详细假设记录在 harness 代码中。这意味着该证明的目标是随着内核代码演进持续维护读者在阅读时应以 harness 中的实际注释与断言为准。三、Harness 代码逐段剖析3.1 顶层入口harness()证明入口位于 TaskPrioritySet_harness.c 的harness()函数void harness() { TaskHandle_t xTask; UBaseType_t uxNewPriority; BaseType_t xTasksPrepared; __CPROVER_assume( uxNewPriority configMAX_PRIORITIES ); xTasksPrepared xPrepareTaskLists( xTask ); /* Check that this second invocation of xPrepareTaskLists is needed. */ if( xPrepareTaskLists( xTask ) ! pdFAIL ) { vTaskPrioritySet( xTask, uxNewPriority ); } }关键设计点如下优先级合法化假设__CPROVER_assume( uxNewPriority configMAX_PRIORITIES )将新优先级约束为合法值。其作用有二一是避免触发configASSERT对应 harness 注释 avoids failed assert二是把符号执行空间限定在 API 契约允许的范围内——vTaskPrioritySet作为公开 API其前置条件本就是优先级小于configMAX_PRIORITIES。在 patches/FreeRTOSConfig.h 中该值被配置为7。两次调用xPrepareTaskLists的用意注释 Check that this second invocation of xPrepareTaskLists is needed 表明第二次调用用于扩展状态空间。xPrepareTaskLists内部大量使用nondet_bool()做非确定性分支两次调用会产生不同的链表填充组合从而覆盖vTaskPrioritySet中更多执行路径例如目标任务是否已挂在就绪列表、pxCurrentTCB是否也在就绪列表中等组合。对pdFAIL的防御若任务列表准备失败例如pxCurrentTCB分配失败返回pdFAIL则跳过vTaskPrioritySet避免在未初始化状态下执行被证明函数。3.2 任务列表准备函数xPrepareTaskLists()该函数定义在同目录的 tasks_test_access_functions.h 中其核心职责是初始化 FreeRTOS 任务列表全局变量并用非确定性填充少量就绪列表项。流程如下BaseType_t xPrepareTaskLists( TaskHandle_t * xTask ) { TCB_t * pxTCB NULL; __CPROVER_assert_zero_allocation(); prvInitialiseTaskLists(); pxTCB xUnconstrainedTCB(); /* 非确定性插入另一个任务 */ if( nondet_bool() ) { TCB_t * pxOtherTCB xUnconstrainedTCB(); if( pxOtherTCB ! NULL ) { vListInsert( pxReadyTasksLists[ pxOtherTCB-uxPriority ], ( pxOtherTCB-xStateListItem ) ); } } if( pxTCB ! NULL ) { if( nondet_bool() ) { vListInsert( pxReadyTasksLists[ pxTCB-uxPriority ], ( pxTCB-xStateListItem ) ); } } /* *xTask NULL 是允许的——此时将使用 pxCurrentTCB */ *xTask pxTCB; pxCurrentTCB xUnconstrainedTCB(); if( pxCurrentTCB NULL ) { return pdFAIL; } if( nondet_bool() ) { vListInsert( pxReadyTasksLists[ pxCurrentTCB-uxPriority ], ( pxCurrentTCB-xStateListItem ) ); /* 为覆盖率推进当前任务指针 */ listGET_OWNER_OF_NEXT_ENTRY( pxCurrentTCB, pxReadyTasksLists[ pxCurrentTCB-uxPriority ] ); } return pdPASS; }其中prvInitialiseTaskLists()是tasks.c内部的静态函数通过FREERTOS_MODULE_TEST宏见 Makefile.json 的DEF配置将其暴露给测试代码——这是 FreeRTOS CBMC 证明中为访问内核内部符号而采用的通用手法在TaskCreate、TaskDelay、TaskDelete、TaskResumeAll、TaskSwitchContext等兄弟证明的tasks_test_access_functions.h中均有相同的调用模式。3.3 非受限 TCB 构造xUnconstrainedTCB()同一文件中的xUnconstrainedTCB()负责在 CBMC 的符号堆上分配一个 TCB并赋予其看似合法但值不确定的成员TaskHandle_t xUnconstrainedTCB( void ) { TCB_t * pxTCB pvPortMalloc( sizeof( TCB_t ) ); uint8_t ucStaticAllocationFlag; if( pxTCB NULL ) { return NULL; } __CPROVER_assume( pxTCB-uxPriority configMAX_PRIORITIES ); vListInitialiseItem( ( pxTCB-xStateListItem ) ); vListInitialiseItem( ( pxTCB-xEventListItem ) ); listSET_LIST_ITEM_OWNER( ( pxTCB-xStateListItem ), pxTCB ); listSET_LIST_ITEM_OWNER( ( pxTCB-xEventListItem ), pxTCB ); if( nondet_bool() ) { listSET_LIST_ITEM_VALUE( ( pxTCB-xStateListItem ), pxTCB-uxPriority ); } else { listSET_LIST_ITEM_VALUE( ( pxTCB-xStateListItem ), portMAX_DELAY ); } if( nondet_bool() ) { listSET_LIST_ITEM_VALUE( ( pxTCB-xEventListItem ), ( TickType_t ) configMAX_PRIORITIES - ( TickType_t ) pxTCB-uxPriority ); } else { listSET_LIST_ITEM_VALUE( ( pxTCB-xEventListItem ), portMAX_DELAY ); } return pxTCB; }设计意图解读TCB 也从堆上分配pvPortMalloc( sizeof( TCB_t ) )使 CBMC 能跟踪该内存的分配与释放进而验证vTaskPrioritySet对 TCB 的读写均落在合法分配区间内优先级约束__CPROVER_assume( pxTCB-uxPriority configMAX_PRIORITIES )保证vListInsert( pxReadyTasksLists[ uxPriority ], ... )的数组下标不越界——这正是证明就绪列表索引安全的关键列表项双向链指针由vListInitialiseItem初始化owner 指向自身 TCB列表项 value 非确定性设置状态列表项xStateListItem的 value 要么是优先级要么是portMAX_DELAY事件列表项xEventListItem的 value 要么是configMAX_PRIORITIES - uxPriorityFreeRTOS 事件列表按优先级倒序排序的经典取值要么是portMAX_DELAY。这种非确定性覆盖了vTaskPrioritySet内部对列表项 value 的比较与插入排序分支。四、证明如何映射到vTaskPrioritySet的真实实现虽然本仓库的FreeRTOS/Source目录在当前快照中未包含tasks.c源码内核通过 submodule 引入但从 harness 结构可以清晰推断被证明函数的内部行为vTaskPrioritySet( xTask, uxNewPriority )首先解析目标任务若xTask NULL则改用pxCurrentTCB这正是原文档强调任务句柄可以为 NULL的原因若目标任务的当前优先级uxCurrentPriority uxNewPriority函数直接返回否则将任务从原就绪列表摘除、更新uxPriority字段与两个列表项的 value再按新优先级重新插入pxReadyTasksLists[ uxNewPriority ]若新优先级高于当前正在运行任务则触发taskYIELD()即宏展开后的portYIELD()在模拟器端口下最终会调用被假设内存安全的vPortGenerateSimulatedInterrupt或相关端口机制当configUSE_MUTEXES启用时vTaskPrioritySet还会调用xTaskPriorityDisinherit或触发xTaskPriorityInherit相关逻辑这些函数被登记在 cbmc-viewer.json 的expected-missing-functions中作为内存安全假设处理。而 harness 中将任务可能不止一个非确定性插入就绪列表、pxCurrentTCB也可能被listGET_OWNER_OF_NEXT_ENTRY推进的设定正是为了让上述摘除→改值→重插路径与触发调度路径都被符号执行充分覆盖。五、构建与运行Makefile.json 深度解读每个证明目录下的 Makefile.json 是构建配置内容如下{ ENTRY: TaskPrioritySet, DEF: [ FREERTOS_MODULE_TEST, mtCOVERAGE_TEST_MARKER()__CPROVER_assert(1, \Coverage marker\), configUSE_TRACE_FACILITY0, configGENERATE_RUN_TIME_STATS0 ], CBMCFLAGS: [ --unwind 1, --unwindset prvInitialiseTaskLists.0:8,vListInsert.0:3 ], OBJS: [ $(ENTRY)_harness.goto, $(FREERTOS)/Source/tasks.goto, $(FREERTOS)/Source/list.goto ], INC: [ $(FREERTOS)/Test/CBMC/proofs/Task/TaskPrioritySet/ ] }逐项说明配置项值作用ENTRYTaskPrioritySet声明证明入口名用于生成目标文件名DEFFREERTOS_MODULE_TEST使tasks.c内部的静态函数如prvInitialiseTaskLists、vListInsert相关内部符号对测试代码可见是 harness 能调用内核内部函数的前提DEFmtCOVERAGE_TEST_MARKER()__CPROVER_assert(1, ...)将覆盖标记宏替换为恒真断言把覆盖率信息转化为可追踪的 CBMC 断言用于统计分支覆盖率DEFconfigUSE_TRACE_FACILITY0、configGENERATE_RUN_TIME_STATS0裁剪无关特性缩小符号执行状态空间聚焦任务调度核心路径CBMCFLAGS--unwind 1全局循环展开 1 次该证明主要循环是插入/遍历操作CBMCFLAGS--unwindset prvInitialiseTaskLists.0:8,vListInsert.0:3对prvInitialiseTaskLists主循环展开 8 次对应就绪列表数组大小与configMAX_PRIORITIES 7匹配、对vListInsert主循环展开 3 次保证链表插入排序循环被完整展开又不至于状态爆炸OBJStasks.goto、list.goto参与证明的 goto 二进制对象任务调度核心与链表实现INC本证明目录头文件搜索路径提供cbmc.h等CBMC 的--unwindset展开次数必须与分析对象的循环上界匹配configMAX_PRIORITIES在 patches/FreeRTOSConfig.h 中被定义为7prvInitialiseTaskLists需要对全部configMAX_PRIORITIES个就绪列表调用vListInitialise展开 8 次正好覆盖完整循环含循环条件检查而vListInsert插入排序的最坏情况扫描次数有限展开 3 次即足以穷尽该循环的路径。运行证明运行环境要求详见 FreeRTOS/Test/CBMC/README.md前置依赖Python ≥ 3.7、Make、CBMC 工具链cbmc、goto-cc、goto-instrument、cbmc-viewer64 位 Linux 上还需安装 32 位 gcc 库如sudo apt-get install gcc-multilib准备在仓库根目录执行git submodule update --init --recursive --checkout拉取内核子模块进入FreeRTOS/Test/CBMC/proofs执行python3 prepare.py生成各证明目录的 Makefile运行进入proofs/Task/TaskPrioritySet执行makeCBMC 将结合本证明的Makefile.json生成 goto 二进制并执行有界模型检查查看结果报告生成于html子目录打开html/index.html查看 HTML 报告若证明通过Errors部分显示None。整个proofs目录还包含TaskCreate、TaskDelete、TaskDelay、TaskResumeAll、TaskSwitchContext等同系列任务证明见 proofs/Task 目录它们共享tasks_test_access_functions.h这一模式TaskPrioritySet证明可以作为理解整套 FreeRTOS CBMC 基础设施的切入点。六、证明的局限性与工程实践启示有界证明而非全量证明--unwind 1与--unwindset表明该证明在给定展开界内穷举路径若循环展开次数不足以覆盖所有迭代证明结果只能覆盖界内行为。这也是原文档标注work-in-progress的原因之一。假设驱动的折中vPortEnterCritical/vPortExitCritical/vPortGenerateSimulatedInterrupt以及优先级继承相关函数被假定内存安全意味着证明的结论依赖于这些假设成立。若内核后续改动影响这些函数的共享内存语义需要重新评估假设。与覆盖率工具协同mtCOVERAGE_TEST_MARKER的替换使 CBMC 能报告哪些分支未被覆盖配合 harness 中大量的nondet_bool()非确定性分支如任务是否插入就绪列表、pxCurrentTCB是否推进在证明正确性的同时兼顾了覆盖率最大化——harness 注释中多次出现 Needed for coverage 正是这一意图的直接体现。对于希望为自有 RTOS 内核或嵌入式组件编写形式化验证的开发者本证明提供了一个可复用的模板用__CPROVER_assume约束合法输入域用nondet_bool构造非确定性状态用内部符号暴露宏如FREERTOS_MODULE_TEST访问静态函数最后用--unwindset精确控制循环展开以平衡完备性与求解开销。这套方法论同样适用于其他链表、队列、内存池类内核数据结构的验证。【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考