Please use this identifier to cite or link to this item:
Title: Separation microkernel security studies and its formal verification related work
Authors: Lu, Shengliang
Keywords: DRNTU::Engineering
Issue Date: 2016
Abstract: A separation kernel provides temporal and spatial separation among applications or partitions. This type of kernels ensure that there are no unwanted channels for information flows between partitions. XtratuM, an open source separation microkernel, is implemented based on ARINC 653 standard for safety-critical system. In order to guarantee that it is free of bugs and is following security policies, completely formal verification on XtratuM is conducted by Securify team. During reasoning about information flow described in ARINC 653, some covert channels are found by Securify Team. In this paper, a successful demonstration on the existence of covert channel in XtratuM is provided, followed by improvement suggestions on fixing the covert channel. With the objective of modeling and hence formally verifying XtratuM, in-depth analysis of its source code and verification related work are discussed in this report.
Rights: Nanyang Technological University
Fulltext Permission: restricted
Fulltext Availability: With Fulltext
Appears in Collections:SCSE Student Reports (FYP/IA/PA/PI)

Files in This Item:
File Description SizeFormat 
  Restricted Access
2.18 MBAdobe PDFView/Open

Page view(s)

Updated on Jun 23, 2021


Updated on Jun 23, 2021

Google ScholarTM


Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.