MAUDE: A Wide-Spectrum Formal Language for Secure Active Networks
Investigators
Objective
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 clt@cs.stanford.edu
13 July 1998.