Cartesian Reachability Logic: A Language-parametric Logic for
Verifying k-Safety Properties

D 2023

Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties

TUŠIL, Jan, Traian SERBANUTA a Jan OBDRŽÁLEK

Základní údaje

Originální název

Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties

Autoři

TUŠIL, Jan (203 Česká republika, domácí), Traian SERBANUTA (642 Rumunsko) a Jan OBDRŽÁLEK (203 Česká republika, garant, domácí)

Vydání

Manchester, Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, od s. 405-456, 52 s. 2023

Nakladatel

EasyChair

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Velká Británie a Severní Irsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Kód RIV

RIV/00216224:14330/23:00131016

Organizační jednotka

Fakulta informatiky

ISSN

DOI

http://dx.doi.org/10.29007/1874

Klíčová slova anglicky

hyperproperties; k-safety; language-parametric; logic

Štítky

core_B, firank_B, Formela

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 7. 4. 2024 23:03, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We introduce a language-parametric calculus for k-safety verification - Cartesian Reachability logic (CRL). In recent years, formal verification of hyperproperties has become an important topic in the formal methods community. An interesting class of hyperproperties is known as k-safety properties, which express the absence of a bad k-tuple of execution traces. Many security policies, such as noninterference, and functional properties, such as commutativity, monotonicity, and transitivity, are k-safety properties. A prominent example of a logic that can reason about k-safety properties of software systems is Cartesian Hoare logic (CHL). However, CHL targets a specific, small imperative language. In order to use it for sound verification of programs in a different language, one needs to extend it with the desired features or hand-craft a translation. Both these approaches require a lot of tedious, error-prone work. Unlike CHL, CRL is language-parametric: it can be instantiated with an operational semantics (of a certain kind) of any deterministic language. Its soundness theorem is proved once and for all, with no need to adapt or re-prove it for different languages or their variants. This approach can significantly reduce the development costs of tools and techniques for sound k-safety verification of programs in deterministic languages: for example, of smart contracts written for EVM (the language powering the Ethereum blockchain), which already has an operational semantics serving as a reference.

Návaznosti

MUNI/A/1081/2022, interní kód MU

Název: Modelování, analýza a verifikace (2023)

Investor: Masarykova univerzita, Modelování, analýza a verifikace (2023)

MUNI/A/1433/2022, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 23

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 23

Přiložené soubory

Cartesian_Reachability_Logic_A_Language-parametric_Logic_for_Verifying_k-Safety_Properties.pdf

Požádat o autorskou verzi souboru

Citovat

TUŠIL, Jan, Traian SERBANUTA a Jan OBDRŽÁLEK. Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties. Online. In Ruzica Piskac and Andrei Voronkov. Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Manchester: EasyChair, 2023, s. 405-456. ISSN 2398-7340. Dostupné z: https://dx.doi.org/10.29007/1874.

@inproceedings{2292879,
   author = {Tušil, Jan and Serbanuta, Traian and Obdržálek, Jan},
   address = {Manchester},
   booktitle = {Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
   doi = {http://dx.doi.org/10.29007/1874},
   editor = {Ruzica Piskac and Andrei Voronkov},
   keywords = {hyperproperties; k-safety; language-parametric; logic},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Manchester},
   pages = {405-456},
   publisher = {EasyChair},
   title = {Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties},
   url = {https://easychair.org/publications/paper/8vTf},
   year = {2023}
}

TY  - JOUR
ID  - 2292879
AU  - Tušil, Jan - Serbanuta, Traian - Obdržálek, Jan
PY  - 2023
TI  - Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties
PB  - EasyChair
CY  - Manchester
KW  - hyperproperties
KW  - k-safety
KW  - language-parametric
KW  - logic
UR  - https://easychair.org/publications/paper/8vTf
N2  - We introduce a language-parametric calculus for k-safety verification - Cartesian Reachability logic (CRL). In recent years, formal verification of hyperproperties has become an important topic in the formal methods community. An interesting class of hyperproperties is known as k-safety properties, which express the absence of a bad k-tuple of execution traces. Many security policies, such as noninterference, and functional properties, such as commutativity, monotonicity, and transitivity, are k-safety properties. A prominent example of a logic that can reason about k-safety properties of software systems is Cartesian Hoare logic (CHL). However, CHL targets a specific, small imperative language. In order to use it for sound verification of programs in a different language, one needs to extend it with the desired features or hand-craft a translation. Both these approaches require a lot of tedious, error-prone work. Unlike CHL, CRL is language-parametric: it can be instantiated with an operational semantics (of a certain kind) of any deterministic language. Its soundness theorem is proved once and for all, with no need to adapt or re-prove it for different languages or their variants. This approach can significantly reduce the development costs of tools and techniques for sound k-safety verification of programs in deterministic languages: for example, of smart contracts written for EVM (the language powering the Ethereum blockchain), which already has an operational semantics serving as a reference.
ER  -

TUŠIL, Jan, Traian SERBANUTA a Jan OBDRŽÁLEK. Cartesian Reachability Logic: A Language-parametric Logic for Verifying k-Safety Properties. Online. In Ruzica Piskac and Andrei Voronkov. \textit{Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning}. Manchester: EasyChair, 2023, s.~405-456. ISSN~2398-7340. Dostupné z: https://dx.doi.org/10.29007/1874.

Podrobný výpis o publikaci