Formal Verification of Machine-Code Systems by Translation of Simulable Descriptions

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21240%2F24%3A00376137" target="_blank" >RIV/68407700:21240/24:00376137 - isvavai.cz</a>

Result on the web

<a href="https://doi.org/10.1109/MECO62516.2024.10577942" target="_blank" >https://doi.org/10.1109/MECO62516.2024.10577942</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/MECO62516.2024.10577942" target="_blank" >10.1109/MECO62516.2024.10577942</a>

Result language

angličtina

Original language name

Formal Verification of Machine-Code Systems by Translation of Simulable Descriptions

Original language description

Correctness of safety- and security-critical systems can be ensured by formal verification. While formal verification of source-code and hardware systems is widely used, existing approaches to formal verification of machine code are severely limited in verification strength and processor choice. In this paper, a formal verification tool written in the Rust programming language is introduced, with emphasis on machine-code verification. The problems of previous tools are circumvented by abstraction refinement, an advanced formal verification technique. System behaviour is defined using simulation descriptions written in a limited subset of Rust, allowing straightforward extension of the tool to new architectures and processor model using architecture and processor manuals. A novel technique of translating the descriptions to their verification analogues at compile-time enables fast verification using abstraction refinement without any need for formal verification knowledge by the description writer.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

S - Specificky vyzkum na vysokych skolach

Publication year

2024

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

2024 13th Mediterranean Conference on Embedded Computing (MECO)

ISBN

979-8-3503-8757-5

ISSN

2377-5475

e-ISSN

2637-9511

Number of pages

4

Pages from-to

140-143

Publisher name

Institute of Electrical and Electronic Engineers

Place of publication

Piscataway

Event location

Budva

Event date

Jun 11, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001268606200105