Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

Abstract

Many security-related properties—such as non-interference—cannot be captured by traditional trace-based specification formalisms such as LTL. The reason is that they relate the events of two (or more) traces of the system, and LTL can only reason on one execution at a time. A number of hyper-property extensions of LTL have been proposed in the past few years, and case studies showing their ability to express interesting properties have also been shown. However, there has been less attention to hyper-properties for quantitative (timed) systems as well as very little work on developing a practically useful tool. Instead existing work focused on using ad-hoc implementations. In this paper we present a probabilistic hyper-property logic HPSTL for stochastic hybrid and timed systems and we show how to integrate the logic into existing statistical model checking tools. To show the feasibility of our approach we integrate the technique into a prototype implementation inside Uppaal SMC and apply it to the analysis of three side-channel attack examples. To our knowledge this is the first full implementation of a hyper logic inside a fully-fledged modelling environment.

Original languageEnglish
Title of host publicationModel Checking Software - 28th International Symposium, SPIN 2022, Proceedings : 28th International Symposium, SPIN 2022, Virtual Event, May 21, 2022, Proceedings
EditorsOwolabi Legunsen, Grigore Rosu
Number of pages18
Volume13255
PublisherSpringer
Publication date23 Aug 2022
Edition1
Pages61-78
ISBN (Print)978-3-031-15076-0
ISBN (Electronic)978-3-031-15077-7
DOIs
Publication statusPublished - 23 Aug 2022
Event28th International Symposium on Model Checking of Software -
Duration: 21 May 202221 May 2022
https://spin2022chi.web.illinois.edu/

Conference

Conference28th International Symposium on Model Checking of Software
Period21/05/202221/05/2022
Internet address
SeriesLecture Notes in Computer Science
ISSN0302-9743

Fingerprint

Dive into the research topics of 'Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals'. Together they form a unique fingerprint.

Cite this