CISPA
Browse
cispa_all_3199.pdf (640.78 kB)

Verified Rust Monitors for Lola Specifications

Download (640.78 kB)
conference contribution
posted on 2023-11-29, 18:13 authored by Bernd FinkbeinerBernd Finkbeiner, Stefan Oswald, Noemi Passing, Maximilian Schwenger
The safety of cyber-physical systems rests on the correctness of their monitoring mechanisms. This is problematic if the specification of the monitor is implemented manually or interpreted by unreliable software. We present a verifying compiler that translates specifications given in the stream-based monitoring language Lola to implementations in Rust. The generated code contains verification annotations that enable the Viper toolkit to automatically prove functional correctness, absence of memory faults, and guaranteed termination. The compiler parallelizes the evaluation of different streams in the monitor based on a dependency analysis of the specification. We present encouraging experimental results obtained with monitor specifications found in the literature. For every specification, our approach was able to either produce a correctness proof or to uncover errors in the specification.

History

Preferred Citation

Bernd Finkbeiner, Stefan Oswald, Noemi Passing and Maximilian Schwenger. Verified Rust Monitors for Lola Specifications. In: International Conference on Runtime Verification (RV). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Conference on Runtime Verification (RV)

Legacy Posted Date

2020-09-14

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3199, title = "Verified Rust Monitors for Lola Specifications", author = "Finkbeiner, Bernd and Oswald, Stefan and Passing, Noemi and Schwenger, Maximilian", booktitle="{International Conference on Runtime Verification (RV)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC