Conference Report: COMPASS ’93, EIGHTH ANNUAL CONFERENCE ON COMPUTER ASSURANCE Gaithersburg, MD June 14-17, 1993

Abstract

Title: Conference Report: COMPASS ’93, EIGHTH ANNUAL CONFERENCE ON COMPUTER ASSURANCE Gaithersburg, MD June 14-17, 1993 Authors: ['Dolores R. Wallace' 'Elizabeth B. Lennon'] ## 1. Introduction Cosponsored by the IEEE Aerospace and Electronics Systems Society and the IEEE National Capital Area Council, in cooperation with the British Computer Society, COMPASS is an organization which advances the theory and practice of building computer assurance into critical systems. NIST’s Computer Systems Laboratory hosted the Eighth Annual Conference on Computer Assurance (COMPASS ’93) on June 14-17, 1993, and served as cosponsors with the following industry and government organizations: Area Systems, Inc.; ARINC Research Corporation; Control Systems Analysis, Inc.; CTA, Inc.; IBM; Logicon, Inc.; Naval Research Laboratory; Naval Surface Warfare Center; Systems Safety Society; TRW Systems Division; and the U.S. General Accounting Office. COMPASS ’93 attracted more than 130 participants from government, industry, academia, and foreign countries such as the United Kingdom, Italy, and Taiwan. This year’s theme, “Practical Paths to Assurance,” highlighted the need to use a pragmatic and realistic approach when providing assurance in a computer system. ## 2. Tutorials COMPASS ’93 featured tutorials for conference participants who wanted an in-depth discussion of two relevant topics. John Rushby and Patrick Lincoln, SRI International, provided an introduction to formal methods with special focus on the use of automated support tools such as PVS, a Prototype “next generation” Verification System that attempts to provide the benefits of powerful and effective automation for an expressive specification language. Worked examples were demonstrated “live” and included examples from hardware design, fault tolerance, and real-time systems. Janet Cugini, NIST, gave a second tutorial on the draft Federal Criteria for Information Technology Security which covered background, protection profiles. Trusted Computing Base (TCB) functional components, development assurance requirements, evaluation assurance requirements, and future work. The first full day of the conference opened with welcoming remarks by James Burrows, CSL Director; Judith Bramlage, COMPASS ’93 General Chair; and John Marciniak, COMPASS ’93 Program Chair. ## 3. Myths of Dependable Computing Peter Neumann, SRI International, keynoted the first day of the conference with a talk entitled “Myths of Dependable Computing: Shooting the Straw Herrings in Midstream.” Citing the belief that most users are doing what they can to assure dependable computing, Neumann identified five problem areas: unsecured PCs; distributed systems which do not back up well; standards and criteria which are useful but inadequate; the lack of use of software engineering and fault tolerance; and the fact that the state-of-the-art in software engineering is not being used in critical systems. Stating that myths tend to be true in the small view, false in the larger picture, he discussed the reliability, security, and safety of software systems, and proposed solutions through research, development, and education. Neumann challenged organizations to do it right in the first place, to make hard decisions, and to look at assurance in the context of the larger picture. ## 4. Verification Technology Moderated by Connie Heitmeyer, Naval Research Laboratory, this session featured three papers. Sidney Bailin and Scott Henderson, CTA Incorporated, presented a talk on “A Tool for Reasoning About Software Models” which described the Formal Interconnection Analysis Tool (FIAT). Supporting formal reasoning about software systems via their specification diagrams, FIAT decomposes the specification into a diagram of interconnected lower-level components and uses this information to establish some automated verification results. Chung-Ming Huang, National Cheng Kung University, Tainan, Taiwan, described a protocol verification method which could use ESTELLE and SDL verification tools to assure the correctness of communication protocols. Current verification protocol techniques utilize a global state reduction technique to allow the use of ESTELLE and SDL; the new technique reduces global states to a single state for live variables having the same value, making the incremental protocol model applicable in the ESTELLE and SDL verification tools. The third presenter was Farn Wang of the University of Texas. Building off the successful use of propositional temporal logic in the verification of digital circuits, Wang and co-author Aloysius K. Mok proposed a technique called Asynchronous Register Temporal Logic (ARTL) to address the verification of distributed real-time software systems. ARTL uses a multi-clock model, utilizes reasoning about items which have more than binary values normally found in digital circuits, and uses a freezing modal operator for fixing register contents. Results are promising for using the verifier for larger benchmarks.