Formal Methods for Industrial Critical Systems
In theory, formal methods give us the ability to determine whether properties we ascribe to specifications or software systems hold for certain. However, the assurance that can be obtained from formal methods comes at a price. In the eighties, the computer networks community invested heavily in tools, theories, and case studies. They used formal methods to provide a rigorous and unambiguous way of designing and documenting protocols, to allow formal analysis (verification/performance analysis) before protocols are implemented, and to allow automatic code generation from the formal specification. The seminal work on Communicating Finite State Machines was followed by approaches based on process algebra and temporal logic, to give an example.
In the past decade, however, attention shifted to computer security as an application area where the expense of faulty software would make the application of formal methods cost-effective. But security properties such as confidentiality and authenticity are often difficult to characterize formally (or even informally). In our presentation, we review ways in which the above communities describe their domain-specific properties, how mechanisms are captured, and how protocols are analyzed. We conclude that despite the different objectives, even "traditional" methods can be applied successfully in the field of computer security. For example, we describe our work on giving an operational semantics to the JavaCard Virtual Machine and using a well-known model checker for analysis.
Note: The content of the following files is part of GMD Report No. 91 and subject to its copyright.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch