Other formats:
BibTeX
LaTeX
RIS
@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 and 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, p.~405-456. ISSN~2398-7340. Available from: https://dx.doi.org/10.29007/1874.
|
