2009 | OriginalPaper | Buchkapitel
Writing an OS Kernel in a Strictly and Statically Typed Language
verfasst von : Toshiyuki Maeda, Akinori Yonezawa
Erschienen in: Formal to Practical Security
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.