Publication Type

Conference Proceeding Article

Version

acceptedVersion

Publication Date

4-2025

Abstract

The analysis of timed properties of programs is a complex task, as it is highly dependent on both the software and the hardware. In this work, we propose a framework for modeling with timed formal models the execution of programs, taking into account the micro-architecture of the machine on which it executes. We model both the program, at the instruction set architecture level, and the hardware, including the processor micro-architecture, using time Petri nets. Our implementation uses the ARM Cortex-M instruction set architecture and a hardware architecture representative of microcontrollers used in IoT nodes. The whole translation is fully automated and allows, starting from binary code, to automatically produce the models usable by the state-of-the-art time Petri net model checker Roméo. In addition, and as a proof of concept, we show how we can check, and enforce to some extent, opacity properties on programs, leveraging the ability of Roméo to verify a parametric timed extension of the classical computation tree logic.

Keywords

execution time, formal methods, program verification, timing attacks

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

SAC '25: Proceedings of the 40th Annual ACM Symposium on Applied Computing, March 30 - April 4, Catania

First Page

1998

Last Page

2006

ISBN

9798400706295

Identifier

10.1145/3672608.3707861

Publisher

Association for Computing Machinery

City or Country

New York

Additional URL

https://doi.org/10.1145/3672608.3707861

Download

Share

COinS