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

Warning

This publication doesn't include Institute of Computer Science. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

TUŠIL Jan SERBANUTA Traian OBDRŽÁLEK Jan

Year of publication 2023
Type Article in Proceedings
Conference Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
MU Faculty or unit

Faculty of Informatics

Citation
Web https://easychair.org/publications/paper/8vTf
Doi http://dx.doi.org/10.29007/1874
Keywords hyperproperties; k-safety; language-parametric; logic
Attached files
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info