Application of formal analysis to enhancing trust in a complex grid-based operating system

Benjamin Aziz

Research output: Contribution to conferencePaperpeer-review

171 Downloads (Pure)

Abstract

This paper presents a case study in the application of formal modelling and verification techniques to a large-scale distributed operating system for Grids called XtreemOS. The process algebraic language of applied pi-calculus is used to model one of the mutual authentication protocols in the XtreemOS trust model, and an associated tool called ProVerif is used to verify the data leakage and mutual authentication properties in the protocol. The results, beside enhancing the level of assurance of the protocol in a critical part of the system, contribute to better understanding of the level of detail in the protocol's specification hence enabling better implementation of the protocol.
Original languageEnglish
Publication statusPublished - 26 Jun 2012
Event3rd International ACM Sigsoft Symposium on Architecting Critical Systems 2012 - Bertinoro, Italy
Duration: 26 Jun 2012 → …

Conference

Conference3rd International ACM Sigsoft Symposium on Architecting Critical Systems 2012
Country/TerritoryItaly
CityBertinoro
Period26/06/12 → …

Fingerprint

Dive into the research topics of 'Application of formal analysis to enhancing trust in a complex grid-based operating system'. Together they form a unique fingerprint.

Cite this