Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
2013 (English)Conference paper (Refereed)
A separation kernel simulates a distributed environment us-ing a single physical machine by executing partitions in iso-lation and appropriately controlling communication amongthem. We present a formal verication of information owsecurity for a simple separation kernel for ARMv7. Previouswork on information ow kernel security leaves communica-tion to be handled by model-external means, and cannot beused to draw conclusions when there is explicit interactionbetween partitions. We propose a dierent approach wherecommunication between partitions is made explicit and theinformation ow is analyzed in the presence of such a chan-nel. Limiting the kernel functionality as much as meaning-fully possible, we accomplish a detailed analysis and veri-cation of the system, proving its correctness at the levelof the ARMv7 assembly. As a sanity check we show howthe security condition is reduced to noninterference in thespecial case where no communication takes place. The ver-ication is done in HOL4 taking the Cambridge model ofARM as basis, transferring verication tasks on the actualassembly code to an adaptation of the BAP binary analysistool developed at CMU.
Place, publisher, year, edition, pages
ACM Press, 2013.
Formal verication; Information Flow Security; Separation Kernel; Hypervisor
IdentifiersURN: urn:nbn:se:kth:diva-136348ScopusID: 2-s2.0-84889040001OAI: oai:DiVA.org:kth-136348DiVA: diva2:675835
2013 ACM SIGSAC Conference on Computer & Communications Security (CCS'13),November 4 - 8, 2013 Berlin, Germany
Qc 201312182013-12-042013-12-042016-09-12Bibliographically approved