Research on Model Checking for SELinux Inter-Process Communication

Ning Wang; Sheng Wen Gong; Huai Xiao  Wang

doi:10.4028/www.scientific.net/AMM.380-384.3826

Paper Titles

Error Correction Based on LDPC Codes in Wireless Optical Communication
p.3811

A New Method of Scalable Image Compression Coding
p.3815

Clustering Research on Fractal Parameter of GIS PD UHF Signals
p.3818

Active Low Pass Filter Design Based on Chaos Theory
p.3822

Research on Model Checking for SELinux Inter-Process Communication
p.3826

Wavelet Denoising-Based Image Feature Extraction by Independent Component Analysis without Pre-Whitening
p.3830

Systems Errors Identification Method of Hull Deformation Data Based on Total Variation Constrained
p.3834

Ear Recognition Based on Point Feature
p.3840

Maximum Average Correlation Height Filter Based on Pulsed Neural Network for Distorted Target Recognition
p.3846

HomeApplied Mechanics and MaterialsApplied Mechanics and Materials Vols. 380-384Research on Model Checking for SELinux...

Research on Model Checking for SELinux Inter-Process Communication

Abstract:

SELinux (Security Enhanced Linux) inherited the basic design of LINUX, and it is a high secure operating system. It is important to know how to make the IPC (Inter-Process Communication) for this kind of multi-task and multi-user system. In this paper, Finite State Automaton is used to verify the security of IPC mechanisms of SELinux. Finally, IPC mechanisms are verified with SPIN model checker.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Applied Mechanics and Materials (Volumes 380-384)

Pages:

3826-3829

DOI:

https://doi.org/10.4028/www.scientific.net/AMM.380-384.3826

Citation:

Cite this paper

Online since:

August 2013

Authors:

Ning Wang, Sheng Wen Gong, Huai Xiao Wang

Keywords:

IPC, Security Enhanced Linux, SPIN Model Checker, System Verification

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] E. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, (1999).

Google Scholar

[2] Immich, P. K., Bhagavatula, R. S., and Pendse, R, Performance analysis of five Inter-process communication mechanisms across UNIX operating systems, J. Syst. Softw. vol. 68, pp.27-43, (2003).

DOI: 10.1016/s0164-1212(02)00134-6

Google Scholar

[3] Stevens, W. Richard, UNIX Network Programming Volume 2: Inter-process Communications, Prentice Hall, (1999).

Google Scholar

[4] Peter Loscocco, NSA, Stephen Smalley, NAI Labs, Integrating Flexible Support for Security Policies into the Linux Operating System, FREENIX Track: 2001 USENIX Annual Technical Conference. June (2001).

Google Scholar

[5] G.J. Holzmann, Design and Validation of Computer Protocols. Englewood Cliffs, Prentice Hall, (1991).

Google Scholar

[6] A. Pnueli, The Temporal Logic of Programs, Proc. 18th IEEE Symp. Foundations of Computer Science, Providence, R. I, 1977, pp.46-57.

Google Scholar