Formal methods in the THETA kernel

Author

Seager, Mike ; Guaspari, David ; Stillerman, Matt ; Marceau, Carla

Author_Institution

Odyssey Res. Associates Inc., Ithaca, NY, USA

fYear

1995

fDate

8-10 May 1995

Firstpage

88

Lastpage

100

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Security and Privacy, 1995. Proceedings., 1995 IEEE Symposium on

Conference_Location

Oakland, CA

Print_ISBN

0-8186-7015-0

Type

conf

DOI

10.1109/SECPRI.1995.398925

Filename

398925