FreeRTOS CBMC 记忆安全证明实战QueueReceiveFromISR 的形式化验证剖析【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS本文以 FreeRTOS 仓库中FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/目录下的 CBMCC Bounded Model Checker证明工程为核心逐文件解读其 README、harness 与 Makefile 配置讲清该证明证明了什么、假设了什么、如何运行。读完后你将掌握 FreeRTOS 内存安全形式化验证的完整方法论如何用非确定性nondeterministic建模构造任意合法状态的队列、如何用 harness 界定有界验证范围、以及如何用 CBMC 对xQueueReceiveFromISR这类 ISR 上下文 API 做自动化记忆安全证明。证明目标与范围该目录的 README.md 对证明范围做了明确声明原文信息如下Assuming the bound declared in the harness, this harness proves the memory safety the QueueReceiveFromISR abstracting away the task pool and concurrency related functions.即在 harness 所声明的界限bound前提下本证明证明了xQueueReceiveFromISR的记忆安全性memory safety并且证明过程抽象掉abstract away了任务池task pool与并发相关的函数。README 同时强调两点关键事实该证明处于进行中的工作work-in-progress状态证明的假设assumptions在 harness 中描述并且证明还额外假设以下三个函数本身是记忆安全的、且对本函数的记忆安全没有相关副作用vPortEnterCriticalvPortExitCriticalxTaskRemoveFromEventList这三点合起来勾勒出 CBMC 有界模型检查Bounded Model Checking的典型边界它不证明整个系统在任何调度下都正确而是证明在给定状态空间、给定端口函数行为假设下xQueueReceiveFromISR的任何可达执行路径都不会越界读写、不会栈溢出、不会解引用未分配内存。证明工程目录结构该证明目录包含 4 个文件各自职责清晰文件职责README.md声明证明目标、前提与额外假设QueueReceiveFromISR_harness.c证明入口构造非确定性队列状态并调用被测函数Makefile.json声明 CBMC 入口点、编译标志、参与验证的目标文件与预处理宏cbmc-viewer.json声明预期缺失的函数清单供 CBMC-viewer 生成报告时过滤噪音这是 CBMC 证明基础设施 的标准布局该基础设施的 README 说明proofs 目录下的每个叶子目录都是对 FreeRTOS 单个入口点记忆安全性的证明且持续集成系统会对每个 pull request 运行这些证明。Harness 深度解析如何构造任意合法状态的队列harness 是整个证明的灵魂完整源码见 QueueReceiveFromISR_harness.c第 32–56 行为核心逻辑/* If the item size is not bounded, the proof does not finish in a * reasonable time due to the involved memcpy commands. */ #ifndef MAX_ITEM_SIZE #define MAX_ITEM_SIZE 10 #endif void harness() { QueueHandle_t xQueue xUnconstrainedQueueBoundedItemSize( MAX_ITEM_SIZE ); BaseType_t * xHigherPriorityTaskWoken pvPortMalloc( sizeof( BaseType_t ) ); if( xQueue ) { void * pvBuffer pvPortMalloc( xQueue-uxItemSize ); if( !pvBuffer ) { xQueue-uxItemSize 0; } xQueueReceiveFromISR( xQueue, pvBuffer, xHigherPriorityTaskWoken ); } }harness 的四个设计要点值得逐条剖析1. MAX_ITEM_SIZE 有界假设——README 中the bound declared in the harness的实体注释说明得很直白如果元素尺寸不加以限制证明因内部涉及的 memcpy 操作而无法在合理时间内结束。harness 通过MAX_ITEM_SIZE默认值 10 对uxItemSize设定上限10 字节。这就是 README 首句 Assuming the bound declared in the harness 所指的具体界限——读者必须意识到证明结论依赖于此假设。2. xUnconstrainedQueueBoundedItemSize非确定性队列建模该辅助函数定义在 queue_init.h其建模手法是 CBMC 证明的核心技巧先通过__CPROVER_assume建立前提uxQueueLength 0、uxItemSize uxItemSizeBound即小于 10并假设存储大小与uxItemSize uxQueueStorageSize / uxQueueLength的关系以规避xQueueGenericCreate中乘法溢出的组合爆炸源码注释指出 QueueGenericCreate 不检查乘法溢出调用真实的xQueueGenericCreate得到一个结构真实的队列对象随后用nondet_int8_t()、nondet_UBaseType_t()等 CBMC 非确定性函数随机化所有可变字段cTxLock、cRxLock并假设锁值! 127这是 FreeRTOS 队列锁字段的饱和编码不变量、uxMessagesWaiting、两个等待任务列表的长度最后假设关键不变量uxMessagesWaiting uxLength队列不满——注释解释若初始状态不满足此不变量CBMC 证明将无法成功。换言之harness 生成的不是某一个具体队列而是所有满足结构性不变量的合法队列的超集。xQueueReceiveFromISR若能在所有这些状态下保持记忆安全证明即成立。3. pvPortMalloc 分配接收缓冲与唤醒标志pvBuffer通过pvPortMalloc( xQueue-uxItemSize )分配使接收目标是一块大小恰好等于元素尺寸的合法堆内存xHigherPriorityTaskWoken同样经堆分配。当分配失败时harness 将uxItemSize置 0——这是刻意覆盖元素尺寸为 0即事件信号队列这一分支路径让xQueueReceiveFromISR中if( pxQueue-uxItemSize ( UBaseType_t ) 0 )的 else 分支也被验证到。4. 只调用一次被测函数harness 对xQueueReceiveFromISR的调用恰好一次配合 Makefile 中的--unwind 1保证验证循环被精确限制在 harness 声明的有界范围内——这正是有界模型检查bounded的含义所在。Makefile.jsonCBMC 验证配置的逐项解读Makefile.json 是prepare.py生成平台相关 Makefile 的输入核心字段如下{ ENTRY: QueueReceiveFromISR, CBMCFLAGS: [ --unwind 1, --signed-overflow-check, --unsigned-overflow-check ], OBJS: [ $(ENTRY)_harness.goto, $(FREERTOS)/Source/queue.goto, $(FREERTOS)/Source/list.goto, $(FREERTOS)/Test/CBMC/proofs/CBMCStubLibrary/tasksStubs.goto ], DEF: [ configUSE_TRACE_FACILITY0, configGENERATE_RUN_TIME_STATS0, mtCOVERAGE_TEST_MARKER()__CPROVER_assert(1, \Coverage marker\) ], GENERATE_HEADER: [ queue_datastructure.h ] }各字段的含义ENTRY验证入口函数即QueueReceiveFromISRCBMC 从该函数出发的所有可达代码路径都是验证对象CBMCFLAGS--unwind 1将循环展开限制为 1 圈与 harness 的单次调用呼应--signed-overflow-check与--unsigned-overflow-check额外把有符号/无符号整数溢出也纳入检查断言因此该证明实际覆盖记忆安全 整数溢出两类缺陷OBJS参与验证的目标文件包括 harness 本身、FreeRTOS 内核子模块中的 queue.c即$(FREERTOS)/Source/queue.goto、list.c 以及 CBMCStubLibrary/tasksStubs.c 的桩库。注意Source/是内核子模块目录本地克隆前需执行git submodule update --init --recursive --checkout拉取见 CBMC READMEDEF通过预处理宏裁剪无关代码路径——关闭 trace 设施与运行时统计并将mtCOVERAGE_TEST_MARKER()改写为 CBMC 断言桩避免该宏成为未定义符号GENERATE_HEADER将queue_datastructure.h纳入生成头文件暴露Queue_t内部结构以便 harness 直接操作uxItemSize等字段harness 中的xQueue-uxItemSize正是依赖此头文件。桩库与被抽象掉的并发原语证明将任务池与并发相关函数抽象掉其工程实现体现在两处桩库tasksStubs.c 提供调度相关函数的桩实现例如xTaskCheckForTimeOut被建模为最多TASK_STUB_COUNTER_LIMIT次迭代内的非确定性超时默认 5 次可在 Makefile.json 中覆盖这正是把真实的时间轮询压缩为有界非确定性分支的典型手法xTaskGetSchedulerState则返回可配置的非确定性状态xStateexpected-missing-functions 声明cbmc-viewer.json 列出了vPortEnterCritical、vPortExitCritical、xTaskRemoveFromEventList、vTaskSuspendAll、xTaskPriorityInherit等共 22 个预期缺失的函数——即这些函数在验证模型中没有实体定义由 CBMC 按未定义行为自由化或按桩库提供CBMC-viewer 生成报告时会将这些符号从缺失函数错误清单中过滤掉。README 中对三个函数vPortEnterCritical、vPortExitCritical、xTaskRemoveFromEventList的记忆安全假设正是这一抽象机制的文档化表述。从源码结构看该抽象是合理的xQueueReceiveFromISR的记忆安全风险主要来自pxQueue、pvBuffer的越界访问而临界区进出与事件列表摘除属于端口/调度层职责将其假定为记忆安全不会掩盖队列自身的缺陷。如何运行该证明依据 Test/CBMC/README.md 的操作流程前置条件Python ≥ 3.7、Make64 位机器需安装 32 位 gcc 库如sudo apt-get install gcc-multilib安装cbmc、goto-cc、goto-instrument与cbmc-viewer命令行工具初始化子模块在仓库根目录执行git submodule update --init --recursive --checkout内核源码来自子模块生成 Makefile进入 proofs 目录后执行python3 prepare.py脚本会为每个证明目录含本目录生成平台相关 Makefile运行证明cd FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR make查看结果make生成 HTML/JSON 报告成功运行proof passes时 Errors 一节应为None。适用前提与结论边界使用或引用该证明的结论时必须牢记以下边界有界性结论依赖MAX_ITEM_SIZE10的元素尺寸界限与--unwind 1的循环界限二者均可在 harness 与 Makefile.json 中调整但放大后证明耗时可能急剧上升端口假设vPortEnterCritical/vPortExitCritical/xTaskRemoveFromEventList被假设为记忆安全且无相关副作用证明不覆盖这三个函数自身的正确性work-in-progress 状态README 明示该证明仍在迭代其假设集合以 harness 当前版本为准验证类型CBMC 提供的是记忆安全证明无越界、无未定义指针行为、无整数溢出不证明功能正确性、实时性或多任务并发正确性。这套harness Makefile.json 桩库 expected-missing-functions的四件套模式在 proofs/Queue/ 下的QueueReceive、QueuePeek、QueueGenericSendFromISR等兄弟证明中同样出现理解了QueueReceiveFromISR这一例即可举一反三地阅读 FreeRTOS 其余 CBMC 证明工程。【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考