1997

Archer, Myla M. and Heitmeyer, Constance L. "Human-Style Theorem Proving Using PVS," TPHOLs '97, Murray Hill, NJ, August 19-22, 1997. PostScript, PDF

A major barrier to more common use of mechanical theorem provers in verifying software designs is the significant distance between proof styles natural to humans and proof styles supported by mechanical provers. To make mechanical provers useful to software designers with some mathematical sophistication but without expertise in mechanical provers, the distance between hand proofs and their mechanized versions must be reduced. To achieve this, we are developing a mechanical prover called TAME on top of PVS. TAME is designed to process proof steps that resemble in style and size the typical steps in hand proofs. TAME's support of more natural proof steps should not only facilitate mechanized checking of hand proofs, but in addition should provide assurance that theorems proved mechanically are true for the reasons expected and also provide a basis for conceptual level feedback when a mechanized proof fails. While infeasible for all applications, designing a prover that can process a set of high-level, natural proof steps for restricted domains should be achievable. In developing TAME, we have had moderate success in defining specialized proof strategies to validate hand proofs of properties of Lynch-Vaandrager timed automata. This paper reports on our successes, the services provided by PVS that support these successes, and some desired enhancements to PVS that would permit us to improve and extend TAME.

Archer, Myla M. and Heitmeyer, Constance L. "Verifying Hybrid Systems Modeled as Timed Automata: A Case Study," Proceedings of HART '97, Grenoble, France, March 26-28, 1997. PostScript, PDF

Verifying properties of hybrid systems can be highly complex. To reduce the effort required to produce a correct proof, the use of mechanical verification techniques is promising. Recently, we extended a mechanical verification system, originally developed to reason about deterministic real-time automata, to verify properties of hybrid systems. To evaluate our approach, we applied our extended proof system to a solution, based on the Lynch-Vaandrager timed automata model, of the Steam Boiler Controller problem, a hybrid systems benchmark. This paper reviews our mechanical verification system, which builds on SRI's Prototype Verification System (PVS), and describes the features we added to handle hybrid systems. It also discusses some errors we detected in applying our system to the benchmark problem. We conclude with a summary of insights we acquired in using our system to specify and verify hybrid systems.

Bharadwaj, Ramesh and Heitmeyer, Constance L. "Verifying SCR Requirements Specifications using State Exploration," Proceedings of First ACM SIGPLAN Workshop on Automatic Analysis of Software, Paris, France, January 14, 1997. PostScript, PDF

Researchers at the Naval Research Laboratory (NRL) have been developing a formal method, known as the SCR (Software Cost Reduction) method, to specify the requirements of software systems using tables. NRL has developed a formal state machine model defining the SCR semantics and support tools for analysis and validation. Recently, a verification capability was added to the SCR toolset. Users can now invoke the Spin model checker within the toolset to establish properties of a specification. This paper describes the results of our initial experiments to verify properties of SCR requirements specifications using Spin. After reviewing the SCR requirements method and introducing our formal requirements model, we describe how SCR specifications can be translated into an imperative programming notation. We also describe how we limit state explosion by verifying abstractions of the original requirements specification. These abstractions are derived using the formula to be verified and special attributes of SCR specifications. The paper concludes with the results of our experiments with Spin and a discussion of ongoing and future work.

Bharadwaj, Ramesh and Heitmeyer, Constance L. "Applying the SCR Requirements Method to a Simple Autopilot, " To be presented at the Fourth NASA Langley Formal Methods Workshop, Hampton, VA, September 10-12, 1997. PostScript [Warning: 4 MB!], PDF

Although formal methods for developing computer systems have been available for more than a decade, few have had significant impact in practice. A major barrier to their use is that developers find formal methods difficult to understand and apply. One exception is a formal method called SCR for specifying computer system requirements which, due to its easy-to-use tabular notation and demonstrated scalability, has achieved some success in industry.

To demonstrate and evaluate the SCR method and tools, we recently used SCR to specify the requirements of a simplified mode control panel for the Boeing 737 autopilot. This paper presents the SCR requirements specification of the autopilot, outlines the process we used to create the SCR specification from a prose description, and discusses the problems and questions that arose in developing the specification. Formalizing and analyzing the requirements specification in SCR uncovered a number of problems with the original prose description, such as incorrect assumptions about the environment, incompleteness, and inconsistency. The paper also introduces a new tabular format we found useful in understanding and analyzing the required behavior of the autopilot. Finally, the paper compares the SCR approach to requirements with that of Rickey Butler of NASA Langley Research Center, who uses the PVS language and prover of SRI International to represent and analyze the autopilot requirements.

