Formally Verifying FreeRTOS’ Interprocess Communication Mechanism

FreeRTOS is a real-time kernel and set of libraries for Internet of Things (IoT) applications. The FreeRTOS kernel provides a portable abstraction layer, task scheduling and interprocess communication (IPC) mechanisms. The main IPC mechanism in FreeRTOS is a concurrent queue: a circular bu!er data structure that tasks and interrupt service routines use to exchange messages. As a fundamental building block for larger applications, the correctness of the queue implementation is vital. We have formally veri"ed the memory safety, thread safety and functional correctness of this queue implementation using deductive veri"cation. Our proofs are publicly available and give machine-checkable assurances of correctness that would be infeasible to obtain through testing alone.