Writing an OS Kernel in a Strictly and Statically Typed Language | SpringerLink
Skip to main content
Springer Nature Link
Log in

Writing an OS Kernel in a Strictly and Statically Typed Language

  • Chapter
Formal to Practical Security

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 5458))

Abstract

OS kernels have been written in weakly typed or non typed programming languages, for example, C. Therefore, it is extremely hard to verify even simple memory safety of the kernels. The difficulty could be resolved by writing OS kernels in strictly typed programming languages, but existing strictly typed languages are not flexible enough to implement important OS facilities (e.g., memory management and multi-thread management facilities). To address the problem, we designed and implemented TALK, a new strictly and statically typed assembly language which is flexible enough to implement OS facilities, and wrote an OS kernel with TALK. In our approach, the safety of the kernel can be verified automatically through static type checking at the level of binary executables without source code.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)

    MATH  Google Scholar 

  2. ECMA: ECMA-334: C# Language Specification (2002)

    Google Scholar 

  3. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)

    Article  Google Scholar 

  4. Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors. ACM Trans. Comput. Syst. 24(4), 393–423 (2006)

    Article  Google Scholar 

  5. Bevier, W.R.: Kit: A study in operating system verification. IEEE Trans. Softw. Eng. 15(11), 1382–1396 (1989)

    Article  Google Scholar 

  6. Betarte, G., Cornes, C., Szasz, N., Tasistro, A.: Specification of a smart card operating system. In: Coquand, T., Nordström, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol. 1956, pp. 77–93. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  7. Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3), 527–568 (1999)

    Article  MATH  Google Scholar 

  8. Smith, F., Walker, D., Morrisett, J.G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 366–381. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  9. Maeda, T., Yonezawa, A.: Writing practical memory management code with a strictly typed assembly language. In: SPACE 2006: Workshop on Semantics, Program Analysis, and Computing Environments For Memory Management, pp. 35–46 (2006)

    Google Scholar 

  10. Maeda, T.: Writing an Operating System with a Strictly Typed Assembly Language. Ph.D thesis, University of Tokyo (2006)

    Google Scholar 

  11. Kosakai, T., Maeda, T., Yonezawa, A.: Compiling C programs into a strongly typed assembly language. In: Cervesato, I. (ed.) ASIAN 2007. LNCS, vol. 4846, pp. 17–32. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  12. Intel Corporation: Intel 64 and IA-32 Architectures Software Developer’s Manual

    Google Scholar 

  13. Maeda, T.: TALK project, http://www.yl.is.s.u-tokyo.ac.jp/~tosh/talk/

  14. Accetta, M.J., Baron, R.V., Bolosky, W.J., Golub, D.B., Rashid, R.F., Tevanian, A., Young, M.: Mach: A new kernel foundation for UNIX development. In: USENIX, pp. 93–113 (Summer 1986)

    Google Scholar 

  15. Engler, D.R., Kaashoek, M.F., O’Toole Jr., J.: Exokernel: an operating system architecture for application-level resource management. In: SOSP 1995: Proceedings of the fifteenth ACM symposium on Operating systems principles, pp. 251–266. ACM, New York (1995)

    Chapter  Google Scholar 

  16. Liedtke, J.: On μ-kernel construction. SIGOPS Oper. Syst. Rev. 29(5), 237–250 (1995)

    Article  Google Scholar 

  17. Witchel, E., Cates, J., Asanović, K.: Mondrian memory protection. SIGARCH Comput. Archit. News 30(5), 304–316 (2002)

    Article  Google Scholar 

  18. Igarashi, A., Kobayashi, N.: Resource usage analysis. In: POPL 2002: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 331–342. ACM, New York (2002)

    Google Scholar 

  19. Zhu, M.Y., Luo, L., Xiong, G.Z.: A provably correct operating system: δ-core. SIGOPS Oper. Syst. Rev. 35(1), 17–33 (2001)

    Article  Google Scholar 

  20. Tuch, H., Klein, G., Heiser, G.: OS verification — now! In: HOTOS 2005: Proceedings of the 10th Workshop on Hot Topics in Operating Systems, Berkeley, CA, USA, pp. 7–12. USENIX Association (2005)

    Google Scholar 

  21. McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3(4), 184–195 (1960)

    Article  MATH  Google Scholar 

  22. Bershad, B.N., Savage, S., Pardyak, P., Sirer, E.G., Fiuczynski, M.E., Becker, D., Chambers, C., Eggers, S.: Extensibility safety and performance in the SPIN operating system. In: SOSP 1995: Proceedings of the fifteenth ACM symposium on Operating systems principles, pp. 267–283. ACM, New York (1995)

    Chapter  Google Scholar 

  23. Nelson, G. (ed.): System Programming in Modula-3. Prentice Hall, Englewood Cliffs (1991)

    Google Scholar 

  24. Hunt, G., Larus, J.R., Abadi, M., Aiken, M., Barham, P., Fähndrich, M., Hawblitzel, C., Hodson, O., Levi, S., Murphy, N., Steensgaard, B., Tarditi, D., Wobber, T., Zill, B.D.: An overview of the Singularity project. Technical Report MSR-TR-2005-135, Microsoft Research (2005)

    Google Scholar 

  25. Hunt, G.C., Larus, J.R.: Singularity: rethinking the software stack. SIGOPS Oper. Syst. Rev. 41(2), 37–49 (2007)

    Article  Google Scholar 

  26. Jim, T., Morrisett, J.G., Grossman, D., Hicks, M.W., Cheney, J., Wang, Y.: Cyclone: A safe dialect of C. In: ATEC 2002: Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, Berkeley, CA, USA, pp. 275–288. USENIX Association (2002)

    Google Scholar 

  27. Smith, G., Volpano, D.: A sound polymorphic type system for a dialect of C. Sci. Comput. Program. 32(1-3), 49–72 (1998)

    Article  MATH  Google Scholar 

  28. Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst. 27(3), 477–526 (2005)

    Article  Google Scholar 

  29. Criswell, J., Lenharth, A., Dhurjati, D., Adve, V.: Secure virtual architecture: a safe execution environment for commodity operating systems. SIGOPS Oper. Syst. Rev. 41(6), 351–366 (2007)

    Article  Google Scholar 

  30. Dhurjati, D., Kowshik, S., Adve, V.: Enforcing Alias Analysis for Weakly Typed Languages. Technical Report #UIUCDCS-R-2005-2657, Computer Science Dept., Univ. of Illinois (November 2005)

    Google Scholar 

  31. Dhurjati, D., Kowshik, S., Adve, V., Lattner, C.: Memory safety without garbage collection for embedded applications. Trans. on Embedded Computing Sys. 4(1), 73–111 (2005)

    Article  Google Scholar 

  32. Dhurjati, D., Kowshik, S., Adve, V.: SAFECode: enforcing alias analysis for weakly typed languages. SIGPLAN Not. 41(6), 144–157 (2006)

    Article  Google Scholar 

  33. Turner, D.N., Wadler, P., Mossin, C.: Once upon a type. In: FPCA 1995: Proceedings of the seventh international conference on Functional programming languages and computer architecture, pp. 1–11. ACM, New York (1995)

    Chapter  Google Scholar 

  34. Cheney, J., Morrisett, G.: A linearly typed assembly language. Technical report, Department of Computer Science, Cornell University (2003)

    Google Scholar 

  35. Aspinall, D., Compagnoni, A.: Heap-bounded assembly language. J. Autom. Reason. 31(3-4), 261–302 (2003)

    Article  MATH  Google Scholar 

  36. Hawblitzel, C., Wei, E., Huang, H., Krupski, E., Wittie, L.: Low-level linear memory management. In: SPACE 2004: Workshop on Semantics, Program Analysis, and Computing Environments For Memory Management. (2004)

    Google Scholar 

  37. Maeda, T.: TOS project, http://www.yl.is.s.u-tokyo.ac.jp/~tosh/tos/

  38. Maeda, T., Yonezawa, A.: Typed assembly language with interrupts (in Japanese). In: JSSST Dependable System Workshop 2007, pp. 107–110 (2007)

    Google Scholar 

  39. Maeda, T., Yonezawa, A.: Typed assembly language for SMP (in Japanese). In: JSSST Dependable System Workshop 2008, pp. 115–126 (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Graduate School of Information Science and Technology, The University of Tokyo, Japan

    Toshiyuki Maeda & Akinori Yonezawa

Authors
  1. Toshiyuki Maeda
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Akinori Yonezawa
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LORIA, Équipe Cassis, Bât. A, Campus Scientifique, BP 239, 54506, Vandoeuvre-lès-Nancy Cedex, France

    Véronique Cortier

  2. Centre de Recherche, INRIA Bordeaux – Sud-Ouest, Bât. A29, 351 Cours de la Libération, 33405, Talence, France

    Claude Kirchner

  3. Department of Philosophy, Keio University, 2-15-45 Mita, Minato-ku, 108-8345, Tokyo, Japan

    Mitsuhiro Okada

  4. 3-1 Morinosato Wakamiya Atsugi-shi, 243-0198, Kanagawa, Japan

    Hideki Sakurada

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Maeda, T., Yonezawa, A. (2009). Writing an OS Kernel in a Strictly and Statically Typed Language. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds) Formal to Practical Security. Lecture Notes in Computer Science, vol 5458. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02002-5_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02002-5_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02001-8

  • Online ISBN: 978-3-642-02002-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics