Skip to Main content Skip to Navigation
Conference papers

Verifying Observational Determinism

Abstract : This paper proposes an approach to verify information flow security of concurrent programs. It discusses a hyperproperty called observational determinism which aims to ensure secure information flow in concurrent programs, and proves how this hyperproperty can be verified by stutter equivalence checking. More precisely, it defines observational determinism in terms of stutter equivalence of all traces having the same low initial value and shows how stutter trace equivalence can be verified by computing a divergence stutter bisimulation quotient. The approach is illustrated by verifying a small example.
Document type :
Conference papers
Complete list of metadatas

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01345097
Contributor : Hal Ifip <>
Submitted on : Wednesday, July 13, 2016 - 10:52:57 AM
Last modification on : Wednesday, July 13, 2016 - 11:18:42 AM

File

337885_1_En_6_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Jaber Karimpour, Ayaz Isazadeh, Ali Noroozi. Verifying Observational Determinism. 30th IFIP International Information Security Conference (SEC), May 2015, Hamburg, Germany. pp.82-93, ⟨10.1007/978-3-319-18467-8_6⟩. ⟨hal-01345097⟩

Share

Metrics

Record views

90

Files downloads

219