Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
2013
Online
unknown
Zugriff:
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.
Titel: |
Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
|
---|---|
Autor/in / Beteiligte Person: | Dam, Mads ; Guanciale, Roberto ; Khakpour, Narges ; Nemati, Hamed ; Schwarz, Oliver |
Link: | |
Veröffentlichung: | 2013 |
Medientyp: | unknown |
DOI: | 10.1145/2508859.2516702 |
Schlagwort: |
|
Sonstiges: |
|