Bharadwaj, Ramesh and Constance L. Heitmeyer. "Model Checking Complete Requirements Specifications Using Abstraction," NRL Memorandum Report NRL/MR/5540--97-7999, November 10, 1997. PostScript, PDF

Although model checking has proven remarkably effective in detecting errors in hardware designs, its success in the analysis of software specifications has been quite limited. Model checking algorithms for hardware verification commonly use Binary Decision Diagrams (BDDs), a highly effective technique for analyzing specifications with the scores of Boolean variables commonly found in hardware descriptions. Unfortunately, BDDs are relatively ineffective for analyzing software specifications, which usually contain not only Booleans but variables spanning a wide range of data types. Further, software specifications have huge, often infinite, state spaces that cannot be model checked directly using conventional symbolic methods. One promising, but largely unexplored technique for limiting the size of the state space to be analyzed by model checking is to extract a model with a smaller state space from a complete specification using sound abstraction methods. Users of model checkers routinely analyze reduced models, but most often generate the models in ad hoc ways. As a result, the reduced models are often incorrect.

This report first describes how one can model check a complete requirements specification expressed in the SCR (Software Cost Reduction) tabular notation. Unlike previous approaches, which apply model checking to mode transition tables with Boolean variables, we use model checking to analyze properties of complete SCR specifications with variables ranging over many data types. The report also describes two sound and complete methods for producing abstractions from requirements specifications. These abstractions are derived from the specification based on the property to be analyzed. Finally, the report describes how SCR requirements specifications can be translated into the languages of Spin, an explicit state model checker, and SMV, a symbolic model checker, and presents the results of model checking two sample SCR specifications using our abstraction methods and the two model checkers.

Froscher, J. and Myong Kang, "A Client-Server Architecture Supporting MLS Interoperability with COTS Components," Proc. MILCOM 97, Monterey, CA, Nov. 1997. PostScript, PDF

A major challenge facing the MLS community is to find ways to provide the information and connectivity that DoD users demand without either imposing unacceptable security risks or requiring expensive hardware and software that fails to mesh with commercial off-the-shelf (COTS) applications. This paper proposes, very briefly, an architecture that meets these goals using only a small number of relatively simple, low cost, high assurance components in combination with a preponderance of unmodified COTS hardware, operating systems and applications.

Goldschlag, David M., Michael G. Reed, and Paul F. Syverson, "Internet Communication Resistant to Traffic Analysis," 1997 NRL Review, Washington, DC, April 1997, pp. 109-111.

Determining who is talking to whom (called traffic analysis) is an important source of intelligence information. As military grade communication devices increasingly depend on the public communications infrastructure, it is important to use that infrastructure in ways that are resistant to traffic analysis. It may also be useful to communicate anonymously, for example when gathering intelligence from public databases. We describe bidirectional and real-time Anonymous Connections that are strongly resistant to eavesdropping and traffic analysis attacks by both insiders and outsiders. If necessary, communication is made anonymous by removing identifying information from the data stream. These anonymous connections have been prototyped in a system that protects the privacy of communication over the Internet and, in particular, the World Wide Web. Anonymous connections can protect both identity and location in many switched communication systems, such as wired, cellular, or satellite phone networks.

Goldschlag, David M., Michael G. Reed, and Paul F. Syverson, "Privacy on the Internet," INET '97, Kuala Lumpur, Malaysia, June 1997. HTML

The World Wide Web is rapidly becoming an important tool for modern day communication and commerce. But electronic messages sent over the Internet can be easily snooped and tracked revealing who is talking to whom and what they are talking about. Is privacy important and how can it be guaranteed? This paper describes how a freely available system, onion routing, can be used to provide privacy for a wide variety of Internet services, including Virtual Private Networks, Web browsing, e-mail, remote login, and electronic cash.

