Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals

Publikation: Bidrag til bog/antologi/rapport/konference proceedingKonferenceartikel i proceedingForskningpeer review


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.

TitelModel Checking Software, SPIN 2022 : 28th International Symposium, SPIN 2022, Proceedings
RedaktørerOwolabi Legunsen, Grigore Rosu
Antal sider18
Publikationsdato23 aug. 2022
ISBN (Trykt)978-3-031-15076-0
ISBN (Elektronisk)978-3-031-15077-7
StatusUdgivet - 23 aug. 2022
Begivenhed28th International Symposium on Model Checking of Software -
Varighed: 21 maj 202221 maj 2022


Konference28th International Symposium on Model Checking of Software
NavnLecture Notes in Computer Science


Dyk ned i forskningsemnerne om 'Statistical Model Checking for Probabilistic Hyperproperties of Real-Valued Signals'. Sammen danner de et unikt fingeraftryk.