Model checking the observational determinism security property using PROMELA and SPIN
| LEADER | caa a22 4500 | ||
|---|---|---|---|
| 001 | 605516243 | ||
| 003 | CHVBK | ||
| 005 | 20210128100713.0 | ||
| 007 | cr unu---uuuuu | ||
| 008 | 210128e20151101xx s 000 0 eng | ||
| 024 | 7 | 0 | |a 10.1007/s00165-014-0331-x |2 doi |
| 035 | |a (NATIONALLICENCE)springer-10.1007/s00165-014-0331-x | ||
| 245 | 0 | 0 | |a Model checking the observational determinism security property using PROMELA and SPIN |h [Elektronische Daten] |c [Maryam Dabaghchian, Mohammad Abdollahi Azgomi] |
| 520 | 3 | |a Observational determinism is a property that ensures the confidentiality in concurrent programs. It conveys that public variables are independent of private variables during the execution of programs, and the scheduling policy of threads. Different definitions for observational determinism have been proposed. On the other hand, observational determinism is not a standard property and it should be checked over two or more executions of a program. The self-composition approach allows comparing two different copies of a program using a single formula. In this paper, we propose a new specification for the observational determinism security property in linear temporal logic. We also present a general method to create the appropriate program model using the self-composition approach. Both the program model and the observational determinism property are encoded in embedded C codes in PROMELA using the SPIN model checker. The paper also discusses a method for the instrumentation of PROMELA code in order to encode the program model for specifying the observational determinism security property. | |
| 540 | |a British Computer Society, 2015 | ||
| 690 | 7 | |a Model checking |2 nationallicence | |
| 690 | 7 | |a Linear temporal logic (LTL) |2 nationallicence | |
| 690 | 7 | |a Information flow security |2 nationallicence | |
| 690 | 7 | |a Observational determinism |2 nationallicence | |
| 690 | 7 | |a SPIN |2 nationallicence | |
| 690 | 7 | |a PROMELA |2 nationallicence | |
| 700 | 1 | |a Dabaghchian |D Maryam |u Department of Computer Engineering, Science and Research Branch, Islamic Azad University, Tehran, Iran |4 aut | |
| 700 | 1 | |a Abdollahi Azgomi |D Mohammad |u Trsutworthy Computing Laboratory, School of Computer Engineering, Iran University of Science and Technology, Hengam St., Resalat Sq., Tehran, Iran |4 aut | |
| 773 | 0 | |t Formal Aspects of Computing |d Springer London |g 27/5-6(2015-11-01), 789-804 |x 0934-5043 |q 27:5-6<789 |1 2015 |2 27 |o 165 | |
| 856 | 4 | 0 | |u https://doi.org/10.1007/s00165-014-0331-x |q text/html |z Onlinezugriff via DOI |
| 898 | |a BK010053 |b XK010053 |c XK010000 | ||
| 900 | 7 | |a Metadata rights reserved |b Springer special CC-BY-NC licence |2 nationallicence | |
| 908 | |D 1 |a research-article |2 jats | ||
| 949 | |B NATIONALLICENCE |F NATIONALLICENCE |b NL-springer | ||
| 950 | |B NATIONALLICENCE |P 856 |E 40 |u https://doi.org/10.1007/s00165-014-0331-x |q text/html |z Onlinezugriff via DOI | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Dabaghchian |D Maryam |u Department of Computer Engineering, Science and Research Branch, Islamic Azad University, Tehran, Iran |4 aut | ||
| 950 | |B NATIONALLICENCE |P 700 |E 1- |a Abdollahi Azgomi |D Mohammad |u Trsutworthy Computing Laboratory, School of Computer Engineering, Iran University of Science and Technology, Hengam St., Resalat Sq., Tehran, Iran |4 aut | ||
| 950 | |B NATIONALLICENCE |P 773 |E 0- |t Formal Aspects of Computing |d Springer London |g 27/5-6(2015-11-01), 789-804 |x 0934-5043 |q 27:5-6<789 |1 2015 |2 27 |o 165 | ||