Skip to Main content Skip to Navigation
New interface
Conference papers

Verified functional programming of an IoT operating system's bootloader

Shenghao Yuan 1 Jean-Pierre Talpin 1 
1 TEA - Tim, Events and Architectures
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The fault of one device on a grid may incur severe economical or physical damages. Among the many critical components in such IoT devices, the operating system's bootloader comes first to initiate the trusted function of the device on the network. However, a bootloader uses hardware-dependent features that make its functional correctness proof difficult. This paper uses verified programming to automate the verification of both the C libraries and assembly boot-sequence of such a, real-world, bootloader in an operating system for ARM-based IoT devices: RIOT. We first define the ARM ISA specification, semantics and properties in F to model its critical assembly code boot sequence. We then use Low , a DSL rendering a Clike memory model in F , to implement the complete bootloader library and verify its functional correctness and memory safety. Other than fixing potential faults and vulnerabilities in the source C and ASM bootloader, our evaluation provides an optimized and formally documented code structure, a reasonable specification/implementation ratio, a high degree of proof automation and an equally efficient generated code.
Document type :
Conference papers
Complete list of metadata
Contributor : Jean-Pierre Talpin Connect in order to contact the contributor
Submitted on : Wednesday, September 22, 2021 - 9:46:00 AM
Last modification on : Friday, August 5, 2022 - 2:54:52 PM


Files produced by the author(s)


  • HAL Id : hal-03343002, version 2


Shenghao Yuan, Jean-Pierre Talpin. Verified functional programming of an IoT operating system's bootloader. MEMOCODE 2021 - 19th ACM-IEEE International Conference on Formal Methods and Models for System Design, Nov 2021, Beijing, China. pp.1-16. ⟨hal-03343002v2⟩



Record views


Files downloads