Dan Zhou and Paul E. Black, Formal Specification of Operating System Operations, Proc. of IEEE TC-ECBS and IFIP WG10.1 joint workshop on Formal Specifications of Computer Based Systems, pages 69-73, Washington, D.C., (April 2001).

Abstract: This paper describes the development of a formal specification for a secure operating system architecture and its security-related operations in higher-order logic theorem prover, HOL. We specify operating system entries as user defined data types and security conditions as predicates that restrict system operations. We also provide a uniform environment for system commands that change the security state of systems.

Get the paper in DVI (29k), Postscript (70k), or PDF (53k). Expanded version in DVI (45k) or Postscript (92k).

This page's URL is /~black/Papers/formalOS2002.html

Updated Mon Oct 20 12:54:59 2003

Go to Black's papers or NIST home page.