Title :
Formal methods in the THETA kernel
Author :
Seager, Mike ; Guaspari, David ; Stillerman, Matt ; Marceau, Carla
Author_Institution :
Odyssey Res. Associates Inc., Ithaca, NY, USA
Abstract :
THETA is a secure distributed operating system designed to run on a variety of hardware platforms. We are currently undertaking an effort to formally specify and implement a new THETA kernel to improve its security properties and to increase its portability. We used a number of “formal methods” tools in developing the specification and analyzing its implementation. The report presents an overview of the THETA kernel architecture, then discusses the methods and tools that we used to develop it. We include a critique of the tools and a discussion of the relative merits of using Ada and C to implement complex secure systems
Keywords :
formal specification; network operating systems; object-oriented methods; operating system kernels; security of data; software portability; software tools; Ada; C language; THETA kernel architecture; complex secure systems; formal methods; formal methods tools; formal specification; hardware platforms; portability; secure distributed operating system; security properties; Access control; Distributed computing; Distributed databases; Hardware; Kernel; Object oriented databases; Operating systems; Protection; Prototypes; Security;
Conference_Titel :
Security and Privacy, 1995. Proceedings., 1995 IEEE Symposium on
Conference_Location :
Oakland, CA
Print_ISBN :
0-8186-7015-0
DOI :
10.1109/SECPRI.1995.398925
