Security Software Verification: (My) Past and Future

We describe two experiences in applying formal methods to software security: formal verification of a secure web server and our on-going work to formally specify (parts of) secure operating systems and automatically generate executable tests from the specification.

The secure web server is about 100 lines of C that ran the arguably most attacked web site on Earth for several years without a single security breach. We describe a Hoare axiomatization of C, formal specification of concepts of security, the formal proof in HOL, and the bugs we found.

We are currently working on formally specifying security properties in HOL and automatically translating these specification into a description suitable for model checking. At the same time, we are specifying the behavior of an add-in, Pitbull, to secure operating systems, including Windows and Solaris. From these specifications, we automatically generate executable tests that complete cover all described behavior.