Separation microkernel security studies and its formal verification related work
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 safe...
Saved in:
| 主要作者: | |
|---|---|
| 其他作者: | |
| 格式: | Final Year Project |
| 語言: | English |
| 出版: |
2016
|
| 主題: | |
| 在線閱讀: | http://hdl.handle.net/10356/66712 |
| 標簽: |
添加標簽
沒有標簽, 成為第一個標記此記錄!
|
| 機構: | Nanyang Technological University |
| 語言: | English |
| 總結: | 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. |
|---|