Abstract
Traditional operating systems protect themselves from user programs with a privilege level facility of CPUs. One problem of the protection-by-hardware approach is that system calls become very slow because heavy operations are required to safely switch the privilege levels of user programs. To solve the problem, we design an operating system that protects itself with a type theory. In our approach, user programs are written in a typed assembly language and the kernel performs type-checking before executing the programs. Then, the user programs can be executed in the kernel mode, because the kernel knows that the type-checked programs do not violate safety of the kernel. Thus, system calls become mere function calls and can be invoked very quickly. We implemented Kernel Mode Linux (KML) that realizes our approach. Several benchmarks show effectiveness of KML.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Appel, A.W.: Foundational proof-carrying code. In: Proc. of 16th Annual IEEE Symposium on Logic in Computer Science, pp. 247–258 (June 2001)
Bershad, B.N., Chambers, C., Eggers, S.J., Maeda, C., McNamee, D., Pardyak, P., Savage, S., Sirer, E.G.: SPIN - an extensible microkernel for application-specific operating system services. In: Proc. of ACM SIGOPS European Workshop, September 1994, pp. 68–71 (1994)
Crary, K.: Toward a foundational typed assembly language. In: Proc. of Symposium on Principles of Programming Languages, January 2003, pp. 198–212 (2003)
Dubnicki, C., Bilas, A., Chen, Y., Damianakis, S., Li, K.: VMMC-2: efficient support for reliable, connection-oriented communication. In: Proc. of Hot Interconnects, August 1997, pp. 37–46 (1997)
Hamid, N., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code. Technical Report YALEU/DCS/TR-1224, Dept. of Computer Science, Yale University (2002)
Harbison, S.P.: Modula-3. Prentice-Hall, Englewood Cliffs (1992)
Intel Corporation. IA-32 Intel Architecture Software Developer’s Manual
The Linux kernel, http://www.kernel.org
McVoy, L.W., Staelin, C.: lmbench: Portable tools for performance analysis. In: Proc. of USENIX Annual Technical Conference, pp. 279–294 (1996)
Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., Zdancewic, S.: TALx86: A realistic typed assembly language. In: Proc. of ACM SIGPLAN Workshop on Compiler Support for System Software, pp. 25–35 (1999)
Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. In: Proc. of Types in Compilation, pp. 28–52 (1998)
Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Transactions on Programming Languages and Systems 21(3), 527–568 (1999)
Norcott, W.D.: The IOzone file system benchmark, http://www.iozone.org
Prylli, L., Tourancheau, B.: BIP: a new protocol designed for high performance networking on Myrinet (March 1998)
Tezuka, H., Hori, A., Ishikawa, Y.: PM: a high-performance communication library for multi-user parallel environments. Technical Report TR-96015, Real World Computing Partnership (1996)
Wahbe, R., Lucco, S., Anderson, T.E., Graham, S.L.: Efficient software-based fault isolation. ACM SIGOPS Operating Systems Review 27(5), 203–216 (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Maeda, T., Yonezawa, A. (2003). Kernel Mode Linux: Toward an Operating System Protected by a Type Theory. In: Saraswat, V.A. (eds) Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation. ASIAN 2003. Lecture Notes in Computer Science, vol 2896. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40965-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-40965-6_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20632-3
Online ISBN: 978-3-540-40965-6
eBook Packages: Springer Book Archive