FreeRTOS CBMC 证明实战对 xQueueCreateMutex 的完全无约束输入做内存安全验证【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS本篇指南围绕 QueueCreateMutex 证明的 README 展开讲清 FreeRTOS 如何用 C Bounded Model CheckerCBMC对队列/互斥量创建函数xQueueCreateMutex做完全无约束输入下的内存安全证明。读完你将理解证明 harness 如何构造非确定性输入、Makefile.json中每个 CBMC 参数的含义、缺失函数假设expected missing functions机制的作用以及如何在本机完整跑通这一证明并解读 HTML/JSON 报告。1. 背景Test/CBMC 证明基础设施FreeRTOS 仓库在 Test/CBMC 目录下内置了一套内存安全自动化证明基础设施。根据该目录的顶层 README每个proofs下的叶子目录对应 FreeRTOS 中单个入口函数的一条内存安全证明CI 系统会对每个 Pull Request 运行这些证明开发者也可以在本机运行证明使用开源静态分析工具 CBMC 执行依赖cbmc、goto-ccWindows 上为goto-cl、goto-instrument三个命令生成报告还需要cbmc-viewer。本机运行的基本流程摘自 CBMC 顶层 README环境要求Python 3.7、Make64 位机器需安装 32 位 gcc 库Linux 上为sudo apt-get install gcc-multilibWindows 可用 WSL。拉取内核子模块本仓库以子模块方式引入 FreeRTOS 内核源码即$(FREERTOS)指向的位置git submodule update --init --recursive --checkout进入proofs目录仓库内为FreeRTOS/Test/CBMC/proofs/生成各证明的 Makefilepython3 prepare.py如需交叉生成 Linux/Windows 的 Makefile可传--system linux或--system windows。进入目标证明目录本文即FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/执行make可能耗时较长。结果HTML 报告位于html/html/index.htmlJSON 报告位于html/json成功时报告中Errors一节显示None。此外patches 目录存放证明前必须打补丁的内容——主要为移除源码中的static与volatile限定符因为 CBMC 对这类限定符的处理会妨碍跨编译单元的分析。Makefile.json 里的$(FREERTOS)/Source/queue.goto等.goto文件正是在此流程下由内核的queue.c、list.c编译转换而来的中间对象。2. 本证明的目标与假设原文档核心内容QueueCreateMutex/README.md 明确了这条证明的定位This harness proves the memory safety of QueueCreateMutex for totally unconstrained input.即证明对象是QueueCreateMutex输入是完全无约束的——不是构造特定测试向量而是让 CBMC 对该函数的参数取所有可表示值做有界模型检查验证其在任何输入下都不会发生越界读/写、解引用非法指针等内存安全错误。README 同时声明这是一个进行中的证明work-in-progress除了 harness 内部描述的假设外它还假设以下函数内存安全且没有影响本函数内存安全性的副作用vPortEnterCriticalvPortExitCriticalvPortGenerateSimulatedInterruptxTaskGetSchedulerStatexTaskPriorityDisinheritxTaskRemoveFromEventList这份清单与 cbmc-viewer.json 中的expected-missing-functions名单相互印证expected-missing-functions列出的是链接阶段允许缺失的函数含上述六个以及vPortEnterCritical/vPortExitCritical等 port 层符号。也就是说证明不链接完整的任务/移植层实现而是把这些符号当作抽象掉的外部行为来处理——这正是假设其内存安全且无相关副作用在工具层面的落地方式。3. 证明 harness3 行代码实现完全无约束输入harness 源码见 QueueCreateMutex_harness.c剥离许可证头后核心仅 5 行#include FreeRTOS.h #include queue.h #include cbmc.h void harness() { uint8_t ucQueueType; xQueueCreateMutex( ucQueueType ); }要点解析harness()是 CBMC 的入口约定函数等价于对xQueueCreateMutex做一次全输入空间调用。ucQueueType是未初始化的局部变量。在 CBMC 的语义中读取未初始化对象会得到非确定性nondeterministic值因此这一个uint8_t就覆盖了 0~255 的全部可能取值——这就是totally unconstrained input的实现手法不写断言、不构造用例把输入域交给模型检查器穷举。cbmc.h见 include/cbmc.h提供证明 harness 的公共工具nondet_*()非确定性取值函数、safeMalloc、pvPortMalloc的非确定性桩可能返回NULL且约定申请 0 字节必返回NULL、__CPROVER_assert相关的调试宏以及CBMC_BITS/CBMC_MAX_OBJECT_SIZE这类与 CBMC 指针编码对象 id 偏移相关的边界常量。4. 证明配置 Makefile.json 逐项解读本证明的构建与检查参数集中在 Makefile.jsonprepare.py会据此展开为实际 Makefile{ ENTRY: QueueCreateMutex, CBMCFLAGS: [ --unwind 1, --signed-overflow-check, --unsigned-overflow-check ], OBJS: [ $(ENTRY)_harness.goto, $(FREERTOS)/Source/queue.goto, $(FREERTOS)/Source/list.goto ], DEF: [ configUSE_TRACE_FACILITY0, configGENERATE_RUN_TIME_STATS0 ] }字段取值含义ENTRYQueueCreateMutex被证明的入口函数也用于定位$(ENTRY)_harness.goto即上文的 harness 编译产物CBMCFLAGS--unwind 1将循环展开次数有界为 1——这是有界模型检查的体现证明只对展开 1 层循环内的行为给出结论--signed-overflow-check/--unsigned-overflow-check额外开启有符号/无符号整数溢出检查把溢出也纳入错误类别OBJS3 个.goto目标harness 内核queue.clist.c。即本证明的分析闭包只包含队列层及其直接依赖的链表层不引入完整任务调度实现DEFconfigUSE_TRACE_FACILITY0、configGENERATE_RUN_TIME_STATS0关闭 trace 设施与运行时统计减少被分析代码路径两个值得注意的配置细节分析闭包最小化只链接queue.goto和list.goto配合第 2 节的缺失函数假设构成核心逻辑真实分析 周边依赖抽象的典型证明切分策略。架构无关的 portmacro证明不依赖任何具体 MCU 移植层而是使用 include/portmacro.h。该文件自述目标是architecture-independent所有常量都用#ifndef包裹允许各证明在自己的 Makefile 中覆写所需常量。例如其中portENTER_CRITICAL()直接映射到外部函数vPortEnterCritical()、portYIELD()映射到vPortGenerateSimulatedInterrupt(portINTERRUPT_YIELD)——这两个恰好都在本证明的假设内存安全清单中。5. 在本机运行这条证明# 1. 仓库根目录本仓库为 FreeRTOS 仓库根拉取子模块 git submodule update --init --recursive --checkout # 2. 生成各证明的 Makefile脚本位于 proofs/ 目录 cd FreeRTOS/Test/CBMC/proofs python3 prepare.py # 3. 进入本证明目录执行 cd Queue/QueueCreateMutex make运行后检查报告HTML 报告FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/html/html/index.html用浏览器打开Errors一节为None即证明通过JSON 报告FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/html/json。报告生成依赖 cbmc-viewer.json 的约定{ expected-missing-functions: [ vApplicationTickHook, pxPortInitialiseStack, vPortEnterCritical, vPortExitCritical, xTaskPriorityDisinherit, xTaskRemoveFromEventList, ... 共 21 个 port/task 层符号 ], proof-name: QueueCreateMutex, proof-root: Test/CBMC/proofs }expected-missing-functions允许 cbmc-viewer 在链接期预期这些符号缺席而不报链接错误proof-name是报告中的证明标识proof-root指明证明树在仓库中的相对位置。6. 在 Queue 证明族中的位置与适用边界proofs/Queue/目录是一套完整的队列 API 验证集QueueCreateMutex 是其中一环。同级的兄弟证明可在 proofs/Queue 下逐一查看包括QueueCreateCountingSemaphore、QueueCreateCountingSemaphoreStatic、QueueCreateMutexStatic、QueueGenericCreate、QueueGenericCreateStatic、QueueGenericReset、QueueGenericSend/QueueGenericSendFromISR、QueueGetMutexHolder/QueueGetMutexHolderFromISR、QueueGiveFromISR、QueueGiveMutexRecursive/QueueTakeMutexRecursive、QueueMessagesWaiting、QueuePeek、QueueReceive/QueueReceiveFromISR、QueueSemaphoreTake、QueueSpacesAvailable以及内部函数prvCopyDataToQueue、prvNotifyQueueSetContainer、prvUnlockQueue。对比这些证明的Makefile.json与 harness可以直观看到同一队列源码、不同入口、不同抽象假设的参数化验证思路。适用边界与限制均以仓库文档为准原 README 自述该证明是work-in-progress其完整假设集合described in the harness并依赖第 2 节列出的六个外部函数假设引用其结论时应带上这一前提。--unwind 1意味着循环被有界处理属于有界内存安全证明而非无条件全路径证明。证明对象是创建互斥量/队列这一入口的内存安全不覆盖运行时调度、优先级继承等并发行为正确性——这些由xTaskPriorityDisinherit等假设符号承接不在本证明分析范围内。内核queue.c/list.c本体位于子模块$(FREERTOS)/Source/若子模块未初始化prepare.py与make无法解析这些源文件。7. 小结这条证明展示了 FreeRTOS 用 CBMC 做入口级内存安全证明的完整范式输入无约束化harness 用一个未初始化即非确定性的uint8_t参数调用xQueueCreateMutex让模型检查器穷举全部 256 种取值QueueCreateMutex_harness.c分析闭包最小化只编译queue.clist.c两个对象其余 21 个 port/task 符号在 cbmc-viewer.json 中声明为预期缺失并假定内存安全参数可审计--unwind 1、溢出检查开关、编译宏全部显式写在 Makefile.json 中配合 patches 的static/volatile剥离使证明在哪份源码、以什么配置、做什么假设完全可复核可复现按 CBMC 顶层 README 的prepare.pymake流程即可在本机复跑并查看 HTML/JSON 报告。【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考