企业官网建设流程全解析

FreeRTOS 内存安全证明：基于 CBMC 对 TaskPrioritySet 的形式化验证深度解析

【免费下载链接】FreeRTOS'Classic' 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 Checker（CBMC）形式化验证 FreeRTOS 任务优先级设置函数vTaskPrioritySet的内存安全性。文章覆盖证明原理、harness 测试代码、任务列表初始化、证明假设、构建配置与运行方法，帮助读者掌握 FreeRTOS 官方 CBMC 证明基础设施的用法，并理解嵌入式 RTOS 内核函数静态形式化验证的完整工程实践。

一、为什么需要为 TaskPrioritySet 编写 CBMC 证明

FreeRTOS 的vTaskPrioritySet用于在运行时修改任务优先级，其实现涉及多个全局链表（就绪列表pxReadyTasksLists等）的插入、移除与排序操作。这类函数直接操作指针与链表，一旦出现越界、空指针解引用、未初始化内存访问或整数溢出，将导致内核内存破坏，且难以通过常规运行时测试完整覆盖。

CBMC（C 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 证明假设：三个被信任的函数

原文档列出以下三个函数被假定为内存安全且对目标函数的内存安全不产生相关副作用：

• vPortEnterCritical
• vPortExitCritical
• vPortGenerateSimulatedInterrupt

这符合 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 ); } }

关键设计点如下：

1. 优先级合法化假设：__CPROVER_assume( uxNewPriority < configMAX_PRIORITIES )将新优先级约束为合法值。其作用有二：一是避免触发configASSERT（对应 harness 注释 "avoids failed assert"）；二是把符号执行空间限定在 API 契约允许的范围内——vTaskPrioritySet作为公开 API，其前置条件本就是"优先级小于configMAX_PRIORITIES"。在 patches/FreeRTOSConfig.h 中该值被配置为7。

2. 两次调用xPrepareTaskLists的用意：注释 "Check that this second invocation of xPrepareTaskLists is needed" 表明，第二次调用用于扩展状态空间。xPrepareTaskLists内部大量使用nondet_bool()做非确定性分支，两次调用会产生不同的链表填充组合，从而覆盖vTaskPrioritySet中更多执行路径（例如目标任务是否已挂在就绪列表、pxCurrentTCB是否也在就绪列表中等组合）。

3. 对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 - uxPriority（FreeRTOS 事件列表按优先级倒序排序的经典取值），要么是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_FACILITY=0", "configGENERATE_RUN_TIME_STATS=0" ], "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/" ] }

逐项说明：

CBMC 的--unwindset展开次数必须与分析对象的循环上界匹配：configMAX_PRIORITIES在 patches/FreeRTOSConfig.h 中被定义为7，prvInitialiseTaskLists需要对全部configMAX_PRIORITIES个就绪列表调用vListInitialise，展开 8 次正好覆盖完整循环（含循环条件检查），而vListInsert插入排序的最坏情况扫描次数有限，展开 3 次即足以穷尽该循环的路径。

运行证明

运行环境要求（详见 FreeRTOS/Test/CBMC/README.md）：

1. 前置依赖：Python ≥ 3.7、Make、CBMC 工具链（cbmc、goto-cc、goto-instrument）、cbmc-viewer；64 位 Linux 上还需安装 32 位 gcc 库（如sudo apt-get install gcc-multilib）；
2. 准备：在仓库根目录执行git submodule update --init --recursive --checkout拉取内核子模块；进入FreeRTOS/Test/CBMC/proofs执行python3 prepare.py生成各证明目录的 Makefile；
3. 运行：进入proofs/Task/TaskPrioritySet执行make，CBMC 将结合本证明的Makefile.json生成 goto 二进制并执行有界模型检查；
4. 查看结果：报告生成于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精确控制循环展开以平衡完备性与求解开销。这套方法论同样适用于其他链表、队列、内存池类内核数据结构的验证。

【免费下载链接】FreeRTOS'Classic' FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS