Distributed System Security---DARPA Summary
Construction Methodolgies for Improving Distributed System Security
The goal of our project aligns with the overall goal of the DARPA effort---to create a technology that will enable the production of secure software systems for the DoD's and the nation's computing infrastructure. The first technical goal is to build a complex practical system using formal methods tools, specifically using a Logical Environment. To meet this goal we helped build the Ensemble Group Communication System using the ML/Nuprl Logical Environment. Our second technical goal is to collaborate with the system developers to support, modify, deploy and document this system using the Logical Environment, and to demonstrate the contributions of the formal tools to security issues.
We are using advanced formal methods tools on significant applications software. Some of the most critical infrastructure software is found in communications systems. These lie at the base of any information infrastructure---close to the operating systems. Such software is concurrent and fault-tolerant. Its mathematical models are subtle, explaining one difficulty with building secure communications systems. Our approach has been to code Ensemble in the ML/Nuprl programming environment. The programming language ML is a flexible polymorphically typed language whose semantics is formally defined by the Nuprl logic. (Indeed the core of ML is the programming language of the Nuprl programming logic.) Next we chose an important feature of the actual use of Ensemble which presents a challenge for security. This feature is the dynamic reconfiguration of protocol stacks to improve performance. This kind of optimization is known to be a major source of errors in systems of all sorts. We intend to use Nuprl to prove that the reconfigured code is equivalent to the original code.
We have configured the Logical Environment so that it can serve the needs of large systems efforts, specifically those of the Ensemble project. This has meant incorporating the additional programming features such as pattern matching, exception handling and rapid static type checking that were most valuable in the coding process. The creation of this environment is detailed in the paper of Kreitz at our Web site. We have also been able to demonstrate Nuprl automatically proving the equivalence of reconfigured code. We have tested a design for coupling parts of the logical environment to the Ensemble system. See the paper of Hickey at our Web site.
We plan to improve our ability to secure reconfigured code by processing actual examples seen in practice. We also plan to deploy more features of the Logical Environment, such as extended type checking, to improve the precision of the description of Ensemble used to drive equivalence proofs.
The methods we are using for Ensemble generalize to a wide variety of systems. We are especially interested in exploring their use in other finite state based protocols and on code with security specifications. Our work will penetrate into areas where Ensemble is used and carry the security enhancements with it.