Tempering network stacks

This paper summarizes existing and describes ongoing work on security policy definition and particularly enforcement in heterogeneous distributed systems. Based on a formal model of operating systems and interactions among networked nodes in a distributed system axiomatizing relations among and abstractions in distributed systems, arbitrary security policies can be defined over the same model; automated reasoning techniques can be used to dynamically derive the compliance of operations with all applicable security policies. A key component for enforcing such security policies in operating system network stacks is described along with instrumentation techniques for the Microsoft Windows NT family of operating systems.