Ottawa Euclid(ID:2324/ott001)Improved Milspec EuclidVerifiable version of Euclid, produced under contract by IP Sharp for the Navy Related languages
References: Introduction In 1976 the Defense Advanced Research Projects Agency (DARPA) commissioned a committee of Computer Scientists to design a Pascal derivative programming language. This new language, to be called Euclid, was to address known deficiencies with Pascal; to include features to support the writing of systems programs; and to be amenable to formal verification. Previous papers [1,2,3,4] have defined the language and discussed its putative benefits. A compiler, which emits code for the PDP-11 series of machines, was implemented jointly by the Computer Systems Research Group, of the University of Toronto, and I.P. Sharp Associates (IPSA) . This compiler recognized a subset of Euclid, called Toronto Euclid [5], and was delivered to DARPA in January 1979. The techniques used by the compiler implementation team and their experiences are related in a number of papers [2,3,4,6]. Unfortunately, the delivery of the Toronto Euclid compiler was too late for what was to have been the first application of Euclid to the development of secure software: KSOS, the Kernelized Secure Operating System. Not until 1981, when IPSA st=rted implementation of the LSI Guard [7], was Euclid applied to the development of security related software. In January 1980, IPSA was funded by the Canadian Department of National Defence (DND) to survey Program Verification (PV) technology. Taking an approach, which was similar to a parallel investigation by the Mitre Corporation [8], we examined, from a "user" perspective, five mechanical systems (Gypsy, Affirm, HDM, Boyer-Moore, and the Stanford Pascal Verifier) . Our experiences are summarized in the final report [91. Briefly, we concluded that the technology was sufficiently advanced that reasonable benefits accrued from using formal specification; we were less receptive toward code proofs because of the weak inference capabilities of current theorem provers. Our combined experiences with Euclid and PV placed us in an ideal position to develop a verification system based upon Euclid. In late 1980 the United States Navy asked us to start this task, with DND adding further support upon our completion of the PV survey. The resulting system is to be called EVES, the Euclid based Verification and Evaluation System. Broadly, the scope of the project consists of the following interrelated tasks: 1. To design a formal specification language. 2. To implement a Euclid compiler for the VAX (and other machines) . 3. To design a logic, within which we can rigorously reason about Euclid programs. 4. To specify formally and implement the LSI Guard. Ultimately, a proof of consistency between the security specification and the implementation will be carried out. 5. To design and implement the EVES environment. The remainder of this paper reports on our progress and briefly outlines some of our technical decisions. Extract: Ottawa Euclid Ottawa Euclid As I mentioned previously, the Euclid committee was to design a Pascal derivative programming language which addressed deficiencies in Pascal, supported the writing of systems programs, and was amenable to PV techniques. Some of the differences between Euclid and Pascal are Euclid?s explicit control of identifier visibility; the prohibition of global variables; type safe variant records; no aliasing; a facility supporting conformant arrays; the introduction of ?module? , to support encapsulation and abstraction; and explicit techniques for accessing the underlying machine. The committee was not asked to develop a verification environment, nor a specification language. These tasks were left to the PV community. Consequently, only rudimentary annotative constructs exist in Euclid. For example, Euclid includes routine pre and post, module invariants, and the assert statement, but, the corresponding Boolean expressions are too weak (e.g. no quantifiers) for stating many necessary specification concepts. The committee envisioned that specification annotations would be treated as "comments" by a Euclid compiler: other tools in the verification environment would process the specifications. We rejected this perspective. After surveying some existing specification languages [101, we concluded that significant advantages would accrue from augmenting Euclid with a specification capability. Firstlyr it meant that only one language had to be understood by those programming and specifying within EVES. Secondly, there is the potential for needing only one, unified, formal semantic description. Thirdly, a compiler could process both code and specifications. Observe that code and specifications will discuss many of the same Euclid units. we are having some success in realizing these advantages. Our dialect of Euclid, called Ottawa Euclid, is described in the reference manual written by David Crowe [11]. I will limit my discussion to two principal additions: the theory and external module constructs. |