Change search
ReferencesLink to record
Permanent link

Direct link
Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Show others and affiliations
Number of Authors: 5
2013 (English)Conference paper (Refereed)
Abstract [en]

A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information flow security for a simple separation kernel for ARMv7. Previous work on information flow kernel security leaves communication to be handled by model-external means, and cannot be used to draw conclusions when there is explicit interaction between partitions. We propose a different approach where communication between partitions is made explicit and the information flow is analyzed in the presence of such a channel. Limiting the kernel functionality as much as meaning-fully possible, we accomplish a detailed analysis and verification of the system, proving its correctness at the level of the ARMv7 assembly. As a sanity check we show how the security condition is reduced to noninterference in the special case where no communication takes place. The verification is done in HOL4 taking the Cambridge model of ARM as basis, transferring verification tasks on the actual assembly code to an adaptation of the BAP binary analysis tool developed at CMU.

Place, publisher, year, edition, pages
2013, 10. 223-234 p.
Keyword [en]
Formal verification, Information Flow Security, Separation Kernel, Hypervisor
National Category
Computer and Information Science
URN: urn:nbn:se:ri:diva-15453DOI: 10.1145/2508859.2516702OAI: diva2:1036770
2013 ACM SIGSAC conference on computer & communications security
Available from: 2016-10-13 Created: 2016-10-13

Open Access in DiVA

fulltext(417 kB)3 downloads
File information
File name FULLTEXT01.pdfFile size 417 kBChecksum SHA-512
Type fulltextMimetype application/pdf

Other links

Publisher's full texthttp

Search in DiVA

By author/editor
Dam, Mads
By organisation
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 3 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Altmetric score

ReferencesLink to record
Permanent link

Direct link