Open access
Datum
2009Typ
- Report
ETH Bibliographie
yes
Altmetrics
Abstract
We investigate the idea of developing access control systems in Event-B by specifying separately the "insecure" target system and the security authorisation, then combining them together in order to construct a secure system. This is based on the work by Basin et. al. [6] where the chosen language is CSP-OZ. Moreover, in order to verify the secure system against some safety temporal properties, we propose an approach of constructing several abstract models corresponding to these properties, and using refinement to prove that the final system satisfies these properties. Mehr anzeigen
Persistenter Link
https://doi.org/10.3929/ethz-a-006733720Publikationsstatus
publishedZeitschrift / Serie
Technical reportBand
Verlag
ETH, Department of Computer ScienceThema
ACCESS CONTROL (OPERATING SYSTEMS); Security; SPEZIFIKATIONSSPRACHEN (SOFTWARE ENGINEERING); SPECIFICATION LANGUAGES (SOFTWARE ENGINEERING); Event-B; Access control; Temporal property; ZUGRIFFSKONTROLLE (BETRIEBSSYSTEME)Organisationseinheit
02150 - Dep. Informatik / Dep. of Computer Science03634 - Basin, David / Basin, David
Anmerkungen
Technical Reports D-INFK.ETH Bibliographie
yes
Altmetrics