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

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2024

Kód důvěrnosti údajů

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

Název statě ve sborníku

2024 13th Mediterranean Conference on Embedded Computing (MECO)

ISBN

979-8-3503-8757-5

ISSN

2377-5475

e-ISSN

2637-9511

Počet stran výsledku

4

Strana od-do

140-143

Název nakladatele

Institute of Electrical and Electronic Engineers

Místo vydání

Piscataway

Místo konání akce

Budva

Datum konání akce

11. 6. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001268606200105