MAUDE: A Wide-Spectrum Formal Language for Secure Active Networks



The active networks architecture poses hard technical challenges. For purposes of specifying and architecting active networks, a formal language capturing the desired semantics seems highly desirable. If such specifications are executable, it will be possible to simulate the designs at very early stages. The formal language should support important features such as openness, distribution, object-orientation, mobility, and reflexive dynamic adaptation. However, there may still be a big gap between specifications and actual code, weakening the degree of assurance that can be obtained at the system level. Such a gap can be greatly reduced by a wide-spectrum formal approach in which specifications can be refined in a provably correct way into declarative mobile code. High assurance is indeed crucial, because of the vital security properties that must be ensured for active networks. A wide-spectrum formal framework can also offer a good mathematical basis on which to develop the new security models and proof techniques that will be needed for secure active networks. Our research over the last six years has developed a new, wide-spectrum formal language called Maude that is very well suited for solving the above challenges. Our goal is to provide the active networks architecture with a formal language technology that will be an ideal match for its design and specification needs, will allow formal transformation of those specifications into mobile code and will support formal verification of security properties.

Relevant Items

Relevant Papers

Other Projects

Last updated by Carolyn Talcott 13 July 1998.