Heitmeyer, Constance L., James Kirby, and Bruce Labaw. "Tools for Formal Specification, Verification, and Validation of Requirements," Proceedings of 12th Annual Conference on Computer Assurance (COMPASS '97), June 16-19, 1997, Gaithersburg, MD. (Accepted for presentation) PostScript [Warning: 20 MB!], PDF

Although formal methods for developing computer systems have been available for more than a decade, few have had significant impact in practice. A major barrier to their use is that software developers find formal methods difficult to understand and apply. One exception is a formal method called SCR for specifying computer system requirements which, due to its easy to use tabular notation and its demonstrated scalability, has already achieved some success in industry. Recently, a set of software tools, including a specification editor, a consistency checker, a simulator, and a verifier, has been developed to support the SCR method [9, 11, 5]. This paper describes recent enhancements to the SCR tools: a new dependency graph browser which displays the dependencies among the variables in the specification, an improved consistency checker which produces detailed feedback about detected errors, and an assertion checker which checks application properties during simulation. To illustrate the tool enchancements, a simple automobile cruise control system is presented and analyzed.

Kang, Myong H., Andrew P. Moore, and Ira S. Moskowitz. "Design and Assurance Strategy for the NRL Pump," Proc. IEEE High-Assuruance Systems Engineering Workshop (HASE97) MS Word Doc

Developing a trustworthy system is difficult because the developer must construct a persuasive argument that the system conforms to its critical requirements. This assurance argument, as well as the software and hardware, must be evaluated by an independent certification team. In this paper, we present the external requirements and logical design of a specific trusted device, the NRL Pump, and describe our plan, called the assurance strategy, to create the eventual assurance argument. Our assurance strategy exploits currently available graphical specification, simulation, formal proof, and testing coverage analysis tools. Portions of the design are represented by figures generated by the Statemate toolset, and we discuss how those tools, and covert channel analysis, will be used to show that the logical design conforms to its external requirements. We conclude with some remarks on a possible physical architecture.

Kang, Myong H., Judith N. Froscher, and Ira S. Moskowitz, "An Architecture for Multilevel Secure Interoperability," 13th Annual Computer Security Applications Conference, IEEE Computer Society, SanDiego, CA, 1997 PostScript, PDF

As computer systems become distributed and heterogeneous, there is strong movement in the commercial sector to ease the problems of interoperability and security. Many standards have been proposed for these problems. However, the commercial sector has not shown strong interest in providing cost-effective high-assurance multilevel security (MLS) solutions to the relatively small communities (e.g., intelligence, military) that require them. In this paper, we introduce a practical, cost-effective, and high-assurance secure solution for multilevel distributed and heterogeneous environments using COTS components. The solution is based on an MLS architecture that consists of commercial single-level hardware and software, and a few specialized security devices. We show how an MLS CORBA can be constructed from single-level CORBAs and two security devices; the NRL Pump and the Starlight Interactive Link. We also introduce the concept of MLS cooperative computing which is a way to semi-automate distributed computing among organizations at different security levels.

Landwehr, C. E. et. al. Safe Use of the Internet for Defence Purposes. TTCP STP-11 report, May, 1997. (Editor and author, with contributions from other STP-11 members) PostScript, PDF

This report, developed by the members of TTCP STP-11 in the spring of 1997, documents why Defence establishments of the TTCP member nations are increasing their use of the Internet and suggests guidelines for using the Internet safely and prudently for Defence purposes. It describes Internet architecture and vulnerabilities, current and emerging technologies that can be used to reduce the risks, and possible demonstrations of existing and emerging technologies.

Landwehr, C.E. "Protecting Unattended Computers Without Software," in Proc. Thirteenth Annual Computer Security Applications Conf., San Diego, CA, Dec., 1997, pp.274-283. PostScript, PDF

In many environments, users login to workstations and then leave them unattended. Rather than trying to stop users from doing what comes naturally, this paper suggests a simple, hardware-based system that can protect computers in such an environment from unauthorized use by those with physical access to the monitor and keyboard. Requirements for the system are described, some design issues are discussed, and a sketch of a design for an initial prototype is provided, together with an assurance argument for it. A prototype implementing many of the concepts described has been built; two dozen copies of a second prototype are soon to be installed in an office environment.

Landwehr, C.E. and David M. Goldschlag, "Security Issues in Networks with Internet Access." Invited paper, Proc IEEE Vol 85, No. 12, Dec. 1997, pp.2034-2051. PostScript, PDF

This paper describes the basic principles of designing and administering a relatively secure network. The principles are illustrated by describing the security issues a hypothetical company faces as the networks that support its operations evolve from strictly private, through a mix of Internet and private nets, to a final state in which the Internet is fully integrated into its operations, and the company participates in international electronic commerce. At each stage, the vulnerabilities and threats that the company faces, the countermeasures that it considers, and the residual risk the company accepts are noted. Network security policy and services are discussed, and a description of Internet architecture and vulnerabilities provides additional technical detail underlying the scenario. Finally, a number of building blocks for secure networks are presented that can mitigate some of the vulnerabilities. Keywords: computer network security, internet, cryptography, authentication

McDermott, J. "Replication does survive information warfare attacks," In Proc. of the 11th Annual Working Conference on Database Security, Lake Tahoe, CA, August 1997, pp. 186-198. PostScript, PDF

Recent literature on information warfare has suggested that general replication is not useful in dealing with storage spoofing attacks. We show that special cases of replication are useful not only in detecting but also in recovering from storage spoofing attacks.

McDermott, J. and Froscher, J. "Practical Defenses Against Storage Jamming," in Proceedings of the 20th National Information Systems Security Conference, Baltimore, MD, October 1997, pp. 162-173. PostScript, PDF

Storage jamming is surreptitious tampering with stored data. The tampering can be done from within the application that manages the authentic storage, or it can be done from outside the application. Conventional security approaches such as access control, encryption, audit, and virus detection do not prevent storage jamming attacks. Attacks can be detected in real systems by replay or by replication.

McDermott, J., R. Gelinas, S. Orenstein. "Doc, Wyatt, and Virgil: Prototyping storage jamming defenses," Proceedings of the 13th Annual Computer Security Applications Conference, San Diego, CA, December 1997, pp. 265-273. PostScript, PDF

This paper describes progress to date on three prototype tools for detecting storage jamming attacks. One prototype uses a replay defense; another uses logical replication, and the third can be used to determine the source and pattern of a detected attack. Three prototype jammers are used to test the effectiveness of the defenses. Initial experiments have shown that access control, encryption, audit, and virus detection do not prevent or detect storage jamming. The prototype tools have been effective in detecting the same attacks. Object-oriented data storage may require the use of application-specific techniques for applying checksums.

Moore, Andrew P. "The JMCIS Information Flow Improvement (JIFI) Assurance Strategy," NRL Memo Report 5542-97-7951. PostScript, PDF, HTML

The Joint Maritime Command Information System (JMCIS) provides a common operating environment for Naval tactical decision aids that currently operates two distinct system high enclaves, one at SECRET/GENSER and one at TOP SECRET/SCI. NRL Code 5540 is developing an extension of JMCIS, called JIFI (JMCIS Information Flow Improvement), to improve the timeliness and accuracy of GENSER information available to SCI JMCIS analysts while maintaining the security posture of the system. This document describes the strategy for developing the evidence that JIFI satisfies its critical security requirements. The strategy views databases in more classified enclaves as potential replica sites for data from less classified enclaves. Replicated data flows from lower enclaves to higher ones via simple one-way connections, yielding a high assurance MLS distributed system. The system high enclaves ensure discretionary security. The one-way connections are the only trusted component with respect to mandatory security. The JIFI architecture incorporates a one-way communications device, called the Pump, and existing COTS database replication technology to provide the extended JMCIS function. The JIFI assurance strategy described here complements and exploits modern system design methods, which separate data management from data processing, and enables effective low-cost MLS operation within that paradigm.

Reed, Michael G., Paul F. Syverson, and David M. Goldschlag, "Protocols using Anonymous Connections: Mobile Applications," Security Protocols, 5th International Workshop Proceedings, B. Christianson, B. Crispo, M. Lomas, and M. Roe (editors), Springer-Verlag LLNCS 1361, 1998, pp. 13-23. Postscript, PDF

This paper describes security protocols that use anonymous channels, which do not reveal their endpoints, as primitive, much in the way that key distribution protocols take encryption as primitive. This abstraction allows us to focus on high level security goals of these protocols much as abstracting away from encryption clarifies and emphasizes high level security goals of key distribution protocols. The protocols described are for mobile applications that protect the location information of the participating principals.

Syverson, Paul F., David M. Goldschlag, Michael G. Reed, "Anonymous Connections and Onion Routing," Proceedings of the 18th Annual Symposium on Security and Privacy, IEEE CS Press, Oakland, CA, May 1997, pp. 44-54. PostScript, PDF

Onion Routing provides anonymous connections that are strongly resistant to both eavesdropping and traffic analysis. Unmodified Internet applications can use these anonymous connections by means of proxies. The proxies may also make communication anonymous by removing identification from the data stream. Onion Routing has been implemented on Sun Solaris 2.4 with proxies for Web browsing, remote logins, and e-mail. This paper's contribution is a detailed specification of the implemented onion routing system, a vulnerability analysis base on this specification, and performance results.

Syverson, Paul F., Stuart G. Stubblebine, and David M. Goldschlag. "Unlinkable Serial Transactions," Proceedings of Financial Cryptography '97, Anguilla, BWI, February 1997. PostScript, PDF

We present a protocol for unlinkable serial transactions suitable for a variety of network-based subscription services. The protocol prevents the service from tracking the behavior of its customers while protecting the service vendor from abuse due to simultaneous or "cloned" usage from a single subscription. We present variants of the protocol supporting pay-per-use transactions within a subscription. We describe other applications including third-party subscription management, multivendor package sales, proof of group membership, and voter registration.

Syverson, Paul F., Michael G. Reed, and David M. Goldschlag, "Private Web Browsing," Journal of Computer Security Special Issue on Web Security, Volume 5, Number 3, 1997, pp. 237-248. Postscript, PDF

This paper describes a communications primitive, anonymous connections, that support bidirectional and near real-time channels that are resistant to both eavesdropping and traffic analysis. The connections are made anonymous, although communication need not be. These anonymous connections are versatile and support private use of many different Internet services. For our purposes, privacy means maintaining the confidentiality of both the data stream and the identity of communicating parties. These are both kept confidential from network elements as well as external observers. Private Web browsing is achieved by unmodified Web browsers using anonymous connections by means of HTTP proxies. Private Web browsing may be made anonymous too by a specialized proxy that removes identifying information from the HTTP data stream. This article specifies anonymous connections, describes our implementation, and discusses its application to Web browsing via HTTP proxies.

Voas, J., and Kassab, L., "Simulating Specification Errors and Ambiguities in Systems Employing Diversity," In Proceedings of Pacific Northwest Software Quality Conference, October 1997, Pages 223-234. Postscript, PDF

This paper looks at methods for predicting how likely it is that an n-version software system will suffer from common-mode failures. Common-mode failures are frequently caused by specification errors, specification ambiguities, and programmer faults. Since common-mode failures are detrimental to n-version systems, we have developed a method and a tool that observes the impact of simulated specification errors and specification ambiguities. These observations are made possible by a new family of fault injection algorithms designed to simulate specification anomalies. As a side-benefit, this analysis also provides clues concerning which portions of the specification, if even slightly wrong or misinterpreted, will lead to identical failures by two or more versions. This suggests which specification directives have the most impact on the system's functionality.

Voas, J., Ghosh, A., Kassab, L. & Charron, F., "Reducing Uncertainty About Common-Mode Failures," Proceedings of International Symposium on Software Reliability Engineering, November 1997, Pages 308-317. Postscript, PDF

Multi-version programming is employed in fault-tolerant computer systems in order to provide protection against common-mode failure in software. Multi-version programming involves building diverse software implementations of critical functions. The premise of building diverse versions is that the likelihood of a programming error in one version causing a failure in an identical manner as an error in another version is reduced. Skeptics of multi-version programming have correctly pointed out that common-mode failures between redundant diverse versions can reduce the return on investment in creating diverse versions.

To date, other than using historical data from other projects, there has been no way to estimate the potential for a given multi-version programming system to suffer a common-mode failure. This paper presents an algorithm and software analysis prototype to reduce the uncertainty of whether software flaws in diverse versions can result in common-mode failure. The analysis uses software fault-injection techniques to subject one or more versions to anomalous behavior. From this, we can predict how the software will behave if real faults exist in the multiple versions.

Back to the CHACS Publications Page.

Back to the Publications Page.